BanditRLProof.ConcentrationFixedMGF

A kernel-valued MGF upper bound at one fixed tilt. Integrability is required at every tilt so that successive conditional laws can be composed without adding boundedness assumptions.

structure HasMGFUpperBoundAt (X : Ω → ℝ) (t ψ : ℝ) (κ : ProbabilityTheory.Kernel Ω' Ω) (ν : Measure Ω' := by volume_tac) : Prop where

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

lemma ae_integrable_exp_mul (h : HasMGFUpperBoundAt X t ψ κ ν) (s : ℝ) : ∀ᵐ ω' ∂ν, Integrable (fun y ↦ exp (s * X y)) (κ ω')

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

lemma ae_forall_integrable_exp_mul (h : HasMGFUpperBoundAt X t ψ κ ν) : ∀ᵐ ω' ∂ν, ∀ s, Integrable (fun ω ↦ exp (s * X ω)) (κ ω')

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

lemma congr {Y : Ω -> Real} (h : HasMGFUpperBoundAt X t ψ κ ν) (hXY : X =ᵐ[κ ∘ₘ ν] Y) : HasMGFUpperBoundAt Y t ψ κ ν where

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

lemma congr_iff {Y : Ω -> Real} (hXY : X =ᵐ[κ ∘ₘ ν] Y) : HasMGFUpperBoundAt X t ψ κ ν ↔ HasMGFUpperBoundAt Y t ψ κ ν

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

lemma memLp_exp_mul (h : HasMGFUpperBoundAt X t ψ κ ν) (s : ℝ) (p : ℝ≥0) : MemLp (fun ω ↦ exp (s * X ω)) p (κ ∘ₘ ν)

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

