English
If the measure is scaled by a scalar c and a compatibility condition holds, the lintegral scales accordingly: f.lintegral(c • μ) = c • f.lintegral(μ).
Русский
Если мера масштабируется скаляром c и соблюдается совместимость, линеграль масштабируется: f.lintegral(c • μ) = c • f.lintegral(μ).
LaTeX
$$$f.lintegral(c \\cdot μ) = c \\cdot f.lintegral(μ)$$$
Lean4
theorem lintegral_smul {R : Type*} [SMul R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞] (f : α →ₛ ℝ≥0∞) (c : R) :
f.lintegral (c • μ) = c • f.lintegral μ := by simpa only [smul_one_smul] using (lintegralₗ f).map_smul (c • 1) μ