ae_eq_zero_of_lintegral_rpow_eq_zero

English

If p ≥ 0 and f is almost everywhere measurable with ∫ f^p dμ = 0, then f = 0 almost everywhere.

Русский

Если p ≥ 0 и f — ae-измеримая функция с ∫ f^p dμ = 0, то f = 0 ae-пропорционально μ.

LaTeX

$$$0 \\le p,\\; f:\\alpha\\to\\mathbb{R}_{\\ge 0}^{\\infty},\\; f \\text{ ae-measurable},\\; \\int f^p \\,d\\mu = 0 \\Rightarrow f =_{\\mathrm{ae}} 0$$$

Lean4

theorem ae_eq_zero_of_lintegral_rpow_eq_zero {p : ℝ} (hp0 : 0 ≤ p) {f : α → ℝ≥0∞} (hf : AEMeasurable f μ)
    (hf_zero : ∫⁻ a, f a ^ p ∂μ = 0) : f =ᵐ[μ] 0 :=
  by
  rw [lintegral_eq_zero_iff' (hf.pow_const p)] at hf_zero
  filter_upwards [hf_zero] with x
  rw [Pi.zero_apply, ← not_imp_not]
  exact fun hx => (rpow_pos_of_nonneg (pos_iff_ne_zero.2 hx) hp0).ne'

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