English
For a scalar c (in extended nonnegative reals), the integral with respect to c·μ scales by c: ∫ f d(c·μ) = c.toReal · ∫ f dμ.
Русский
Для скаляра c из ⊤-полных чисел, интеграл по мере c·μ масштабируется: ∫ f d(c·μ) = c.toReal · ∫ f dμ.
LaTeX
$$$$\int x, f x \partial(c \cdot \mu) = c^{\mathrm{toReal}} \cdot \int x, f x \partial\mu.$$$$
Lean4
@[simp]
theorem integral_smul_measure (f : α → G) (c : ℝ≥0∞) : ∫ x, f x ∂c • μ = c.toReal • ∫ x, f x ∂μ :=
by
by_cases hG : CompleteSpace G; swap
·
simp [integral, hG]
-- First we consider the “degenerate” case `c = ∞`
rcases eq_or_ne c ∞ with (rfl | hc)
·
rw [ENNReal.toReal_top, zero_smul, integral_eq_setToFun, setToFun_top_smul_measure]
-- Main case: `c ≠ ∞`
simp_rw [integral_eq_setToFun, ← setToFun_smul_left]
have hdfma : DominatedFinMeasAdditive μ (weightedSMul (c • μ) : Set α → G →L[ℝ] G) c.toReal :=
mul_one c.toReal ▸ (dominatedFinMeasAdditive_weightedSMul (c • μ)).of_smul_measure hc
have hdfma_smul := dominatedFinMeasAdditive_weightedSMul (F := G) (c • μ)
rw [← setToFun_congr_smul_measure c hc hdfma hdfma_smul f]
exact setToFun_congr_left' _ _ (fun s _ _ => weightedSMul_smul_measure μ c) f
