setIntegral_pos_iff_support_of_nonneg_ae

English

If f is nonnegative μ-a.e. on s and integrable, then 0 < ∫_s f implies μ(support f ∩ s) > 0.

Русский

Если f ≥ 0 μ-почти всюду на s и интегрируема, то 0 < ∫_s f ⇒ μ(support f ∩ s) > 0.

LaTeX

$$$$ 0 < \\int_{s} f \\, d\\mu \\;\\Rightarrow\\; \\mu(\\mathrm{supp}\; f \\cap s) > 0 $$$$

Lean4

theorem setIntegral_pos_iff_support_of_nonneg_ae {f : X → ℝ} (hf : 0 ≤ᵐ[μ.restrict s] f) (hfi : IntegrableOn f s μ) :
    (0 < ∫ x in s, f x ∂μ) ↔ 0 < μ (support f ∩ s) :=
  by
  rw [integral_pos_iff_support_of_nonneg_ae hf hfi, Measure.restrict_apply₀]
  rw [support_eq_preimage]
  exact hfi.aestronglyMeasurable.aemeasurable.nullMeasurable (measurableSet_singleton 0).compl

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