withDensityᵥ_eq_iff — Mathlib

English

For real-valued integrable f, μ.withDensityᵥ f equals the difference of the two signed measures obtained by densitying μ with ENNReal.ofReal f and ENNReal.ofReal(-f).

Русский

Для действительной интегрируемой f векторная мера μ.withDensityᵥ f равна разности двух знаковых мер, полученных наложением плотности ENNReal.ofReal f и ENNReal.ofReal(-f) на μ.

LaTeX

$$$\mu.withDensityᵥ f = \mathrm{toSignedMeasure}(\mu.withDensity (x \mapsto ENNReal.ofReal(f(x)))) - \mathrm{toSignedMeasure}(\mu.withDensity (x \mapsto ENNReal.ofReal(-f(x))))$$$

Lean4

theorem withDensityᵥ_eq_iff [CompleteSpace E] {f g : α → E} (hf : Integrable f μ) (hg : Integrable g μ) :
    μ.withDensityᵥ f = μ.withDensityᵥ g ↔ f =ᵐ[μ] g :=
  ⟨fun hfg => hf.ae_eq_of_withDensityᵥ_eq hg hfg, fun h => WithDensityᵥEq.congr_ae h⟩

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