English
Under mild non-vanishing assumptions, the density-inverse operation returns the original measure.
Русский
При умеренных допущениях ненулевости плотности, операция обращения плотности возвращает исходную меру.
LaTeX
$$$(\mu.withDensity f).withDensity f^{-1} = μ$ under non-vanishing conditions.$$
Lean4
theorem withDensity_inv_same₀ {μ : Measure α} {f : α → ℝ≥0∞} (hf : AEMeasurable f μ) (hf_ne_zero : ∀ᵐ x ∂μ, f x ≠ 0)
(hf_ne_top : ∀ᵐ x ∂μ, f x ≠ ∞) : (μ.withDensity f).withDensity (fun x ↦ (f x)⁻¹) = μ :=
by
rw [← withDensity_mul₀ hf hf.inv]
suffices (f * fun x ↦ (f x)⁻¹) =ᵐ[μ] 1 by rw [withDensity_congr_ae this, withDensity_one]
filter_upwards [hf_ne_zero, hf_ne_top] with x hf_ne_zero hf_ne_top
simp only [Pi.mul_apply]
rw [ENNReal.mul_inv_cancel hf_ne_zero hf_ne_top, Pi.one_apply]
