ae_eq_zero_of_hasSubgaussianMGF_zero_of_measurable

English

If X is measurable and has zero subgaussian MGF with c = 0, then X = 0 almost everywhere with respect to the measure κ ∘ₘ ν.

Русский

Если X измерима и имеет нулевой субгауссов MGФ с c = 0, то X равно нулю почти всюду относительно меры κ ∘ₘ ν.

LaTeX

$$$X =^{a.e.}_{κ \circ_{m} ν} 0$ when $X$ is measurable and HasSubgaussianMGF X 0 κ ν$$

Lean4

/-- Auxiliary lemma for `ae_eq_zero_of_hasSubgaussianMGF_zero'`. -/
theorem ae_eq_zero_of_hasSubgaussianMGF_zero_of_measurable (hX : Measurable X) (h : HasSubgaussianMGF X 0 κ ν) :
    X =ᵐ[κ ∘ₘ ν] 0 :=
  by
  rw [Filter.EventuallyEq, Measure.ae_comp_iff (measurableSet_eq_fun hX (by fun_prop))]
  exact h.ae_eq_zero_of_hasSubgaussianMGF_zero

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