setLIntegral_eq_const — Mathlib

English

For a measurable f, the integral over the level set {x | f(x)=r} equals r times the measure of that level set.

Русский

Для измеримой f интеграл по множество {x | f(x)=r} равен r умножить на меру этого множества.

LaTeX

$$$$ \\int^-_{x \\in {x | f(x)=r}} f(x) \\, d\\mu = r \\cdot \\mu\\{x : f(x)=r\\}. $$$$

Lean4

theorem setLIntegral_eq_const {f : α → ℝ≥0∞} (hf : Measurable f) (r : ℝ≥0∞) :
    ∫⁻ x in {x | f x = r}, f x ∂μ = r * μ {x | f x = r} :=
  by
  have : ∀ x ∈ {x | f x = r}, f x = r := fun _ hx => hx
  rw [setLIntegral_congr_fun _ this]
  · rw [lintegral_const, Measure.restrict_apply MeasurableSet.univ, Set.univ_inter]
  · exact hf (measurableSet_singleton r)

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