English
The core provides a normed additive commutative group structure via the inner-product-based norm.
Русский
Ядро задаёт нормированную аддитивно-коммутативную группу через норму, заданную через скалярное произведение.
LaTeX
$$NormedAddCommGroup from core with norm ∥x∥ = √(Re ⟪x,x⟫)$$
Lean4
/-- Given an `InnerProductSpace.Core` structure on a space with a topology, one can use it to turn
the space into an inner product space. The `NormedAddCommGroup` structure is expected
to already be defined with `InnerProductSpace.ofCore.toNormedAddCommGroupOfTopology`. -/
def ofCoreOfTopology [AddCommGroup F] [hF : Module 𝕜 F] [TopologicalSpace F] [IsTopologicalAddGroup F]
[ContinuousConstSMul 𝕜 F] (cd : InnerProductSpace.Core 𝕜 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';
InnerProductSpace 𝕜 F :=
letI : NormedAddCommGroup F := cd.toNormedAddCommGroupOfTopology h h'
letI : NormedSpace 𝕜 F := cd.toNormedSpaceOfTopology h h'
{ cd with
norm_sq_eq_re_inner := fun x => by
have h₁ : ‖x‖ ^ 2 = √(re (cd.inner x x)) ^ 2 := rfl
have h₂ : 0 ≤ re (cd.inner x x) := InnerProductSpace.Core.inner_self_nonneg
simp [h₁, sq_sqrt, h₂] }
