English
For r ∈ ℝ≥0∞ and Measurable f, the linearity holds: ∫⁻ r * f = r * ∫⁻ f.
Русский
Для константы r ∈ ℝ≥0∞ и измеримой f выполняется линейность: ∫⁻ r f = r ∫⁻ f.
LaTeX
$$$\forall r : \mathbb{R}_{\ge 0}^{\infty},\; \forall f : \alpha \to \mathbb{R}_{\ge 0}^{\infty},\; \mathrm{Measurable}(f) \Rightarrow ∫^- a, r \cdot f a \partial\mu = r \cdot ∫^- a, f a \partial\mu$$$
Lean4
@[simp]
theorem lintegral_const_mul (r : ℝ≥0∞) {f : α → ℝ≥0∞} (hf : Measurable f) : ∫⁻ a, r * f a ∂μ = r * ∫⁻ a, f a ∂μ :=
calc
∫⁻ a, r * f a ∂μ = ∫⁻ a, ⨆ n, (const α r * eapprox f n) a ∂μ :=
by
congr
funext a
rw [← iSup_eapprox_apply hf, ENNReal.mul_iSup]
simp
_ = ⨆ n, r * (eapprox f n).lintegral μ := by
rw [lintegral_iSup]
· congr
funext n
rw [← SimpleFunc.const_mul_lintegral, ← SimpleFunc.lintegral_eq_lintegral]
· intro n
exact SimpleFunc.measurable _
· intro i j h a
exact mul_le_mul_left' (monotone_eapprox _ h _) _
_ = r * ∫⁻ a, f a ∂μ := by rw [← ENNReal.mul_iSup, lintegral_eq_iSup_eapprox_lintegral hf]
