theorem Orthogonalization.FinDim.inner_apply_eq_of_adjoint_comp_eq {H : Type u_1} {K : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] [NormedAddCommGroup K] [InnerProductSpace ℂ K] [FiniteDimensional ℂ K] (T : H →L[ℂ] K) (s : H →L[ℂ] H) (hT : ContinuousLinearMap.adjoint T ∘SL T = s ∘SL s) (v w : H) : inner ℂ (T v) (T w) = inner ℂ ((s ∘SL s) v) w

‖T v‖² = ⟪s² v, v⟫ when T* T = s * s.

theorem Orthogonalization.FinDim.exists_isometry_completion {H : Type u_1} {K : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] [NormedAddCommGroup K] [InnerProductSpace ℂ K] [FiniteDimensional ℂ K] (T : H →L[ℂ] K) (s : H →L[ℂ] H) (hs : IsSelfAdjoint s) (hs0 : 0 ≤ s) (hT : ContinuousLinearMap.adjoint T ∘SL T = s ∘SL s) (L : Submodule ℂ K) (hTL : (↑T).range ≤ L) (hL : Module.finrank ℂ ↥L = Module.finrank ℂ H) : ∃ (u : H →L[ℂ] K), ContinuousLinearMap.adjoint u ∘SL u = 1 ∧ u ∘SL ContinuousLinearMap.adjoint u = L.starProjection ∧ u ∘SL s = T

Isometric completion.