withDensity_inv_same_le — Mathlib

English

If f is a.e. positive, then applying density f followed by density f⁻¹ returns the original measure.

Русский

Если f > 0 почти везде, то применение плотности f затем плотности f⁻¹ возвращает исходную меру.

LaTeX

$$ If f is a.e. positive, then (μ.withDensity f).withDensity f⁻¹ ≤ μ and in fact equals μ under appropriate conditions. $$

Lean4

theorem withDensity_inv_same_le {μ : Measure α} {f : α → ℝ≥0∞} (hf : AEMeasurable f μ) :
    (μ.withDensity f).withDensity f⁻¹ ≤ μ :=
  by
  change (μ.withDensity f).withDensity (fun x ↦ (f x)⁻¹) ≤ μ
  rw [← withDensity_mul₀ hf hf.inv]
  suffices (f * fun x ↦ (f x)⁻¹) ≤ᵐ[μ] 1 by
    refine (withDensity_mono this).trans ?_
    rw [withDensity_one]
  filter_upwards with x
  simp

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