integral_const — Mathlib

English

For a constant simple function constant function y, its Bochner integral equals μ.real(univ) times y.

Русский

Для константной простой функции y интеграл Бо́хнера равен μ.real(всё множество) × y.

LaTeX

$$$$ (\\mathrm{const}\\; \\alpha\\; y)_{\\text{integral}}\\; \\mu = \\mu_{\\mathbb{R}}(\\mathrm{univ}) \\cdot y $$$$

Lean4

@[simp]
theorem integral_const {m : MeasurableSpace α} (μ : Measure α) (y : F) : (const α y).integral μ = μ.real univ • y := by
  classical
    calc
    (const α y).integral μ = ∑ z ∈ { y }, μ.real (const α y ⁻¹' { z }) • z :=
      integral_eq_sum_of_subset <| (filter_subset _ _).trans (range_const_subset _ _)
    _ = μ.real univ • y := by simp [Set.preimage]

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