withDensity_apply_le — Mathlib

English

For measurable s, the integral of f over s is bounded above by (μ.withDensity f)(s).

Русский

Для измеримого s интеграл f по μ ограничен сверху величиной (μ.withDensity f)(s).

LaTeX

$$$\int_{s} f \, d\mu \le (\mu\text{ withDensity } f)(s)$$$

Lean4

theorem withDensity_apply_le (f : α → ℝ≥0∞) (s : Set α) : ∫⁻ a in s, f a ∂μ ≤ μ.withDensity f s :=
  by
  let t := toMeasurable (μ.withDensity f) s
  calc
    ∫⁻ a in s, f a ∂μ ≤ ∫⁻ a in t, f a ∂μ := lintegral_mono_set (subset_toMeasurable (withDensity μ f) s)
    _ = μ.withDensity f t := (withDensity_apply f (measurableSet_toMeasurable (withDensity μ f) s)).symm
    _ = μ.withDensity f s := measure_toMeasurable s

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