English
For a density f and a set s that is null-measurable with respect to μ, the measure of s under μ with density f equals the integral of f over s with respect to μ.
Русский
Для плотности f и множества s, которое по μ нулево измеримо, мера s под плотностью f равна интегралу f по s относительно μ.
LaTeX
$$$(\\mu_f)(s) = \\int\\_s f \\, d\\mu$$$
Lean4
theorem withDensity_apply₀ (f : α → ℝ≥0∞) {s : Set α} (hs : NullMeasurableSet s μ) :
μ.withDensity f s = ∫⁻ a in s, f a ∂μ := by
let t := toMeasurable μ s
have A : ∫⁻ a in t, f a ∂μ = ∫⁻ a in s, f a ∂μ := setLIntegral_congr hs.toMeasurable_ae_eq
have B : μ.withDensity f t = μ.withDensity f s :=
measure_congr (withDensity_absolutelyContinuous μ f hs.toMeasurable_ae_eq)
rw [← A, ← B]
exact withDensity_apply _ (measurableSet_toMeasurable μ s)
