setLIntegral_eq_zero_iff' — Mathlib

English

For hs meas, and f AEMeasurable on μ.restrict s, ∫_s f dμ = 0 iff (∀ᵐ x, x∈s → f x = 0).

Русский

Для измеримого s и f AEMеас measurable на μ.restrict s: ∫_s f dμ = 0 тогда и только тогда, когда μ- почти каждая точка x в s удовлетворяет f x = 0.

LaTeX

$$$\\int^⁻_a in s, f a \\partial μ = 0 \\;\\Leftrightarrow\\; ∀^a x \\partial μ, x ∈ s \\to f x = 0$$$

Lean4

/-- The measurability assumption is necessary, otherwise there are counterexamples: for instance,
the conclusion fails if `s = univ` and `f` is the characteristic function of a Vitali set. -/
theorem setLIntegral_eq_zero_iff' {s : Set α} (hs : MeasurableSet s) {f : α → ℝ≥0∞}
    (hf : AEMeasurable f (μ.restrict s)) : ∫⁻ a in s, f a ∂μ = 0 ↔ ∀ᵐ x ∂μ, x ∈ s → f x = 0 :=
  (lintegral_eq_zero_iff' hf).trans (ae_restrict_iff' hs)

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