Orthogonality

DefinitionOrthogonal elements#

A set of vectors v is orthogonal with respect to some bilinear form B if and only if for all i ≠ j, B (v i) (v j) = 0.

LinearMap.BilinForm.iIsOrtho.{w, u_1, u_2} {R : Type u_1} {M : Type u_2} [CommSemiring R]
  [AddCommMonoid M] [_root_.Module R M] {n : Type w} (B : LinearMap.BilinForm R M) (v : n → M) :
  Prop
Sources
MathlibLinearMap.BilinForm.iIsOrtho
Uses 1
Statement usesBilinear form

DefinitionAdjoint endomorphism#

Given the nondegenerate bilinear form B and the linear map φ, leftAdjointOfNondegenerate provides the left adjoint of φ with respect to B. The lemma proving this property is BilinForm.isAdjointPairLeftAdjointOfNondegenerate.

LinearMap.BilinForm.leftAdjointOfNondegenerate.{u_5, u_6} {V : Type u_5} {K : Type u_6} [Field K]
  [AddCommGroup V] [_root_.Module K V] [FiniteDimensional K V] (B : LinearMap.BilinForm K V)
  (b : B.Nondegenerate) (φ : V →ₗ[K] V) : V →ₗ[K] V
Sources
MathlibLinearMap.BilinForm.leftAdjointOfNondegenerate
Uses 8
Statement usesAssociative algebra over a commutative ring · Cardinal · Dual vector space · Field · Finite-dimensionality · Linear independence · Nondegenerate forms · Range of a linear map

TheoremSylvester's law of inertia (existence)#

Sylvester's law of inertia: A real quadratic form is equivalent to a weighted sum of squares with the weights being ±1 or 0.

QuadraticForm.equivalent_one_zero_neg_one_weighted_sum_squared.{u_2} {M : Type u_2} [AddCommGroup M]
  [_root_.Module ℝ M] [FiniteDimensional ℝ M] (Q : QuadraticForm ℝ M) :
  ∃ w,
    (∀ (i : Fin (Module.finrank ℝ M)), w i = -1 ∨ w i = 0 ∨ w i = 1) ∧
      QuadraticMap.Equivalent Q (QuadraticMap.weightedSumSquares ℝ w)
Sources
MathlibQuadraticForm.equivalent_one_zero_neg_one_weighted_sum_squared
Uses 12
Statement usesAssociative algebra over a commutative ring · Cardinal · Finite-dimensionality · Linear independence · Quadratic form · Real number
Proof usesCharacteristic zero · Field \(\R\) of real numbers · Invertible elements · Isomorphism with \(K^n\) · Order · Range of a linear map

TheoremSylvester's law of inertia (uniqueness)#

Uniqueness part of Sylvester's law of inertia (positive part): for any weighted sum of squares equivalent to Q, the number of strictly positive weights is equal to sigPos Q.

QuadraticForm.sigPos_of_equiv_weightedSumSquares.{u_2, u_4, u_5} {M : Type u_2} [AddCommGroup M]
  {𝕜 : Type u_4} [Field 𝕜] [LinearOrder 𝕜] [_root_.Module 𝕜 M] {Q : QuadraticForm 𝕜 M}
  {ι : Type u_5} [Fintype ι] {w : ι → 𝕜} [IsStrictOrderedRing 𝕜]
  (hQ : QuadraticMap.Equivalent Q (QuadraticMap.weightedSumSquares 𝕜 w)) :
  sigPos Q = {i | 0 < w i}.ncard
Sources
MathlibQuadraticForm.sigPos_of_equiv_weightedSumSquares
Uses 11
Statement usesAssociative algebra over a commutative ring · Cardinal · Field · Linear independence · Quadratic form · Rational number
Proof usesBasis · Euclidean domain · Finite-dimensionality · Ordered ring · Vector subspace

TheoremComplex classification#

A nondegenerate quadratic form on an algebraically closed field of characteristic not equal to 2 is equivalent to the sum of squares, i.e. weightedSumSquares with weight fun (i : ι) => 1.

QuadraticForm.equivalent_weightedSumSquares_of_isAlgClosed.{u_2, u_3} {K : Type u_2} [Field K]
  [IsAlgClosed K] [Invertible 2] {M : Type u_3} [AddCommGroup M] [_root_.Module K M]
  [FiniteDimensional K M] (Q : QuadraticForm K M)
  (hQ : LinearMap.SeparatingLeft (QuadraticMap.associated Q)) :
  QuadraticMap.Equivalent Q (QuadraticMap.weightedSumSquares K 1)
Sources
MathlibQuadraticForm.equivalent_weightedSumSquares_of_isAlgClosed
Uses 8
Statement usesAlgebraically closed field · Associative algebra over a commutative ring · Cardinal · Finite-dimensionality · Invertible elements · Linear independence · Polar form of a quadratic · Quadratic form

TheoremGram-Schmidt orthogonalisation#

Gram-Schmidt Orthogonalisation: gramSchmidt produces an orthogonal system of vectors.

InnerProductSpace.gramSchmidt_orthogonal.{u_1, u_2, u_3} (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜]
  [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [LinearOrder ι]
  [LocallyFiniteOrderBot ι] (f : ι → E) {a b : ι} (h₀ : a ≠ b) :
  inner 𝕜 (InnerProductSpace.gramSchmidt 𝕜 f a) (InnerProductSpace.gramSchmidt 𝕜 f b) = 0
Sources
MathlibInnerProductSpace.gramSchmidt_orthogonal
Uses 5
Statement usesFinite set · Generating sets · Orthogonal projection
Proof usesCompactness in terms of filters · Finite-dimensionality

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.