integral_indicator — Mathlib

English

If the indicator of a set S lies inside the interval [a,b], then the integral over [a,b] of the indicator times f equals the integral over S of f.

Русский

Если индикатор множества S накладывается на интервал [a,b], то интеграл индикатора × f по [a,b] равен интегралу по S.

LaTeX

$$$ \\int_{a}^{b} (\\mathbf{1}_{S}) f(x) \\, dμ = \\int_{S} f(x) \\, dμ $, при условии, что S \\subseteq [a,b].$$

Lean4

nonrec theorem integral_indicator {a₁ a₂ a₃ : ℝ} (h : a₂ ∈ Icc a₁ a₃) :
    ∫ x in a₁..a₃, indicator {x | x ≤ a₂} f x ∂μ = ∫ x in a₁..a₂, f x ∂μ :=
  by
  have : {x | x ≤ a₂} ∩ Ioc a₁ a₃ = Ioc a₁ a₂ := Iic_inter_Ioc_of_le h.2
  rw [integral_of_le h.1, integral_of_le (h.1.trans h.2), integral_indicator, Measure.restrict_restrict, this]
  · exact measurableSet_Iic
  all_goals apply measurableSet_Iic

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