ae_eq_zero_of_hasSubgaussianMGF_zero

English

If c = 0, then X is almost surely zero with respect to the measure ν pushed through κ for almost every ω'.

Русский

Если c = 0, то X равна нулю почти surely относительно меры, полученной от ν через κ для почти всех ω'.

LaTeX

$$$\forall^{⋄} ω' ∂ ν:\ X =^{a.e.}_{κ(ω')} 0$$$

Lean4

theorem ae_eq_zero_of_hasSubgaussianMGF_zero (h : HasSubgaussianMGF X 0 κ ν) : ∀ᵐ ω' ∂ν, X =ᵐ[κ ω'] 0 :=
  by
  filter_upwards [(h.neg).measure_pos_eq_zero_of_hasSubGaussianMGF_zero,
    h.measure_pos_eq_zero_of_hasSubGaussianMGF_zero]
  intro ω' h1 h2
  simp_rw [Pi.neg_apply, Left.neg_pos_iff] at h1
  apply nonpos_iff_eq_zero.1
  calc
    (κ ω') {ω | X ω ≠ 0}
    _ = (κ ω') {ω | X ω < 0 ∨ 0 < X ω} := by simp_rw [ne_iff_lt_or_gt]
    _ ≤ (κ ω') {ω | X ω < 0} + (κ ω') {ω | 0 < X ω} := (measure_union_le _ _)
    _ = 0 := by simp [h1, h2]

Похожие утверждения