English
If μ is SFinite, then for any measurable s, μ.withDensity f s = ∫⁻ f dμ over s.
Русский
Если μ-SFinite, то для любого измеримого s: μ.withDensity f (s) = ∫_s f dμ.
LaTeX
$$$[SFinite\ μ]\ (\mu\text{ withDensity } f)(s) = \int_{s} f \, d\mu$$$
Lean4
theorem withDensity_apply' [SFinite μ] (f : α → ℝ≥0∞) (s : Set α) : μ.withDensity f s = ∫⁻ a in s, f a ∂μ :=
by
apply le_antisymm ?_ (withDensity_apply_le f s)
let t := toMeasurable μ s
calc
μ.withDensity f s ≤ μ.withDensity f t := measure_mono (subset_toMeasurable μ s)
_ = ∫⁻ a in t, f a ∂μ := (withDensity_apply f (measurableSet_toMeasurable μ s))
_ = ∫⁻ a in s, f a ∂μ := by congr 1; exact restrict_toMeasurable_of_sFinite s