ae_eq_of_withDensityᵥ_eq — Mathlib

English

If f and g are integrable, then μ.withDensityᵥ f = μ.withDensityᵥ g if and only if f and g are equal almost everywhere with respect to μ.

Русский

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

LaTeX

$$$(\mu.withDensityᵥ f) = (\mu.withDensityᵥ g) \iff f =^{\mu} g$$$

Lean4

/-- Having the same density implies the underlying functions are equal almost everywhere. -/
theorem ae_eq_of_withDensityᵥ_eq [CompleteSpace E] {f g : α → E} (hf : Integrable f μ) (hg : Integrable g μ)
    (hfg : μ.withDensityᵥ f = μ.withDensityᵥ g) : f =ᵐ[μ] g :=
  by
  refine hf.ae_eq_of_forall_setIntegral_eq f g hg fun i hi _ => ?_
  rw [← withDensityᵥ_apply hf hi, hfg, withDensityᵥ_apply hg hi]

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