integral_indicator_const — Mathlib

English

Let e ∈ E and s ⊆ X be a measurable set. Then the Bochner integral over X of the function x ↦ s.indicator (fun _ => e) x equals μ.real s times e.

Русский

Пусть e ∈ E и s ⊆ X измеримо. Тогда интеграл Бо́хнера по области X функции x ↦ s.indicator (константа e) равен μ.real(s) умножить на e.

LaTeX

$$$$ \\int_X \\mathbf{1}_s(x) \\; e \\, d\\mu(x) = \\mu_{\\mathbb{R}}(s) \\; e $$$$

Lean4

@[simp]
theorem integral_indicator_const [CompleteSpace E] (e : E) ⦃s : Set X⦄ (s_meas : MeasurableSet s) :
    ∫ x : X, s.indicator (fun _ : X => e) x ∂μ = μ.real s • e := by rw [integral_indicator s_meas, ← setIntegral_const]

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