English
For Measurable f, Measurable g, ∫⁻ f a * g a = (∫⁻ f a) * g a.
Русский
Для измеримой f и g выполняется: ∫⁻ f · g = (∫⁻ f) · g.
LaTeX
$$$\forall f : α \to \mathbb{R}_{\ge 0}^{\infty},\; \{g : α \to \mathbb{R}_{\ge 0}^{\infty}\} (hf : \mathrm{Measurable} f) \Rightarrow ∫^- a, f a \cdot r ∂μ = (∫^- a, f a ∂μ) \cdot r$$$
Lean4
theorem lintegral_const_mul' (r : ℝ≥0∞) (f : α → ℝ≥0∞) (hr : r ≠ ∞) : ∫⁻ a, r * f a ∂μ = r * ∫⁻ a, f a ∂μ :=
by
by_cases h : r = 0
· simp [h]
apply le_antisymm _ (lintegral_const_mul_le r f)
have rinv : r * r⁻¹ = 1 := ENNReal.mul_inv_cancel h hr
have rinv' : r⁻¹ * r = 1 := by
rw [mul_comm]
exact rinv
have := lintegral_const_mul_le (μ := μ) r⁻¹ fun x => r * f x
simp only [(mul_assoc _ _ _).symm, rinv'] at this
simpa [(mul_assoc _ _ _).symm, rinv] using mul_le_mul_left' this r
