integral_eq_zero_iff_of_nonneg_ae

English

If f: α → Real is integrable and nonnegative almost everywhere, then ∫ f = 0 implies f = 0 a.e.

Русский

Если f: α → Real интегрируема и неотрицательна почти нигде, то ∫ f = 0 тогда и только f = 0 почти всюду.

LaTeX

$$$\\\\int a \\, f(a) \\, d\\\\mu = 0 \\\\Longrightarrow \\\\ f = a.e. \\\\ 0$ [для неотрицательных ae-функций]$$

Lean4

theorem integral_eq_zero_iff_of_nonneg_ae {f : α → ℝ} (hf : 0 ≤ᵐ[μ] f) (hfi : Integrable f μ) :
    ∫ x, f x ∂μ = 0 ↔ f =ᵐ[μ] 0 :=
  by
  simp_rw [integral_eq_lintegral_of_nonneg_ae hf hfi.1, ENNReal.toReal_eq_zero_iff, ← ENNReal.not_lt_top, ←
    hasFiniteIntegral_iff_ofReal hf, hfi.2, not_true_eq_false, or_false]
  rw [lintegral_eq_zero_iff']
  · rw [← hf.ge_iff_eq', Filter.EventuallyEq, Filter.EventuallyLE]
    simp only [Pi.zero_apply, ofReal_eq_zero]
  · exact (ENNReal.measurable_ofReal.comp_aemeasurable hfi.1.aemeasurable)

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