Freedman / Bernstein inequality for martingales (adapted sums of sub-gamma increments) #
The variance-based (Freedman) martingale tail: a finite adapted sum of conditionally sub-gamma
increments satisfies P(∑ Yᵢ ≥ ε) ≤ exp(−ε²/(2(∑Vᵢ + cε))). Mathlib has Azuma (sub-Gaussian
martingales) but not the sub-gamma / Freedman version. Built on the sub-gamma MGF and Bernstein tail
of Contrib.BennettBernstein, with kernel-level tower additivity of the variance factors.
Contrib.Freedman.subgamma_bernstein_tail— the Freedman/Bernstein upper tail.Contrib.Freedman.Kernel.HasSubgammaMGF(+add_compProd,add_of_indep) — kernel-valued sub-gamma MGF with tower additivity.Contrib.Freedman.MeasureSubgammaMGF,Contrib.Freedman.HasCondSubgammaMGF— the measure- and conditional-level analogues, and the summation lemma over an adapted sequence.
Sorry-free and axiom-clean [propext, Classical.choice, Quot.sound].
structure
Contrib.Freedman.Kernel.HasSubgammaMGF
{Ω : Type u_1}
{Ω' : Type u_2}
{mΩ : MeasurableSpace Ω}
{mΩ' : MeasurableSpace Ω'}
(X : Ω → ℝ)
(V c : NNReal)
(κ : ProbabilityTheory.Kernel Ω' Ω)
(ν : MeasureTheory.Measure Ω' := by volume_tac)
:
Kernel-valued sub-gamma MGF bound. Integrability is required for every real parameter (rather than only the effective domain of the estimate), as in Mathlib's kernel-valued sub-Gaussian definition; this is what makes the tower argument composable.
- integrable_exp_mul (t : ℝ) : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) (ν.bind ⇑κ)
Instances For
theorem
Contrib.Freedman.Kernel.HasSubgammaMGF.ae_integrable_exp_mul
{Ω : Type u_1}
{Ω' : Type u_2}
{mΩ : MeasurableSpace Ω}
{mΩ' : MeasurableSpace Ω'}
{ν : MeasureTheory.Measure Ω'}
{κ : ProbabilityTheory.Kernel Ω' Ω}
{X : Ω → ℝ}
{V c : NNReal}
(h : HasSubgammaMGF X V c κ ν)
(t : ℝ)
:
theorem
Contrib.Freedman.Kernel.HasSubgammaMGF.ae_forall_integrable_exp_mul
{Ω : Type u_1}
{Ω' : Type u_2}
{mΩ : MeasurableSpace Ω}
{mΩ' : MeasurableSpace Ω'}
{ν : MeasureTheory.Measure Ω'}
{κ : ProbabilityTheory.Kernel Ω' Ω}
{X : Ω → ℝ}
{V c : NNReal}
(h : HasSubgammaMGF X V c κ ν)
:
theorem
Contrib.Freedman.Kernel.HasSubgammaMGF.memLp_exp_mul
{Ω : Type u_1}
{Ω' : Type u_2}
{mΩ : MeasurableSpace Ω}
{mΩ' : MeasurableSpace Ω'}
{ν : MeasureTheory.Measure Ω'}
{κ : ProbabilityTheory.Kernel Ω' Ω}
{X : Ω → ℝ}
{V c : NNReal}
(h : HasSubgammaMGF X V c κ ν)
(t : ℝ)
(p : NNReal)
:
MeasureTheory.MemLp (fun (ω : Ω) => Real.exp (t * X ω)) (↑p) (ν.bind ⇑κ)
@[simp]
theorem
Contrib.Freedman.Kernel.HasSubgammaMGF.fun_zero
{Ω : Type u_1}
{Ω' : Type u_2}
{mΩ : MeasurableSpace Ω}
{mΩ' : MeasurableSpace Ω'}
{ν : MeasureTheory.Measure Ω'}
{κ : ProbabilityTheory.Kernel Ω' Ω}
{c : NNReal}
[MeasureTheory.IsFiniteMeasure ν]
[ProbabilityTheory.IsZeroOrMarkovKernel κ]
:
HasSubgammaMGF (fun (x : Ω) => 0) 0 c κ ν
@[simp]
theorem
Contrib.Freedman.Kernel.HasSubgammaMGF.zero_measure
{Ω : Type u_1}
{Ω' : Type u_2}
{mΩ : MeasurableSpace Ω}
{mΩ' : MeasurableSpace Ω'}
{κ : ProbabilityTheory.Kernel Ω' Ω}
{X : Ω → ℝ}
{V c : NNReal}
:
HasSubgammaMGF X V c κ 0
@[simp]
theorem
Contrib.Freedman.Kernel.HasSubgammaMGF.zero
{Ω : Type u_1}
{Ω' : Type u_2}
{mΩ : MeasurableSpace Ω}
{mΩ' : MeasurableSpace Ω'}
{ν : MeasureTheory.Measure Ω'}
{κ : ProbabilityTheory.Kernel Ω' Ω}
{c : NNReal}
[MeasureTheory.IsFiniteMeasure ν]
[ProbabilityTheory.IsZeroOrMarkovKernel κ]
:
HasSubgammaMGF 0 0 c κ ν
theorem
Contrib.Freedman.Kernel.HasSubgammaMGF.congr
{Ω : Type u_1}
{Ω' : Type u_2}
{mΩ : MeasurableSpace Ω}
{mΩ' : MeasurableSpace Ω'}
{ν : MeasureTheory.Measure Ω'}
{κ : ProbabilityTheory.Kernel Ω' Ω}
{X : Ω → ℝ}
{V c : NNReal}
{Y : Ω → ℝ}
(h : HasSubgammaMGF X V c κ ν)
(h' : X =ᵐ[ν.bind ⇑κ] Y)
:
HasSubgammaMGF Y V c κ ν
theorem
Contrib.Freedman.Kernel.HasSubgammaMGF.prodMkLeft_compProd
{Ω : Type u_1}
{Ω' : Type u_2}
{mΩ : MeasurableSpace Ω}
{mΩ' : MeasurableSpace Ω'}
{ν : MeasureTheory.Measure Ω'}
{κ : ProbabilityTheory.Kernel Ω' Ω}
{c : NNReal}
{Ω'' : Type u_3}
{mΩ'' : MeasurableSpace Ω''}
{Y : Ω'' → ℝ}
{W : NNReal}
{η : ProbabilityTheory.Kernel Ω Ω''}
(h : HasSubgammaMGF Y W c η (ν.bind ⇑κ))
:
HasSubgammaMGF Y W c (ProbabilityTheory.Kernel.prodMkLeft Ω' η) (ν.compProd κ)
theorem
Contrib.Freedman.Kernel.HasSubgammaMGF.integrable_exp_add_compProd
{Ω : Type u_1}
{Ω' : Type u_2}
{mΩ : MeasurableSpace Ω}
{mΩ' : MeasurableSpace Ω'}
{ν : MeasureTheory.Measure Ω'}
{κ : ProbabilityTheory.Kernel Ω' Ω}
{X : Ω → ℝ}
{V c : NNReal}
{Ω'' : Type u_3}
{mΩ'' : MeasurableSpace Ω''}
{Y : Ω'' → ℝ}
{W : NNReal}
[MeasureTheory.SFinite ν]
{η : ProbabilityTheory.Kernel (Ω' × Ω) Ω''}
[ProbabilityTheory.IsZeroOrMarkovKernel η]
(hX : HasSubgammaMGF X V c κ ν)
(hY : HasSubgammaMGF Y W c η (ν.compProd κ))
(t : ℝ)
:
theorem
Contrib.Freedman.Kernel.HasSubgammaMGF.add_compProd
{Ω : Type u_1}
{Ω' : Type u_2}
{mΩ : MeasurableSpace Ω}
{mΩ' : MeasurableSpace Ω'}
{ν : MeasureTheory.Measure Ω'}
{κ : ProbabilityTheory.Kernel Ω' Ω}
{X : Ω → ℝ}
{V c : NNReal}
{Ω'' : Type u_3}
{mΩ'' : MeasurableSpace Ω''}
{Y : Ω'' → ℝ}
{W : NNReal}
[MeasureTheory.SFinite ν]
{η : ProbabilityTheory.Kernel (Ω' × Ω) Ω''}
[ProbabilityTheory.IsZeroOrMarkovKernel η]
(hX : HasSubgammaMGF X V c κ ν)
(hY : HasSubgammaMGF Y W c η (ν.compProd κ))
:
HasSubgammaMGF (fun (p : Ω × Ω'') => X p.1 + Y p.2) (V + W) c (κ.compProd η) ν
Tower-property additivity of variance factors for two consecutive kernel increments.
theorem
Contrib.Freedman.Kernel.HasSubgammaMGF.add_of_indep
{Ω : Type u_1}
{Ω' : Type u_2}
{mΩ : MeasurableSpace Ω}
{mΩ' : MeasurableSpace Ω'}
{ν : MeasureTheory.Measure Ω'}
{κ : ProbabilityTheory.Kernel Ω' Ω}
{X : Ω → ℝ}
{V c : NNReal}
{Ω'' : Type u_3}
{mΩ'' : MeasurableSpace Ω''}
{Y : Ω'' → ℝ}
{W : NNReal}
[MeasureTheory.SFinite ν]
{η : ProbabilityTheory.Kernel Ω Ω''}
[ProbabilityTheory.IsZeroOrMarkovKernel η]
(hX : HasSubgammaMGF X V c κ ν)
(hY : HasSubgammaMGF Y W c η (ν.bind ⇑κ))
:
HasSubgammaMGF (fun (p : Ω × Ω'') => X p.1 + Y p.2) (V + W) c (κ.compProd (ProbabilityTheory.Kernel.prodMkLeft Ω' η)) ν
Additivity in the usual sequential-kernel formulation.
def
Contrib.Freedman.HasCondSubgammaMGF
{Ω : Type u_1}
(m : MeasurableSpace Ω)
{mΩ : MeasurableSpace Ω}
(hm : m ≤ mΩ)
[StandardBorelSpace Ω]
(X : Ω → ℝ)
(V c : NNReal)
(μ : MeasureTheory.Measure Ω := by volume_tac)
[MeasureTheory.IsFiniteMeasure μ]
:
Conditional sub-gamma MGF, expressed using the conditional-expectation kernel.
Equations
- Contrib.Freedman.HasCondSubgammaMGF m hm X V c μ = Contrib.Freedman.Kernel.HasSubgammaMGF X V c (ProbabilityTheory.condExpKernel μ m) (μ.trim hm)
Instances For
theorem
Contrib.Freedman.HasCondSubgammaMGF.integrable_exp_mul
{Ω : Type u_1}
{m mΩ : MeasurableSpace Ω}
{X : Ω → ℝ}
{V c : NNReal}
{hm : m ≤ mΩ}
[StandardBorelSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
(h : HasCondSubgammaMGF m hm X V c μ)
(t : ℝ)
:
MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ
theorem
Contrib.Freedman.HasCondSubgammaMGF.ae_condExp_le
{Ω : Type u_1}
{m mΩ : MeasurableSpace Ω}
{X : Ω → ℝ}
{V c : NNReal}
{hm : m ≤ mΩ}
[StandardBorelSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
(h : HasCondSubgammaMGF m hm X V c μ)
{t : ℝ}
(ht : 0 ≤ t)
(htc : ↑c * t < 1)
:
structure
Contrib.Freedman.MeasureSubgammaMGF
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
(X : Ω → ℝ)
(V c : NNReal)
(μ : MeasureTheory.Measure Ω := by volume_tac)
:
Measure-valued sub-gamma MGF bound, including exponential integrability.
- integrable_exp_mul (t : ℝ) : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ
Instances For
theorem
Contrib.Freedman.measureSubgammaMGF_iff_kernel
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{X : Ω → ℝ}
{V c : NNReal}
:
MeasureSubgammaMGF X V c μ ↔ Kernel.HasSubgammaMGF X V c (ProbabilityTheory.Kernel.const Unit μ) (MeasureTheory.Measure.dirac ())
@[simp]
theorem
Contrib.Freedman.MeasureSubgammaMGF.fun_zero
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{c : NNReal}
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
:
MeasureSubgammaMGF (fun (x : Ω) => 0) 0 c μ
@[simp]
theorem
Contrib.Freedman.MeasureSubgammaMGF.zero
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{c : NNReal}
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
:
MeasureSubgammaMGF 0 0 c μ
theorem
Contrib.Freedman.MeasureSubgammaMGF.of_map
{Ω : Type u_1}
{Ω' : Type u_2}
{mΩ : MeasurableSpace Ω}
{mΩ' : MeasurableSpace Ω'}
{X : Ω → ℝ}
{V c : NNReal}
{μ : MeasureTheory.Measure Ω'}
{Y : Ω' → Ω}
(hY : AEMeasurable Y μ)
(h : MeasureSubgammaMGF X V c (MeasureTheory.Measure.map Y μ))
:
MeasureSubgammaMGF (X ∘ Y) V c μ
theorem
Contrib.Freedman.MeasureSubgammaMGF.trim
{Ω : Type u_1}
{m mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{X : Ω → ℝ}
{V c : NNReal}
(hm : m ≤ mΩ)
(hXm : Measurable X)
(hX : MeasureSubgammaMGF X V c μ)
:
MeasureSubgammaMGF X V c (μ.trim hm)
theorem
Contrib.Freedman.MeasureSubgammaMGF.add_of_hasCondSubgammaMGF
{Ω : Type u_1}
{m mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{X : Ω → ℝ}
[StandardBorelSpace Ω]
[MeasureTheory.IsFiniteMeasure μ]
{Y : Ω → ℝ}
{V W c : NNReal}
(hm : m ≤ mΩ)
(hX : MeasureSubgammaMGF X V c (μ.trim hm))
(hY : HasCondSubgammaMGF m hm Y W c μ)
:
MeasureSubgammaMGF (X + Y) (V + W) c μ
theorem
Contrib.Freedman.MeasureSubgammaMGF.sum_of_hasCondSubgammaMGF
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[StandardBorelSpace Ω]
{Y : ℕ → Ω → ℝ}
{V : ℕ → NNReal}
{c : NNReal}
{ℱ : MeasureTheory.Filtration ℕ mΩ}
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
(h_adapted : MeasureTheory.StronglyAdapted ℱ Y)
(h0 : MeasureSubgammaMGF (Y 0) (V 0) c μ)
(n : ℕ)
(h_subG : ∀ i < n - 1, HasCondSubgammaMGF (↑ℱ i) ⋯ (Y (i + 1)) (V (i + 1)) c μ)
:
MeasureSubgammaMGF (fun (ω : Ω) => ∑ i ∈ Finset.range n, Y i ω) (∑ i ∈ Finset.range n, V i) c μ
theorem
Contrib.Freedman.subgamma_bernstein_tail
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[StandardBorelSpace Ω]
{Y : ℕ → Ω → ℝ}
{V : ℕ → NNReal}
{c : NNReal}
{ℱ : MeasureTheory.Filtration ℕ mΩ}
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
(h_adapted : MeasureTheory.StronglyAdapted ℱ Y)
(h0 : MeasureSubgammaMGF (Y 0) (V 0) c μ)
(n : ℕ)
(h_subG : ∀ i < n - 1, HasCondSubgammaMGF (↑ℱ i) ⋯ (Y (i + 1)) (V (i + 1)) c μ)
{ε : ℝ}
(hV : 0 < ∑ i ∈ Finset.range n, V i)
(hc : 0 < c)
(hε : 0 ≤ ε)
:
Freedman/Bernstein upper tail for a finite adapted sum of conditionally sub-gamma increments.