Bilinear forms

This file relates bilinar forms and matrices, and proves properties about real vector spaces with positive definite symmetric bilinear forms.

noncomputable def Coxeter.LinearMap.BilinForm.toMatrix {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {ι : Type u_3} (b : Module.Basis ι R M) : LinearMap.BilinForm R M ≃ₗ[R] Matrix ι ι R

Omits the Fintype and DecidableEq hypotheses from mathlib's version

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Coxeter.Matrix.toBilin {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {ι : Type u_3} (b : Module.Basis ι R M) : Matrix ι ι R ≃ₗ[R] LinearMap.BilinForm R M

Omits the Fintype and DecidableEq hypotheses from mathlib's version

Equations

• Coxeter.Matrix.toBilin b = (Coxeter.LinearMap.BilinForm.toMatrix b).symm

theorem Coxeter.Matrix.toBilin_single {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {ι : Type u_3} (b : Module.Basis ι R M) (B : Matrix ι ι R) (i j : ι) : (((toBilin b) B) (b i)) (b j) = B i j

Positive definite symmetric bilinear forms on real vector spaces

def Coxeter.Orthonormal {V : Type u_4} [AddCommGroup V] [Module ℝ V] {ι : Type u_5} (B : LinearMap.BilinForm ℝ V) (v : ι → V) : Prop

Equations

• Coxeter.Orthonormal B v = ((∀ (i : ι), (B (v i)) (v i) = 1) ∧ LinearMap.IsOrthoᵢ B v)

theorem Coxeter.exists_orthonormal_basis {V : Type u_4} [AddCommGroup V] [Module ℝ V] [FiniteDimensional ℝ V] (B : LinearMap.BilinForm ℝ V) (hB1 : B.IsSymm) (hB2 : B.IsNonneg) (hB3 : B.Nondegenerate) : ∃ (v : Module.Basis (Fin (Module.finrank ℝ V)) ℝ V), Orthonormal B ⇑v

A positive definite symmetric bilinear form on a finite dimensional real vector space has an orthonormal basis.

theorem Coxeter.sup_orthogonal_eq_top {V : Type u_4} [AddCommGroup V] [Module ℝ V] {W : Submodule ℝ V} [FiniteDimensional ℝ ↥W] (B : LinearMap.BilinForm ℝ V) (hB1 : B.IsSymm) (hB2 : (B.restrict W).IsNonneg) (hB3 : (B.restrict W).Nondegenerate) : W ⊔ W.orthogonalBilin B = ⊤

If $V$ is an arbitrary real vector space equipped with a positive definite symmetric bilinar form and $W$ is a finite dimensional subspace, then $V$ is a sum of $W$ and its orthogonal complement.