lemma zero_kernel : HasMGFUpperBoundAt X t ψ (0 : ProbabilityTheory.Kernel Ω' Ω) ν

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

lemma zero_measure : HasMGFUpperBoundAt X t ψ κ (0 : Measure Ω')

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

lemma prodMkLeft_compProd {η : ProbabilityTheory.Kernel Ω Ω''} (h : HasMGFUpperBoundAt Y t ψY η (κ ∘ₘ ν)) : HasMGFUpperBoundAt Y t ψY (ProbabilityTheory.Kernel.prodMkLeft Ω' η) (ν ⊗ₘ κ)

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

lemma integrable_exp_add_compProd {η : ProbabilityTheory.Kernel (Ω' × Ω) Ω''} [ProbabilityTheory.IsZeroOrMarkovKernel η] (hX : HasMGFUpperBoundAt X t ψ κ ν) (hY : HasMGFUpperBoundAt Y t ψY η (ν ⊗ₘ κ)) (s : ℝ) : Integrable (fun ω ↦ exp (s * (X ω.1 + Y ω.2))) ((κ ⊗ₖ η) ∘ₘ ν)

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

theorem add_compProd {η : ProbabilityTheory.Kernel (Ω' × Ω) Ω''} [ProbabilityTheory.IsZeroOrMarkovKernel η] (hX : HasMGFUpperBoundAt X t ψ κ ν) (hY : HasMGFUpperBoundAt Y t ψY η (ν ⊗ₘ κ)) : HasMGFUpperBoundAt (fun p ↦ X p.1 + Y p.2) t (ψ + ψY) (κ ⊗ₖ η) ν

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

lemma add_comp {η : ProbabilityTheory.Kernel Ω Ω''} [ProbabilityTheory.IsZeroOrMarkovKernel η] (hX : HasMGFUpperBoundAt X t ψ κ ν) (hY : HasMGFUpperBoundAt Y t ψY η (κ ∘ₘ ν)) : HasMGFUpperBoundAt (fun p ↦ X p.1 + Y p.2) t (ψ + ψY) (κ ⊗ₖ ProbabilityTheory.Kernel.prodMkLeft Ω' η) ν

A measure-level MGF upper bound at one fixed tilt.

structure HasMGFUpperBoundAt (X : Ω → ℝ) (t ψ : ℝ) (μ : Measure Ω := by volume_tac) : Prop where

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

lemma hasMGFUpperBoundAt_iff_kernel : HasMGFUpperBoundAt X t ψ μ ↔ Kernel.HasMGFUpperBoundAt X t ψ (ProbabilityTheory.Kernel.const Unit μ) (Measure.dirac ())

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

lemma of_map {Ω' : Type*} {mΩ' : MeasurableSpace Ω'} {μ' : Measure Ω'} {Z : Ω' → Ω} (hZ : AEMeasurable Z μ') (h : HasMGFUpperBoundAt X t ψ (μ'.map Z)) : HasMGFUpperBoundAt (X ∘ Z) t ψ μ' where

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

lemma id_map_iff (hX : AEMeasurable X μ) : HasMGFUpperBoundAt id t ψ (μ.map X) ↔ HasMGFUpperBoundAt X t ψ μ

Subtracting a deterministic log-MGF budget turns a fixed-tilt bound into a unit-tilt zero-budget bound. This is the algebraic step used to iterate exponential supermartingale increments.

theorem compensated (h : HasMGFUpperBoundAt X t ψ μ) : HasMGFUpperBoundAt (fun ω => t * X ω - ψ) 1 0 μ

Conditional fixed-tilt MGF bound, expressed through Mathlib's conditional expectation kernel.

def HasCondMGFUpperBoundAt (X : Ω → ℝ) (t ψ : ℝ) (μ : Measure Ω := by volume_tac) [IsFiniteMeasure μ] : Prop

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

lemma trim (hm : m ≤ mΩ) (hXm : Measurable[m] X) (hX : HasMGFUpperBoundAt X t ψ μ) : HasMGFUpperBoundAt X t ψ (μ.trim hm) where

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

theorem add_of_hasCondMGFUpperBoundAt {Y : Ω → ℝ} {ψX ψY : ℝ} (hm : m ≤ mΩ) (hX : HasMGFUpperBoundAt X t ψX (μ.trim hm)) (hY : HasCondMGFUpperBoundAt m hm Y t ψY μ) : HasMGFUpperBoundAt (X + Y) t (ψX + ψY) μ

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

lemma measure_ge_le_exp_add (h : HasMGFUpperBoundAt X t ψ μ) (ε : ℝ) (ht : 0 ≤ t) : μ.real {ω | ε ≤ X ω} ≤ exp (-t * ε + ψ)

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

theorem HasMGFUpperBoundAt.sum_of_hasCondMGFUpperBoundAt [IsZeroOrProbabilityMeasure μ] (h_adapted : StronglyAdapted ℱ Y) (h0 : HasMGFUpperBoundAt (Y 0) t (ψY 0) μ) (n : ℕ) (h_mgf : ∀ i < n - 1, HasCondMGFUpperBoundAt (ℱ i) (ℱ.le i) (Y (i + 1)) t (ψY (i + 1)) μ) : HasMGFUpperBoundAt (fun ω ↦ ∑ i ∈ Finset.range n, Y i ω) t (∑ i ∈ Finset.range n, ψY i) μ

Fixed-tilt Chernoff bound for a strongly adapted finite sum with conditional MGF budgets.

theorem measure_sum_ge_le_of_hasCondMGFUpperBoundAt [IsZeroOrProbabilityMeasure μ] (h_adapted : StronglyAdapted ℱ Y) (h0 : HasMGFUpperBoundAt (Y 0) t (ψY 0) μ) (n : ℕ) (h_mgf : ∀ i < n - 1, HasCondMGFUpperBoundAt (ℱ i) (ℱ.le i) (Y (i + 1)) t (ψY (i + 1)) μ) (ε : ℝ) (ht : 0 ≤ t) : μ.real {ω | ε ≤ ∑ i ∈ Finset.range n, Y i ω} ≤ exp (-t * ε + ∑ i ∈ Finset.range n, ψY i)

Fixed-tilt tail bound with a random predictable compensator retained in the event. The conditional MGF hypotheses are imposed on the compensated increments `tilt * Y i - varianceCoeff * V i`; on the event where the cumulative compensator is at most `varianceBudget`, their exponential tail controls the uncompensated sum.

theorem measure_sum_ge_inter_sum_le_of_compensated_hasCondMGFUpperBoundAt [IsZeroOrProbabilityMeasure μ] (Y V : ℕ → Ω → ℝ) (n : ℕ) (tilt varianceCoeff threshold varianceBudget : ℝ) (h_adapted : StronglyAdapted ℱ (fun i ω => tilt * Y i ω - varianceCoeff * V i ω)) (h0 : HasMGFUpperBoundAt (fun ω => tilt * Y 0 ω - varianceCoeff * V 0 ω) 1 0 μ) (h_mgf : ∀ i < n - 1, HasCondMGFUpperBoundAt (ℱ i) (ℱ.le i) (fun ω => tilt * Y (i + 1) ω - varianceCoeff * V (i + 1) ω) 1 0 μ) (htilt : 0 ≤ tilt) (hvarianceCoeff : 0 ≤ varianceCoeff) : μ {ω | threshold ≤ ∑ i ∈ Finset.range n, Y i ω ∧ (∑ i ∈ Finset.range n, V i ω) ≤ varianceBudget} ≤ ENNReal.ofReal (Real.exp (-tilt * threshold + varianceCoeff * varianceBudget))