English
The core determines a SeminormedAddCommGroup structure with norm p(x) = sqrt(Re ⟪x,x⟫).
Русский
Ядро определяет структуру семиномормного добавочно-коммутативного группы с нормой p(x) = sqrt(Re ⟪x,x⟫).
LaTeX
$$$p(x) = \sqrt{\operatorname{Re}\langle x,x\rangle}$$$
Lean4
/-- Seminormed group structure constructed from a `PreInnerProductSpace.Core` structure -/
def toSeminormedAddCommGroup : SeminormedAddCommGroup F :=
AddGroupSeminorm.toSeminormedAddCommGroup
{ toFun := fun x => √(re ⟪x, x⟫)
map_zero' := by simp only [sqrt_zero, inner_zero_right, map_zero]
neg' := fun x => by simp only [inner_neg_left, neg_neg, inner_neg_right]
add_le' := fun x y => by
have h₁ : ‖⟪x, y⟫‖ ≤ ‖x‖ * ‖y‖ := norm_inner_le_norm _ _
have h₂ : re ⟪x, y⟫ ≤ ‖⟪x, y⟫‖ := re_le_norm _
have h₃ : re ⟪x, y⟫ ≤ ‖x‖ * ‖y‖ := h₂.trans h₁
have h₄ : re ⟪y, x⟫ ≤ ‖x‖ * ‖y‖ := by rwa [← inner_conj_symm, conj_re]
have : ‖x + y‖ * ‖x + y‖ ≤ (‖x‖ + ‖y‖) * (‖x‖ + ‖y‖) :=
by
simp only [← inner_self_eq_norm_mul_norm, inner_add_add_self, mul_add, mul_comm, map_add]
linarith
exact nonneg_le_nonneg_of_sq_le_sq (add_nonneg (sqrt_nonneg _) (sqrt_nonneg _)) this }
