integral_smul — Mathlib

English

If the scalar field 𝕜 acts on E, then the integral of r · f is r times the integral of f.

Русский

Если 𝕜 действует на E, то интеграл от r · f равен r умноженному на интеграл от f.

LaTeX

$$$\int_{a}^{b} (r \cdot f(x)) \, dμ = r \cdot \int_{a}^{b} f(x) \, dμ$$$

Lean4

/-- Compatibility with scalar multiplication. Note this assumes `𝕜` is a division ring in order to
ensure that for `c ≠ 0`, `c • f` is integrable iff `f` is. For scalar multiplication by more
general rings assuming integrability, see `IntervalIntegrable.integral_smul`. -/
@[simp]
nonrec theorem integral_smul [NormedDivisionRing 𝕜] [Module 𝕜 E] [NormSMulClass 𝕜 E] [SMulCommClass ℝ 𝕜 E] (r : 𝕜)
    (f : ℝ → E) : ∫ x in a..b, r • f x ∂μ = r • ∫ x in a..b, f x ∂μ := by
  simp only [intervalIntegral, integral_smul, smul_sub]

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