Lean module · Probability layer
BanditRLProof.ConcentrationConditionalMGF
Constructors connecting conditional expectation bounds to the shared fixed-tilt conditional MGF interface.
Module map
Imports
BanditRLProof.ConcentrationFixedMGF
Imported by
BanditRLProof.Algorithms.CUCBConditionalMGF, BanditRLProof.Algorithms.HOOConditionalMGF
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.Concentration.hasCondMGFUpperBoundAt_of_condExp_le
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book · Reinforcement Learning Book · Online Learning Book
2. Probability, kernels, filtrations, and concentration
Canonical node identity
declaration:BanditRLProof.Concentration.hasCondMGFUpperBoundAt_of_condExp_leReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem hasCondMGFUpperBoundAt_of_condExp_le {Ω : Type*} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {μ : Measure Ω} [IsFiniteMeasure μ] (m : MeasurableSpace Ω) (hm : m ≤ mΩ) (X : Ω → ℝ) (t ψ : ℝ) (hi : ∀ s, Integrable (fun ω => Real.exp (s * X ω)) μ) (hc : μ[fun ω => Real.exp (t * X ω) | m] ≤ᵐ[μ] fun _ => Real.exp ψ) : HasCondMGFUpperBoundAt m hm X t ψ μ