withDensity_congr_ae — Mathlib

English

If f and g are almost everywhere equal with respect to μ, their densities yield equal measures μ.withDensity f = μ.withDensity g.

Русский

Если f и g равны почти всюду относительно μ, то μ.withDensity f = μ.withDensity g.

LaTeX

$$$f =^{\mathrm{ae}}_{\mu} g \Rightarrow \mu.withDensity f = \mu.withDensity g$$$

Lean4

theorem withDensity_congr_ae {f g : α → ℝ≥0∞} (h : f =ᵐ[μ] g) : μ.withDensity f = μ.withDensity g :=
  by
  refine Measure.ext fun s hs => ?_
  rw [withDensity_apply _ hs, withDensity_apply _ hs]
  exact lintegral_congr_ae (ae_restrict_of_ae h)

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