withDensity_apply' — Mathlib

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

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