inftyCStarRing — Mathlib

English

Under hp ≠ 0, for c ∈ 𝕜 and f ∈ Subtype of lp E p, the norm respects scaling exactly: ‖c • f‖ = ‖c‖ · ‖f‖.

Русский

При hp ≠ 0 и c ∈ 𝕜, f ∈ lpE(p) нормa масштаба верна строго: ‖c•f‖ = ‖c‖ · ‖f‖.

LaTeX

$$$\\|c \\cdot f\\| = \\|c\\| \\cdot \\|f\\|$$$

Lean4

instance inftyCStarRing [∀ i, CStarRing (B i)] : CStarRing (lp B ∞) where
  norm_mul_self_le
    f := by
    rw [← sq, ← Real.le_sqrt (norm_nonneg _) (norm_nonneg _)]
    refine lp.norm_le_of_forall_le ‖star f * f‖.sqrt_nonneg fun i => ?_
    rw [Real.le_sqrt (norm_nonneg _) (norm_nonneg _), sq, ← CStarRing.norm_star_mul_self]
    exact lp.norm_apply_le_norm ENNReal.top_ne_zero (star f * f) i

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