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]