Lean module · Foundations
BanditRLProof.Algorithms.CUCBRoundMGF
Integrating the primitive masked MGF over the actual oracle action. The action and its triggered feedback retain their joint round kernel.
Module map
Imports
BanditRLProof.Algorithms.CUCBObservationMGF
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.CUCB.marginalMean_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.marginalMean_memReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem marginalMean_mem (D : Measure UnitOutcome) [IsProbabilityMeasure D] : marginalMean D ∈ Set.Icc (0:ℝ) 1
theorem
BanditRLProof.CUCB.centeredFactor_nonneg
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.centeredFactor_nonnegReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem centeredFactor_nonneg (D : Measure UnitOutcome) (tilt : ℝ) (x : UnitOutcome) : 0≤centeredFactor D tilt x
theorem
BanditRLProof.CUCB.centeredFactor_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.centeredFactor_leReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem centeredFactor_le (D : Measure UnitOutcome) [IsProbabilityMeasure D] (tilt : ℝ) (x : UnitOutcome) : centeredFactor D tilt x ≤ Real.exp |tilt|
theorem
BanditRLProof.CUCB.observedFactor_nonneg
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.observedFactor_nonnegReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem observedFactor_nonneg {m : ℕ} (D : Measure UnitOutcome) (i : Fin m) (tilt : ℝ) (z : Feedback m) : 0≤observedFactor D i tilt z
theorem
BanditRLProof.CUCB.observedFactor_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.observedFactor_leReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem observedFactor_le {m : ℕ} (D : Measure UnitOutcome) [IsProbabilityMeasure D] (i : Fin m) (tilt : ℝ) (z : Feedback m) : observedFactor D i tilt z≤Real.exp |tilt|
theorem
BanditRLProof.CUCB.measurable_observedFactor
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_observedFactorReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem measurable_observedFactor {m : ℕ} (D : Measure UnitOutcome) (i : Fin m) (tilt : ℝ) : Measurable (observedFactor D i tilt)
theorem
BanditRLProof.CUCB.integrable_observedFactor_comp
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_observedFactor_compReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem integrable_observedFactor_comp {Ω : Type*} [MeasurableSpace Ω] (ν : Measure Ω) [IsProbabilityMeasure ν] {m : ℕ} (D : Measure UnitOutcome) [IsProbabilityMeasure D] (i : Fin m) (tilt : ℝ) (g : Ω → Feedback m) (hg : Measurable g) : Integrable (fun ω => observedFactor D i tilt (g ω)) ν
theorem
BanditRLProof.CUCB.roundKernel_observedFactor_le_one
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.roundKernel_observedFactor_le_oneReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem roundKernel_observedFactor_le_one {A : Type*} [MeasurableSpace A] {m : ℕ} (oracle : Kernel (Input m) A) (environment : Kernel A (Feedback m)) [IsMarkovKernel oracle] [IsMarkovKernel environment] (D : Measure UnitOutcome) [IsProbabilityMeasure D] (i : Fin m) (hcompat : ∀a, ObservationCompatible (environment a) D i) (v : Input m) (tilt : ℝ) : (∫ z, observedFactor D i tilt z.2 ∂roundKernel oracle environment v)≤1