lintegral_smul — Mathlib

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) μ

Похожие утверждения