norm_weightedSMul_le — Mathlib

English

The family of weightedSMul operators is dominated FinMeasAdditive with domination constant 1, i.e., μ defines a dominated additive structure for weighted smuls.

Русский

Семейство weightedSMul образует доминированную FinMeasAdditive структуру с константой доминирования 1.

LaTeX

$$DominatedFinMeasAdditive μ (weightedSMul μ) 1$$

Lean4

theorem norm_weightedSMul_le (s : Set α) : ‖(weightedSMul μ s : F →L[ℝ] F)‖ ≤ μ.real s :=
  calc
    ‖(weightedSMul μ s : F →L[ℝ] F)‖ = ‖μ.real s‖ * ‖ContinuousLinearMap.id ℝ F‖ :=
      norm_smul (μ.real s) (ContinuousLinearMap.id ℝ F)
    _ ≤ ‖μ.real s‖ := ((mul_le_mul_of_nonneg_left norm_id_le (norm_nonneg _)).trans (mul_one _).le)
    _ = abs μ.real s := (Real.norm_eq_abs _)
    _ = μ.real s := abs_eq_self.mpr ENNReal.toReal_nonneg

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