BanditRLProof.LeafLemmas

No declaration docstring is present; use the chapter context and exact statement below.

@[simp] theorem pullCount_one : pullCount action a 1 = if action 0 = a then 1 else 0

No declaration docstring is present; use the chapter context and exact statement below.

theorem pullCount_succ_of_eq (h : action t = a) : pullCount action a (t + 1) = pullCount action a t + 1

No declaration docstring is present; use the chapter context and exact statement below.

theorem pullCount_succ_of_ne (h : action t ≠ a) : pullCount action a (t + 1) = pullCount action a t

No declaration docstring is present; use the chapter context and exact statement below.

theorem pullCount_le_succ : pullCount action a t ≤ pullCount action a (t + 1)

No declaration docstring is present; use the chapter context and exact statement below.

theorem pullCount_succ_le_succ : pullCount action a (t + 1) ≤ pullCount action a t + 1

No declaration docstring is present; use the chapter context and exact statement below.

theorem pullCount_mono {s t : Nat} (h : s ≤ t) : pullCount action a s ≤ pullCount action a t

No declaration docstring is present; use the chapter context and exact statement below.

theorem pullCount_le_time : pullCount action a t ≤ t

No declaration docstring is present; use the chapter context and exact statement below.

theorem pullCount_add_le (n : Nat) : pullCount action a (t + n) ≤ pullCount action a t + n

No declaration docstring is present; use the chapter context and exact statement below.

theorem pullCount_le_add : pullCount action a t ≤ pullCount action a (t + n)

No declaration docstring is present; use the chapter context and exact statement below.

theorem pullCount_eq_zero_of_forall_ne (h : ∀ s, s < t → action s ≠ a) : pullCount action a t = 0

No declaration docstring is present; use the chapter context and exact statement below.

theorem pullCount_eq_time_of_forall_eq (h : ∀ s, s < t → action s = a) : pullCount action a t = t

No declaration docstring is present; use the chapter context and exact statement below.

theorem pullCount_pos_of_eq_before {s t : Nat} (hst : s < t) (h : action s = a) : 0 < pullCount action a t

Pull counts depend only on the half-open action prefix `0, ..., t - 1`. This keeps later adaptive-policy wrappers from reproving the same induction when a history-generated trace is known to agree pointwise with an index-policy trace up to a finite horizon.

theorem pullCount_eq_of_forall_lt (action action' : ActionTrace Action) (a : Action) : forall t : Nat, (forall s : Nat, s < t -> action s = action' s) -> pullCount action a t = pullCount action' a t

No declaration docstring is present; use the chapter context and exact statement below.

@[simp] theorem pullCount_const_self (a : Action) (t : Nat) : pullCount (fun _ => a) a t = t

No declaration docstring is present; use the chapter context and exact statement below.

theorem pullCount_const_of_ne (b : Action) (h : b ≠ a) (t : Nat) : pullCount (fun _ => b) a t = 0

No declaration docstring is present; use the chapter context and exact statement below.

theorem pullCount_add_eq_of_forall_ne_between (n : Nat) (h : ∀ s, t ≤ s → s < t + n → action s ≠ a) : pullCount action a (t + n) = pullCount action a t

No declaration docstring is present; use the chapter context and exact statement below.

theorem pullCount_add_eq_add_of_forall_eq_between (n : Nat) (h : ∀ s, t ≤ s → s < t + n → action s = a) : pullCount action a (t + n) = pullCount action a t + n

The recursive pull count equals the number of matching actions in the half-open time prefix `0, ..., t - 1`. This is intentionally a dependency-light `List.range` bridge. The Mathlib `Finset.range` cardinality wrapper is a separate downstream leaf.

theorem pullCount_eq_list_filter_length : pullCount action a t = ((List.range t).filter (fun s : Nat => decide (action s = a))).length

No declaration docstring is present; use the chapter context and exact statement below.

theorem sumRewards_succ_of_eq (h : action t = a) : sumRewards action reward a (t + 1) = sumRewards action reward a t + reward t

No declaration docstring is present; use the chapter context and exact statement below.

theorem sumRewards_succ_of_ne (hzero : ∀ x : Reward, x + 0 = x) (h : action t ≠ a) : sumRewards action reward a (t + 1) = sumRewards action reward a t

No declaration docstring is present; use the chapter context and exact statement below.

