Documentation

LeanPool.MatrixMultiplicationAllFields.LinearAlgebra.MatrixMultiplication.AuxiliarySeparation.Determinant.Bounds

Degree bounds for the binary determinant relation #

The polynomial identity A + X * B = 0 forces one extra degree of cancellation: if A has degree less than e + 1, then B has degree less than e.

source
theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.degree_lt_of_diagonal_eq_zero {R : Type u_1} [CommRing R] {e : ℕ} {A B : Polynomial R} (hA : A.degree < ↑(e + 1)) (h : A + Polynomial.X * B = 0) :
B.degree < ↑e

A degree bound on the first component of a diagonal relation bounds the second component by one degree less.

source
theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.degree_neg_X_mul_lt {R : Type u_1} [CommRing R] {e : ℕ} {q : Polynomial R} (hq : q.degree < ↑e) :
(-(Polynomial.X * q)).degree < ↑(e + 1)

Multiplication by -X increases the strict degree bound by at most one.

source
theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.determinant_degree_bounds {R : Type u_1} [CommRing R] {e : ℕ} {q : Polynomial R} (hq : q.degree < ↑e) :
(-(Polynomial.X * q)).degree < ↑(e + 1) ∧ q.degree < ↑(e + 1)

The determinant generator preserves the two component degree bounds.

source
@[reducible, inline]
abbrev MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.BoundedPair (R : Type u_2) [CommRing R] (e : ℕ) :
Type u_2

Pairs representing forms of bidegree (e, 1).

Equations
Instances For
    source
    noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.diagonal {R : Type u_1} [CommRing R] (e : ℕ) :
    BoundedPair R e →ₗ[R] Polynomial R

    Diagonal substitution on the space with the prescribed degree bounds.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.negativeShift {R : Type u_1} [CommRing R] (e : ℕ) :
      ↥(Polynomial.degreeLT R e) →ₗ[R] ↥(Polynomial.degreeLT R (e + 1))

      The first component of multiplication by uw-vs.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.widen {R : Type u_1} [CommRing R] (e : ℕ) :
        ↥(Polynomial.degreeLT R e) →ₗ[R] ↥(Polynomial.degreeLT R (e + 1))

        Increase the allowed degree bound by one.

        Equations
        Instances For
          source
          @[simp]
          theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.widen_coe {R : Type u_1} [CommRing R] (e : ℕ) (q : ↥(Polynomial.degreeLT R e)) :
          ↑((widen e) q) = ↑q
          source
          noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.determinant {R : Type u_1} [CommRing R] (e : ℕ) :
          ↥(Polynomial.degreeLT R e) →ₗ[R] BoundedPair R e

          Multiplication by uw-vs lands in the bounded pair space.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.diagonal_apply {R : Type u_1} [CommRing R] (e : ℕ) (p : BoundedPair R e) :
            (diagonal e) p = ↑p.1 + Polynomial.X * ↑p.2
            source
            @[simp]
            theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.determinant_fst {R : Type u_1} [CommRing R] (e : ℕ) (q : ↥(Polynomial.degreeLT R e)) :
            ↑((determinant e) q).1 = -Polynomial.X * ↑q
            source
            @[simp]
            theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.determinant_snd {R : Type u_1} [CommRing R] (e : ℕ) (q : ↥(Polynomial.degreeLT R e)) :
            ↑((determinant e) q).2 = ↑q
            source
            theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.diagonal_determinant {R : Type u_1} [CommRing R] (e : ℕ) (q : ↥(Polynomial.degreeLT R e)) :
            (diagonal e) ((determinant e) q) = 0
            source
            noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.toKernel {R : Type u_1} [CommRing R] (e : ℕ) :
            ↥(Polynomial.degreeLT R e) →ₗ[R] ↥(diagonal e).ker

            The determinant map with codomain restricted to the diagonal kernel.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[simp]
              theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.toKernel_coe {R : Type u_1} [CommRing R] (e : ℕ) (q : ↥(Polynomial.degreeLT R e)) :
              ↑((toKernel e) q) = (determinant e) q
              source
              theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.toKernel_bijective {R : Type u_1} [CommRing R] (e : ℕ) :
              Function.Bijective ⇑(toKernel e)
              source
              noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.kernelEquiv {R : Type u_1} [CommRing R] (e : ℕ) :
              ↥(Polynomial.degreeLT R e) ≃ₗ[R] ↥(diagonal e).ker

              The bounded determinant kernel has exactly the degree-< e polynomials as its parameters, including at e = 0.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.finrank_kernel (K : Type u_2) [Field K] (e : ℕ) :
                Module.finrank K ↥(diagonal e).ker = e

                The finite determinant kernel has dimension e.

                source
                theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.degree_diagonal_lt {R : Type u_1} [CommRing R] (e : ℕ) (p : BoundedPair R e) :
                ((diagonal e) p).degree < ↑(e + 2)

                The diagonal has the next larger degree bound.

                source
                noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.diagonalToDegreeLT {R : Type u_1} [CommRing R] (e : ℕ) :
                BoundedPair R e →ₗ[R] ↥(Polynomial.degreeLT R (e + 2))

                Diagonal substitution with both the domain and codomain degree bounded.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  @[simp]
                  theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.diagonalToDegreeLT_coe {R : Type u_1} [CommRing R] (e : ℕ) (p : BoundedPair R e) :
                  ↑((diagonalToDegreeLT e) p) = (diagonal e) p
                  source
                  theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.degree_divX_lt {R : Type u_1} [CommRing R] {e : ℕ} {p : Polynomial R} (hp : p.degree < ↑(e + 1)) :
                  p.divX.degree < ↑e

                  Removing the constant coefficient lowers the strict degree bound by one.

                  source
                  theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.diagonalToDegreeLT_surjective {R : Type u_1} [CommRing R] (e : ℕ) :
                  Function.Surjective ⇑(diagonalToDegreeLT e)

                  Every polynomial of the output degree is a diagonal restriction of a bounded pair.

                  source
                  @[simp]
                  theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.ker_diagonalToDegreeLT {R : Type u_1} [CommRing R] (e : ℕ) :
                  (diagonalToDegreeLT e).ker = (diagonal e).ker