A positive-definite form is the standard one in suitable coordinates

Let S be a symmetric operator on a finite-dimensional inner product space V whose associated Hermitian form ⟪S v, w⟫ is positive definite. This file produces a linear automorphism of V along which that form pulls back to the inner product V already carries:

TauCeti.exists_continuousLinearEquiv_inner_map_map gives e : V ≃L[𝕜] V with ⟪S (e x), e y⟫ = ⟪x, y⟫ for all x and y.

Equivalently e is an isometry from (V, ⟪·,·⟫) onto (V, ⟪S ·, ·⟫), so its inverse is the operator usually written S ^ (1 / 2); the construction here avoids building an operator square root by scaling an orthonormal eigenbasis of S instead. The eigenvalues of S are positive because the form is definite, so dividing the i-th eigenvector by √(λ i) produces a basis that is orthonormal for the form, and e is the map carrying the eigenbasis to it.

Main statements

• TauCeti.exists_continuousLinearEquiv_inner_map_map: a positive-definite symmetric operator's form becomes the standard inner product after a change of coordinates.

Only the existence of e is exported, since it depends on a choice of eigenbasis. The operator is taken continuous and the change of coordinates produced is a continuous linear equivalence; on a finite-dimensional space that is no restriction either way, and it is the form the consumer both supplies and wants.

The intended consumer is Weyl's unitarian trick: applied to the Gram operator of the Haar-averaged inner product of a representation of a compact group, this is what turns the invariant form into an honest unitary structure, in TauCeti/RepresentationTheory/Compact/UnitaryModel.lean.

theorem TauCeti.exists_continuousLinearEquiv_inner_map_map {𝕜 : Type u_1} {V : Type u_2} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [FiniteDimensional 𝕜 V] (S : V →L[𝕜] V) (hsymm : (↑S).IsSymmetric) (hpos : ∀ (v : V), v ≠ 0 → 0 < RCLike.re (inner 𝕜 (S v) v)) : ∃ (e : V ≃L[𝕜] V), ∀ (x y : V), inner 𝕜 (S (e x)) (e y) = inner 𝕜 x y

A positive-definite form is standard in suitable coordinates. If S is a symmetric operator on a finite-dimensional inner product space whose form ⟪S ·, ·⟫ is positive definite, then there is a continuous linear automorphism e with ⟪S (e x), e y⟫ = ⟪x, y⟫.

The automorphism is the inverse of the square root of S, built without any operator functional calculus: an orthonormal eigenbasis b of S has positive eigenvalues λ i, so the vectors (√(λ i))⁻¹ • b i are orthonormal for the form ⟪S ·, ·⟫, and e is the automorphism carrying b i to them.