theorem sumRewards_eq_zero_of_forall_ne (hzero : ∀ x : Reward, x + 0 = x) (h : ∀ s, s < t → action s ≠ a) : sumRewards action reward a t = 0

No declaration docstring is present; use the chapter context and exact statement below.

theorem sumRewards_const_of_ne (hzero : ∀ x : Reward, x + 0 = x) (b : Action) (h : b ≠ a) (t : Nat) : sumRewards (fun _ => b) reward a t = 0

No declaration docstring is present; use the chapter context and exact statement below.

theorem sumRewards_add_eq_of_forall_ne_between (hzero : ∀ x : Reward, x + 0 = x) (n : Nat) (h : ∀ s, t ≤ s → s < t + n → action s ≠ a) : sumRewards action reward a (t + n) = sumRewards action reward a t

The recursive reward sum equals a left fold over the half-open time prefix. This bridge deliberately keeps the false-branch `+ 0` steps in the fold, so it does not require additive laws beyond the weak assumptions used by `sumRewards`.

theorem sumRewards_eq_list_range_foldl : sumRewards action reward a t = (List.range t).foldl (fun acc s => acc + if action s = a then reward s else 0) 0

The reward sum can also drop nonmatching time steps from the list fold when the accumulator has a right-zero law. This is still dependency-light: it uses `List.range` and `List.filter`, not a Mathlib `Finset` sum.

theorem sumRewards_eq_list_range_filter_foldl (hzero : ∀ x : Reward, x + 0 = x) : sumRewards action reward a t = ((List.range t).filter (fun s : Nat => decide (action s = a))).foldl (fun acc s => acc + reward s) 0

No declaration docstring is present; use the chapter context and exact statement below.

@[simp] theorem bestMean_eq_mean_bestArm (model : FiniteBanditModel K) : model.bestMean = model.mean model.bestArm

No declaration docstring is present; use the chapter context and exact statement below.

theorem gap_of_ne_bestArm (model : FiniteBanditModel K) (arm : Fin K) (h : arm ≠ model.bestArm) : model.gap arm = model.bestMean - model.mean arm

No declaration docstring is present; use the chapter context and exact statement below.

@[simp] theorem pseudoRegret_one : pseudoRegret model action 1 = model.gap (action 0)

No declaration docstring is present; use the chapter context and exact statement below.

theorem pseudoRegret_succ_of_bestArm (h : action t = model.bestArm) : pseudoRegret model action (t + 1) = pseudoRegret model action t

No declaration docstring is present; use the chapter context and exact statement below.

theorem pseudoRegret_succ_of_gap_zero (h : model.gap (action t) = 0) : pseudoRegret model action (t + 1) = pseudoRegret model action t

No declaration docstring is present; use the chapter context and exact statement below.

theorem pseudoRegret_eq_zero_of_forall_bestArm (h : ∀ s, s < t → action s = model.bestArm) : pseudoRegret model action t = 0

No declaration docstring is present; use the chapter context and exact statement below.

theorem pseudoRegret_eq_zero_of_forall_gap_zero (h : ∀ s, s < t → model.gap (action s) = 0) : pseudoRegret model action t = 0

No declaration docstring is present; use the chapter context and exact statement below.

@[simp] theorem pseudoRegret_const_bestArm : pseudoRegret model (fun _ => model.bestArm) t = 0

No declaration docstring is present; use the chapter context and exact statement below.

theorem pseudoRegret_const_of_gap_zero (arm : Fin K) (h : model.gap arm = 0) : pseudoRegret model (fun _ => arm) t = 0

No declaration docstring is present; use the chapter context and exact statement below.

theorem pseudoRegret_add_eq_of_forall_bestArm_between (n : Nat) (h : ∀ s, t ≤ s → s < t + n → action s = model.bestArm) : pseudoRegret model action (t + n) = pseudoRegret model action t

No declaration docstring is present; use the chapter context and exact statement below.

theorem pseudoRegret_add_eq_of_forall_gap_zero_between (n : Nat) (h : ∀ s, t ≤ s → s < t + n → model.gap (action s) = 0) : pseudoRegret model action (t + n) = pseudoRegret model action t

The recursive pseudo-regret equals a left fold over the half-open time prefix. This is the dependency-light `List.range` bridge for the Rat-valued regret accumulator. It matches the recursive bracketing directly.

theorem pseudoRegret_eq_list_range_foldl : pseudoRegret model action t = (List.range t).foldl (fun acc s => acc + model.gap (action s)) 0