English
Given an InnerProductSpace.Core structure on a space with a topology, one obtains an inner product space structure on the same space.
Русский
Дано ядро InnerProductSpace.Core, и при этом имеется топология; пространство приобретает структуру скалярного произведения.
LaTeX
$$InnerProductSpace from core (of topology)$$
Lean4
/-- Given an `InnerProductSpace.Core` structure on a space, 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.toNormedAddCommGroup`. -/
def ofCore [AddCommGroup F] [Module 𝕜 F] (cd : InnerProductSpace.Core 𝕜 F) : InnerProductSpace 𝕜 F :=
letI : NormedSpace 𝕜 F := InnerProductSpace.Core.toNormedSpace
{ 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₂] }
