prod_norm_le_norm_add — Mathlib

English

There is a norm on the product C*-module given by the Euclidean combination of the component norms.

Русский

Существует норма на произведении C*-модулей, задаваемая евклидовой комбинацией норм компонент.

LaTeX

$$$\\text{instNormProd}: \\| (x,y) \\| = \\sqrt{\\|x\\|^{2} + \\|y\\|^{2}}$$$

Lean4

theorem prod_norm_le_norm_add (x : C⋆ᵐᵒᵈ(A, E × F)) : ‖x‖ ≤ ‖x.1‖ + ‖x.2‖ :=
  by
  refine abs_le_of_sq_le_sq' ?_ (by positivity) |>.2
  calc
    ‖x‖ ^ 2 ≤ ‖⟪x.1, x.1⟫_A‖ + ‖⟪x.2, x.2⟫_A‖ := prod_norm_sq x ▸ norm_add_le _ _
    _ = ‖x.1‖ ^ 2 + 0 + ‖x.2‖ ^ 2 := by simp [norm_sq_eq A]
    _ ≤ ‖x.1‖ ^ 2 + 2 * ‖x.1‖ * ‖x.2‖ + ‖x.2‖ ^ 2 := by gcongr; positivity
    _ = (‖x.1‖ + ‖x.2‖) ^ 2 := by ring

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