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]