Lean module · Foundations
BanditRLProof.Algorithms.CUCBConditionalMGF
Conditional compensated MGF for the actual CUCB trajectory.
Module map
Imports
BanditRLProof.Algorithms.CUCBRoundMGF, BanditRLProof.ConcentrationConditionalMGF
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.CUCB.observedNoise
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.observedNoiseReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def observedNoise {m : ℕ} (D : Measure UnitOutcome) (i : Fin m) (z : Feedback m) : ℝ
def
BanditRLProof.CUCB.observedIndicator
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.observedIndicatorReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
def observedIndicator {m : ℕ} (i : Fin m) (z : Feedback m) : ℝ
def
BanditRLProof.CUCB.observedCompensated
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.observedCompensatedReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def observedCompensated {m : ℕ} (D : Measure UnitOutcome) (i : Fin m) (tilt : ℝ) (z : Feedback m) : ℝ
theorem
BanditRLProof.CUCB.measurable_observedCompensated
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.measurable_observedCompensatedReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem measurable_observedCompensated {m : ℕ} (D : Measure UnitOutcome) (i : Fin m) (tilt : ℝ) : Measurable (observedCompensated D i tilt)
theorem
BanditRLProof.CUCB.observedCompensated_abs_le
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.observedCompensated_abs_leReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem observedCompensated_abs_le {m : ℕ} (D : Measure UnitOutcome) [IsProbabilityMeasure D] (i : Fin m) (tilt : ℝ) (z : Feedback m) : |observedCompensated D i tilt z|≤|tilt|+tilt^2/8
theorem
BanditRLProof.CUCB.integrable_exp_observedCompensated
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.integrable_exp_observedCompensatedReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem integrable_exp_observedCompensated {Ω : Type*} [MeasurableSpace Ω] (ν : Measure Ω) [IsProbabilityMeasure ν] {m : ℕ} (D : Measure UnitOutcome) [IsProbabilityMeasure D] (i : Fin m) (tilt scale : ℝ) (g : Ω → Feedback m) (hg : Measurable g) : Integrable (fun ω => Real.exp (scale*observedCompensated D i tilt (g ω))) ν
theorem
BanditRLProof.CUCB.exp_observedCompensated
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.exp_observedCompensatedReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem exp_observedCompensated {m : ℕ} (D : Measure UnitOutcome) (i : Fin m) (tilt : ℝ) (z : Feedback m) : Real.exp (observedCompensated D i tilt z)=observedFactor D i tilt z
theorem
BanditRLProof.CUCB.cucb_condExp_observedCompensated
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.cucb_condExp_observedCompensatedReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem cucb_condExp_observedCompensated (n : ℕ) (tilt : ℝ) : (cucbTrajectory oracle environment)[fun Y => Real.exp (observedCompensated D i tilt (Y (n+1)).2) | MeasurableSpace.comap (Preorder.frestrictLe n) inferInstance] ≤ᵐ[cucbTrajectory oracle environment] fun _ => 1
theorem
BanditRLProof.CUCB.cucb_successor_condMGF
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.cucb_successor_condMGFReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem cucb_successor_condMGF (n : ℕ) (tilt : ℝ) : Concentration.HasCondMGFUpperBoundAt (MeasurableSpace.comap (Preorder.frestrictLe n) inferInstance) (Preorder.measurable_frestrictLe n).comap_le (fun Y => observedCompensated D i tilt (Y (n+1)).2) 1 0 (cucbTrajectory oracle environment)
theorem
BanditRLProof.CUCB.cucb_initial_MGF
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.cucb_initial_MGFReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem cucb_initial_MGF (tilt : ℝ) : Concentration.HasMGFUpperBoundAt (fun Y : ℕ → Round A m => observedCompensated D i tilt (Y 0).2) 1 0 (cucbTrajectory oracle environment)