withDensity_eq_iff — Mathlib

English

If densities f,g are a.e. equal, then measures with those densities are equal a.e.

Русский

Если плотности f,g равны почти повсюду, то меры с такими плотностями равны почти повсюду.

LaTeX

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

Lean4

theorem withDensity_eq_iff {f g : α → ℝ≥0∞} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) (hfi : ∫⁻ x, f x ∂μ ≠ ∞) :
    μ.withDensity f = μ.withDensity g ↔ f =ᵐ[μ] g :=
  ⟨fun hfg ↦ by
    refine AEMeasurable.ae_eq_of_forall_setLIntegral_eq hf hg hfi ?_ fun s hs _ ↦ ?_
    ·
      rwa [← setLIntegral_univ, ← withDensity_apply g MeasurableSet.univ, ← hfg, withDensity_apply f MeasurableSet.univ,
        setLIntegral_univ]
    · rw [← withDensity_apply f hs, ← withDensity_apply g hs, ← hfg], withDensity_congr_ae⟩

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