withDensity_eq_iff_of_sigmaFinite

English

Two densities f,g with finite integrals satisfy μ.withDensity f = μ.withDensity g iff f=g a.e.

Русский

Две плотности f,g с конечными интегралами удовлетворяют равенству с плотностью μ, если и только если f=g a.e.

LaTeX

$$$$ \mu \mathrm{withDensity} f = \mu \mathrm{withDensity} g \iff f =^{\mathrm{ae}}_{\mu} g $$$$

Lean4

theorem withDensity_eq_iff_of_sigmaFinite [SigmaFinite μ] {f g : α → ℝ≥0∞} (hf : AEMeasurable f μ)
    (hg : AEMeasurable g μ) : μ.withDensity f = μ.withDensity g ↔ f =ᵐ[μ] g :=
  ⟨fun hfg ↦ by
    refine ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite₀ hf hg fun s hs _ ↦ ?_
    rw [← withDensity_apply f hs, ← withDensity_apply g hs, ← hfg], withDensity_congr_ae⟩

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