LeanMachineLearning

ProbabilityTheory.Kernel.HasSubexponentialMGF.of_ae_mgf_le🔗

Lemma

From the authors

To prove that X is sub-exponential with respect to κ and ν, it suffices to check the bound on the mgf for each admissible t separately, almost everywhere.

Types
  • Ω : Type u_1mΩ : MeasurableSpace ΩA measurable space is a space equipped with a σ-algebra.
  • Ω' : Type u_2mΩ' : MeasurableSpace Ω'
Given
  • ν : MeasureTheory.Measure Ω'A measure is defined to be an outer measure that is countably additive on measurable sets, with the additional assumption that the outer measure is the canonical extension of the restricted measure.
  • κ : Kernel Ω' ΩA kernel from a measurable space α to another measurable space β is a measurable function κ : α → Measure β.
  • X : Ω → ℝ
  • V : ℝ
  • b : ℝ
Assuming
  • h_int : ∀ (t : ℝ), b * |t| ≤ 1 → MeasureTheory.Integrable (fun ω => Real.exp (t * X ω)) (ν.bind ⇑κ)Integrable f μ means that f is measurable and that the integral ∫⁻ a, ‖f a‖ ∂μ is finite.
  • h_mgf : ∀ (t : ℝ), b * |t| ≤ 1 → ∀ᵐ (ω' : Ω') ∂ν, mgf X (κ ω') t ≤ Real.exp (V * t ^ 2 / 2)f.Eventually p or ∀ᶠ x in f, p x mean that {x | p x} ∈ f.
Then
Code
protected lemma of_ae_mgf_le
    (h_int : ∀ t : ℝ, b * |t| ≤ 1 → Integrable (fun ω ↦ exp (t * X ω)) (κ ∘ₘ ν))
    (h_mgf : ∀ t : ℝ, b * |t| ≤ 1 → ∀ᵐ ω' ∂ν, mgf X (κ ω') t ≤ exp (V * t ^ 2 / 2)) :
    Kernel.HasSubexponentialMGF X V b κ ν where
  integrable_exp_mul
Proof
h_int
  mgf_le := by
    have h_rat : ∀ᵐ ω' ∂ν, ∀ q : ℚ, b * |(q : ℝ)| ≤ 1 →
        mgf X (κ ω') q ≤ exp (V * (q : ℝ) ^ 2 / 2) := by
      rw [ae_all_iff]
      intro q
      by_cases hq : b * |(q : ℝ)| ≤ 1
      · filter_upwards [h_mgf q hq] with ω' h _ using h
      · exact ae_of_all _ fun _ h ↦ absurd h hq
    have h_end : ∀ᵐ ω' ∂ν, ∀ t, b * |t| = 1 → mgf X (κ ω') t ≤ exp (V * t ^ 2 / 2) := by
      rcases le_or_gt b 0 with hb | hb
      · refine ae_of_all _ fun _ t ht ↦ absurd ht ?_
        nlinarith [abs_nonneg t]
      · have hb1 : b * |1 / b| ≤ 1 := by
          rw [abs_of_pos (by positivity), mul_one_div_cancel hb.ne']
        have hb2 : b * |-(1 / b)| ≤ 1 := by rwa [abs_neg]
        filter_upwards [h_mgf _ hb1, h_mgf _ hb2] with ω' h1 h2 t ht
        have ht' : |t| = 1 / b := by rw [eq_div_iff hb.ne', mul_comm]; exact ht
        rcases (abs_eq (by positivity : (0 : ℝ) ≤ 1 / b)).1 ht' with rfl | rfl
        · exact h1
        · exact h2
    filter_upwards [ae_forall_integrable_exp_mul_of_forall h_int, h_rat, h_end]
      with ω' h_int h_rat h_end t ht
    rcases ht.lt_or_eq with ht | ht
    · have hU : IsOpen {s : ℝ | b * |s| < 1} := isOpen_lt (by fun_prop) continuous_const
      have hsub : {s : ℝ | b * |s| < 1} ⊆ interior (integrableExpSet X (κ ω')) :=
        hU.subset_interior_iff.2 fun s hs ↦ h_int s hs.le
      refine ContinuousWithinAt.closure_le (f := mgf X (κ ω'))
        (g := fun s ↦ exp (V * s ^ 2 / 2))
        (s := {s : ℝ | b * |s| < 1} ∩ Set.range ((↑) : ℚ → ℝ))
        (Dense.open_subset_closure_inter Rat.denseRange_cast hU ht) ?_ ?_ ?_
      · exact (continuousOn_mgf.continuousAt
          (isOpen_interior.mem_nhds (hsub ht))).continuousWithinAt
      · exact (by fun_prop : Continuous fun s : ℝ ↦ exp (V * s ^ 2 / 2)).continuousAt
          |>.continuousWithinAt
      · rintro _ ⟨hs, q, rfl⟩
        exact h_rat q hs.le
    · exact h_end t ht

Meaning last changed in v4.34.0-rc2-76-g565f652 (2026-09-10).

Self-contained, with its dependencies inlined and proofs replaced by sorry: download the raw file · open it in the Lean web editor.

Dependency graph

Audit surface: 1 project declarations, 60 external constants

✓ Proved: no sorry anywhere in its closure

This is the tool's own reading of one build's recorded axioms, and it is not robust against an author who wants it to pass. Checking meant to be relied on should go through Comparator, which replays the proof through the kernel from an export against an explicit list of permitted axioms.