Lean module · Foundations
BanditRLProof.Algorithms.CUCBCharge
Integer analysis counters for the repaired source charging rule. These counters use only actions and fixed instance data, never current feedback. They are analysis objects, not an additional learner input.
Module map
Imports
BanditRLProof.Algorithms.CUCBThreshold, BanditRLProof.Algorithms.CUCBTrajectory
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
structure
BanditRLProof.CUCB.ChargeData
Compiled
Fixed inputs to the analysis rule. Full source model obligations are separate.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.CUCB.ChargeDataReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
structure ChargeData (A : Type*) (m : ℕ) where
def
BanditRLProof.CUCB.ChargeData.choose
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.CUCB.ChargeData.chooseReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def choose (N : Fin m → ℕ) (a : A) : Option (Fin m)
def
BanditRLProof.CUCB.ChargeData.counters
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.CUCB.ChargeData.countersReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def counters (actions : ℕ → A) : ℕ → Fin m → ℕ | 0 => fun _ => 0 | n+1 => fun i => counters actions n i + if C.choose (counters actions n) (actions n) = some i then 1 else 0 theorem counters_zero (actions : ℕ → A) (i : Fin m) : C.counters actions 0 i=0
theorem
BanditRLProof.CUCB.ChargeData.counters_zero
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.CUCB.ChargeData.counters_zeroReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem counters_zero (actions : ℕ → A) (i : Fin m) : C.counters actions 0 i=0
theorem
BanditRLProof.CUCB.ChargeData.counters_succ
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.CUCB.ChargeData.counters_succReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem counters_succ (actions : ℕ → A) (n : ℕ) (i : Fin m) : C.counters actions (n+1) i=C.counters actions n i+ if C.choose (C.counters actions n) (actions n)=some i then 1 else 0
theorem
BanditRLProof.CUCB.ChargeData.choose_mem
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.CUCB.ChargeData.choose_memReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem choose_mem (N : Fin m → ℕ) (a : A) (i : Fin m) (h : C.choose N a=some i) : C.bad a=true ∧ i∈C.triggers a
theorem
BanditRLProof.CUCB.ChargeData.choose_sufficient
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.CUCB.ChargeData.choose_sufficientReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem choose_sufficient (N : Fin m → ℕ) (a : A) (i : Fin m) (h : C.choose N a=some i) (hu : 0<C.inverseGap a) (hp : ∀j∈C.triggers a, 0<C.triggerLower j) (n : ℕ) (hi : samplingThreshold n (C.inverseGap a) (C.triggerLower i)<N i) : ∀j∈C.triggers a, samplingThreshold n (C.inverseGap a) (C.triggerLower j)<N j
theorem
BanditRLProof.CUCB.ChargeData.counters_le_time
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.CUCB.ChargeData.counters_le_timeReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem counters_le_time (actions : ℕ → A) (n : ℕ) (i : Fin m) : C.counters actions n i≤n
theorem
BanditRLProof.CUCB.ChargeData.counters_mono_step
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.CUCB.ChargeData.counters_mono_stepReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem counters_mono_step (actions : ℕ → A) (n : ℕ) (i : Fin m) : C.counters actions n i≤C.counters actions (n+1) i
theorem
BanditRLProof.CUCB.ChargeData.counters_causal
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.CUCB.ChargeData.counters_causalReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem counters_causal (actions actions' : ℕ → A) (n : ℕ) (h : ∀t<n, actions t=actions' t) : C.counters actions n=C.counters actions' n
theorem
BanditRLProof.CUCB.ChargeData.charge_before_feedback
Compiled
The charge may use the current action but not its sampled feedback.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.CUCB.ChargeData.charge_before_feedbackReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem charge_before_feedback (Y Z : ℕ → Round A m) (n : ℕ) (hpast : ∀t<n, (Y t).1=(Z t).1) (hcurrent : (Y n).1=(Z n).1) : C.choose (C.counters (fun t => (Y t).1) n) (Y n).1 = C.choose (C.counters (fun t => (Z t).1) n) (Z n).1
theorem
BanditRLProof.CUCB.ChargeData.counters_sum
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.CUCB.ChargeData.counters_sumReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem counters_sum (actions : ℕ → A) (n : ℕ) : ∑i:Fin m, C.counters actions n i = ∑t∈Finset.range n, if C.bad (actions t) then 1 else 0
theorem
BanditRLProof.CUCB.ChargeData.counters_eq_sum
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.CUCB.ChargeData.counters_eq_sumReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem counters_eq_sum (actions : ℕ → A) (n : ℕ) (i : Fin m) : C.counters actions n i = ∑t∈Finset.range n, if C.choose (C.counters actions t) (actions t)=some i then 1 else 0
def
BanditRLProof.CUCB.ChargeData.chargedObservations
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.CUCB.ChargeData.chargedObservationsReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def chargedObservations (Y : ℕ → Round A m) (n : ℕ) (i : Fin m) : ℕ
theorem
BanditRLProof.CUCB.ChargeData.chargedObservations_le_observationCount
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.CUCB.ChargeData.chargedObservations_le_observationCountReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem chargedObservations_le_observationCount (Y : ℕ → Round A m) (n : ℕ) (i : Fin m) : C.chargedObservations Y n i≤observationCount (fun t => (Y t).2) n i
theorem
BanditRLProof.CUCB.ChargeData.chargedObservations_le_counters
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.CUCB.ChargeData.chargedObservations_le_countersReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem chargedObservations_le_counters (Y : ℕ → Round A m) (n : ℕ) (i : Fin m) : C.chargedObservations Y n i≤C.counters (fun t => (Y t).1) n i
theorem
BanditRLProof.CUCB.ChargeData.counters_le_observations_of_always_triggered
Compiled
Deterministic triggering is recovered without a probabilistic tail bound.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.CUCB.ChargeData.counters_le_observations_of_always_triggeredReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem counters_le_observations_of_always_triggered (Y : ℕ → Round A m) (n : ℕ) (i : Fin m) (h : ∀t<n, C.choose (C.counters (fun s => (Y s).1) t) (Y t).1=some i → (Y t).2.1 i=true) : C.counters (fun t => (Y t).1) n i≤observationCount (fun t => (Y t).2) n i
theorem
BanditRLProof.CUCB.ChargeData.measurable_choose
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.CUCB.ChargeData.measurable_chooseReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem measurable_choose : Measurable (fun p : (Fin m → ℕ) × A => C.choose p.1 p.2)
theorem
BanditRLProof.CUCB.ChargeData.measurable_counters
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.CUCB.ChargeData.measurable_countersReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem measurable_counters (n : ℕ) : Measurable (fun actions : ℕ → A => C.counters actions n)
theorem
BanditRLProof.CUCB.ChargeData.measurable_path_charge
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.CUCB.ChargeData.measurable_path_chargeReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem measurable_path_charge (n : ℕ) : Measurable (fun Y : ℕ → Round A m => C.choose (C.counters (fun t => (Y t).1) n) (Y n).1)