English
If the subgaussian MGF parameter is zero, then the right-tail probability of X above any positive ε is zero almost everywhere (in the base measure).
Русский
Если параметр субгауссового MGФ равен нулю, то правая граница хвоста X выше любого положительного ε равна нулю почти наверняка.
LaTeX
$$$\text{If } c=0:\forall^{⋄} ω' ∂ ν:\ (κ(ω'))\{ω: ε ≤ X(ω)\} = 0\quad \text{for all } ε>0$$$
Lean4
theorem measure_pos_eq_zero_of_hasSubGaussianMGF_zero (h : HasSubgaussianMGF X 0 κ ν) :
∀ᵐ ω' ∂ν, (κ ω') {ω | 0 < X ω} = 0 :=
by
have hs : {ω | 0 < X ω} = ⋃ ε : { ε : ℚ // 0 < ε }, {ω | ε ≤ X ω} :=
by
ext ω
simp only [Set.mem_setOf_eq, Set.mem_iUnion, Subtype.exists, exists_prop]
constructor
· intro hp
obtain ⟨q, h1, h2⟩ := exists_rat_btwn hp
exact ⟨q, (q.cast_pos.1 h1), h2.le⟩
· intro ⟨q, h1, h2⟩
exact lt_of_lt_of_le (q.cast_pos.2 h1) h2
have hb (ε : ℚ) : ∀ᵐ ω' ∂ν, 0 < ε → (κ ω') {ω | ε ≤ X ω} = 0 :=
by
filter_upwards [h.measure_ge_le_exp_add ε, h.isFiniteMeasure] with ω' hm _ hε
simp only [neg_mul, NNReal.coe_zero, zero_mul, zero_div, add_zero] at hm
suffices (κ ω').real {ω | ε ≤ X ω} = 0 by simpa [Measure.real, ENNReal.toReal_eq_zero_iff]
have hl : Filter.Tendsto (fun t ↦ rexp (-(t * ε))) Filter.atTop (𝓝 0) :=
by
apply tendsto_exp_neg_atTop_nhds_zero.comp
exact Filter.Tendsto.atTop_mul_const (ε.cast_pos.2 hε) (fun _ a ↦ a)
apply le_antisymm
· exact ge_of_tendsto hl (Filter.eventually_atTop.2 ⟨0, hm⟩)
· exact measureReal_nonneg
filter_upwards [ae_all_iff.2 hb] with ω' hn
simp only [hs, measure_iUnion_null_iff, Subtype.forall]
exact fun _ ↦ hn _
