Theorems · Theorem · measure theory

MeasureTheory.integral_smul

∀ {α : Type u_1} {𝕜 : Type u_4} [inst : NormedDivisionRing 𝕜] {G : Type u_5} [inst_1 : NormedAddCommGroup G]
  [inst_2 : NormedSpace ℝ G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst_3 : Module 𝕜 G]
  [NormSMulClass 𝕜 G] [SMulCommClass ℝ 𝕜 G] (c : 𝕜) (f : α → G), ∫ (a : α), c • f a ∂μ = c • ∫ (a : α), f a ∂μ

The Bochner integral is linear. Note this requires 𝕜 to be a normed division ring, in order to ensure that for c ≠ 0, the function c • f is integrable iff f is. For an analogous statement for more general rings with an a priori integrability assumption on f, see MeasureTheory.Integrable.integral_smul.

Defined in

Mathlib.MeasureTheory.Integral.Bochner.Basic

Cited by

23 results in Mathlib

Foundations

Depth 252 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedDivisionRingNormedAddCommGroupNormedSpaceModuleNormSMulClassSMulCommClass