const_mul_lintegral — Mathlib

English

For a simple function f and a constant x, (const α x * f).lintegral μ = x * f.lintegral μ.

Русский

Для простой функции f и константы x: (const α x * f).lintegral μ = x * f.lintegral μ.

LaTeX

$$$ (const\ α\ x * f).lintegral\ μ = x * f.lintegral\ μ $$$

Lean4

theorem const_mul_lintegral (f : α →ₛ ℝ≥0∞) (x : ℝ≥0∞) : (const α x * f).lintegral μ = x * f.lintegral μ :=
  calc
    (f.map fun a => x * a).lintegral μ = ∑ r ∈ f.range, x * r * μ (f ⁻¹' { r }) := map_lintegral _ _
    _ = x * ∑ r ∈ f.range, r * μ (f ⁻¹' { r }) := by simp_rw [Finset.mul_sum, mul_assoc]

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