withDensity_eq_zero_iff — Mathlib

English

If f is a.e. zero, then μ.withDensity f = 0, and conversely provided a.e. equivalence.

Русский

Если f равно нулю почти везде, то μ.withDensity f = 0, и наоборот при условии эквивалентности almost everywhere.

LaTeX

$$$\\mu.withDensity f = 0 \\iff f =\\!\\!_{μ}^{\\text{a.e.}} 0$$$

Lean4

@[simp]
theorem withDensity_eq_zero_iff {f : α → ℝ≥0∞} (hf : AEMeasurable f μ) : μ.withDensity f = 0 ↔ f =ᵐ[μ] 0 := by
  rw [← measure_univ_eq_zero, withDensity_apply _ .univ, restrict_univ, lintegral_eq_zero_iff' hf]

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