Documentation

TauCeti.LinearAlgebra.Matrix.ToQuadraticForm

Basic rules for the quadratic form of a matrix #

Elementary rules for Mathlib's Matrix.toQuadraticForm' — evaluation, its behaviour under scaling, negation, transposition and on diagonal matrices — together with the isometries of the attached forms induced by congruence, block diagonals and reindexing. They are kept apart from the signature theory so that consumers needing only these rules do not import it.

Main definitions #

Main results #

source
theorem Matrix.toQuadraticForm'_apply {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (A : Matrix ι ι R) (x : ι → R) :
A.toQuadraticForm' x = x ⬝ᵥ A.mulVec x

The quadratic form attached to a matrix, evaluated at a vector.

source
@[simp]
theorem Matrix.toQuadraticForm'_smul {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (c : R) (A : Matrix ι ι R) :
(c • A).toQuadraticForm' = c • A.toQuadraticForm'

Scaling a matrix scales its quadratic form.

source
theorem Matrix.toQuadraticForm'_transpose {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (A : Matrix ι ι R) :
A.transpose.toQuadraticForm' = A.toQuadraticForm'

A matrix and its transpose carry the same quadratic form.

source
theorem Matrix.toQuadraticForm'_add_transpose {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (A : Matrix ι ι R) :
(A + A.transpose).toQuadraticForm' = 2 • A.toQuadraticForm'

The quadratic form of A + Aᵀ is twice the quadratic form of A.

source
@[simp]
theorem Matrix.toQuadraticForm'_neg {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (A : Matrix ι ι R) :
(-A).toQuadraticForm' = -A.toQuadraticForm'

The quadratic form of -A is the negative of the quadratic form of A.

source
theorem Matrix.toQuadraticForm'_diagonal {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (d : ι → R) :
(diagonal d).toQuadraticForm' = QuadraticMap.weightedSumSquares R d

The quadratic form of a diagonal matrix is the corresponding weighted sum of squares.

source
noncomputable def Matrix.isometryEquivCongr {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {P : Matrix ι ι R} (hP : IsUnit P.det) (A : Matrix ι ι R) :
QuadraticMap.IsometryEquiv (P * A * P.transpose).toQuadraticForm' A.toQuadraticForm'

Congruence by a matrix with unit determinant is an isometry of the attached quadratic forms.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Matrix.isometryEquivFromBlocks {R : Type u_1} [CommRing R] {ι : Type u_2} {κ : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] (A : Matrix ι ι R) (B : Matrix κ κ R) :
    QuadraticMap.IsometryEquiv (fromBlocks A 0 0 B).toQuadraticForm' (QuadraticMap.prod A.toQuadraticForm' B.toQuadraticForm')

    Splitting the coordinates of a block-diagonal matrix is an isometry onto the orthogonal product of the quadratic forms of the two blocks.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Matrix.isometryEquivReindex {R : Type u_1} [CommRing R] {ι : Type u_2} {κ : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] (e : ι ≃ κ) (A : Matrix ι ι R) :
      QuadraticMap.IsometryEquiv ((reindex e e) A).toQuadraticForm' A.toQuadraticForm'

      Reindexing the rows and columns of a matrix along the same equivalence only transports the coordinates of its quadratic form.

      Equations
      Instances For