congr_ae — Mathlib

English

If f and g are almost everywhere equal with respect to μ, then the corresponding vector densities produce equal vector measures: μ.withDensityᵥ f = μ.withDensityᵥ g.

Русский

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

LaTeX

$$If $f =^{\mu} g$, then $\mu.withDensityᵥ f = \mu.withDensityᵥ g$$$

Lean4

theorem congr_ae {f g : α → E} (h : f =ᵐ[μ] g) : μ.withDensityᵥ f = μ.withDensityᵥ g :=
  by
  by_cases hf : Integrable f μ
  · ext i hi
    rw [withDensityᵥ_apply hf hi, withDensityᵥ_apply (hf.congr h) hi]
    exact integral_congr_ae (ae_restrict_of_ae h)
  · have hg : ¬Integrable g μ := by intro hg; exact hf (hg.congr h.symm)
    rw [withDensityᵥ, withDensityᵥ, dif_neg hf, dif_neg hg]

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