smul — Mathlib

English

If c is nonzero, then FinMeasAdditive for μ after smul by c is equivalent to FinMeasAdditive for μ with scaled bound.

Русский

Если c ≠ 0, то FinMeasAdditive после умножения меры на c эквивалентно FinMeasAdditive для исходной меры с масштабированной границей.

LaTeX

$$of_smul_measure {c} (hc_ne_top) (hT) : FinMeasAdditive μ T (c.toReal * C)$$

Lean4

theorem smul [SeminormedAddGroup 𝕜] [DistribSMul 𝕜 β] [IsBoundedSMul 𝕜 β] (hT : DominatedFinMeasAdditive μ T C)
    (c : 𝕜) : DominatedFinMeasAdditive μ (fun s => c • T s) (‖c‖ * C) :=
  by
  refine ⟨hT.1.smul c, fun s hs hμs => (norm_smul_le _ _).trans ?_⟩
  rw [mul_assoc]
  exact mul_le_mul le_rfl (hT.2 s hs hμs) (norm_nonneg _) (norm_nonneg _)

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