withDensity_inv_same — Mathlib

English

For measurable f, the density equality holds: applying density f then inverse density yields the same result as direct equality of measures in appropriate equality context.

Русский

Для измеримой f выполняется эквивалентность плотностей: применение плотности f затем обратной плотности совпадает с прямым равенством мер.

LaTeX

$$$(μ.withDensity f).withDensity f^{-1} = μ$ when f ≠ 0 a.e. and finite a.e.$$

Lean4

theorem withDensity_inv_same {μ : Measure α} {f : α → ℝ≥0∞} (hf : Measurable f) (hf_ne_zero : ∀ᵐ x ∂μ, f x ≠ 0)
    (hf_ne_top : ∀ᵐ x ∂μ, f x ≠ ∞) : (μ.withDensity f).withDensity (fun x ↦ (f x)⁻¹) = μ :=
  withDensity_inv_same₀ hf.aemeasurable hf_ne_zero hf_ne_top

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