English
From the core one obtains a normed space structure on F; the norm is induced by the inner product.
Русский
Из ядра получается норма пространства на F; норма задаётся через внутреннее произведение.
LaTeX
$$NormedSpace from core with norm defined by √(Re ⟪x,x⟫)$$
Lean4
/-- Normed space structure constructed from an `InnerProductSpace.Core` structure, adjusting the
topology to make sure it is defeq to an already existing topology. -/
@[reducible]
def toNormedSpaceOfTopology [tF : TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜 F]
(h : ContinuousAt (fun (v : F) ↦ cd.inner v v) 0) (h' : IsVonNBounded 𝕜 {v : F | re (cd.inner v v) < 1}) :
letI : NormedAddCommGroup F := cd.toNormedAddCommGroupOfTopology h h';
NormedSpace 𝕜 F :=
letI : NormedAddCommGroup F := cd.toNormedAddCommGroupOfTopology h h'
{
norm_smul_le r
x := by
rw [norm_eq_sqrt_re_inner, inner_smul_left, inner_smul_right, ← mul_assoc]
rw [RCLike.conj_mul, ← ofReal_pow, re_ofReal_mul, sqrt_mul, ← ofReal_normSq_eq_inner_self, ofReal_re]
· simp [sqrt_normSq_eq_norm]
· positivity }
