Bounds.lean`

24 declarations, 0 contain sorry, 0 declared as axioms

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.

theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.degree_lt_of_diagonal_eq_zero line 24
Source documentation
A degree bound on the first component of a diagonal relation bounds the second component by one degree less.
```
theorem degree_lt_of_diagonal_eq_zero {e : ℕ} {A B : R[X]}
    (hA : A.degree < (e + 1 : ℕ)) (h : A + X * B = 0) :
    B.degree < e := by
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.degree_neg_X_mul_lt line 34
Source documentation
Multiplication by -X increases the strict degree bound by at most one.
```
theorem degree_neg_X_mul_lt {e : ℕ} {q : R[X]} (hq : q.degree < e) :
    (-(X * q) : R[X]).degree < (e + 1 : ℕ) := by
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.determinant_degree_bounds line 43
Source documentation
The determinant generator preserves the two component degree bounds.
```
theorem determinant_degree_bounds {e : ℕ} {q : R[X]} (hq : q.degree < e) :
    (-(X * q) : R[X]).degree < (e + 1 : ℕ) ∧ q.degree < (e + 1 : ℕ) := by
…
```
abbrev OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.BoundedPair line 49
Source documentation
Pairs representing forms of bidegree (e, 1).
```
abbrev BoundedPair (R : Type*) [CommRing R] (e : ℕ) :=
…
```
def OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.diagonal line 53
Source documentation
Diagonal substitution on the space with the prescribed degree bounds.
```
def diagonal (e : ℕ) : BoundedPair R e →ₗ[R] R[X] where
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.BoundedPair
def OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.negativeShift line 59
Source documentation
The first component of multiplication by uw-vs.
```
def negativeShift (e : ℕ) : degreeLT R e →ₗ[R] degreeLT R (e + 1) :=
…
```
def OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.widen line 66
Source documentation
Increase the allowed degree bound by one.
```
def widen (e : ℕ) : degreeLT R e →ₗ[R] degreeLT R (e + 1) :=
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.widen_coe line 69
def OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.determinant line 74
Source documentation
Multiplication by uw-vs lands in the bounded pair space.
```
def determinant (e : ℕ) : degreeLT R e →ₗ[R] BoundedPair R e where
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.BoundedPair
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.diagonal_apply line 79
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.determinant_fst line 82
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.determinant_snd line 85
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.diagonal_determinant line 90
def OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.toKernel line 95
Source documentation
The determinant map with codomain restricted to the diagonal kernel.
```
def toKernel (e : ℕ) : degreeLT R e →ₗ[R] LinearMap.ker (diagonal (R := R) e) :=
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.diagonal
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.toKernel_coe line 98
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.toKernel_bijective line 101
def OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.kernelEquiv line 123
Source documentation
The bounded determinant kernel has exactly the degree-< e polynomials as its parameters, including at e = 0.
```
def kernelEquiv (e : ℕ) : degreeLT R e ≃ₗ[R] LinearMap.ker (diagonal (R := R) e) :=
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.diagonal
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.finrank_kernel line 127
Source documentation
The finite determinant kernel has dimension e.
```
theorem finrank_kernel (K : Type*) [Field K] (e : ℕ) :
    Module.finrank K (LinearMap.ker (diagonal (R := K) e)) = e := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.diagonal
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.degree_diagonal_lt line 133
Source documentation
The diagonal has the next larger degree bound.
```
theorem degree_diagonal_lt (e : ℕ) (p : BoundedPair R e) :
    (diagonal e p).degree < (e + 2 : ℕ) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.BoundedPair, OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.diagonal
def OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.diagonalToDegreeLT line 143
Source documentation
Diagonal substitution with both the domain and codomain degree bounded.
```
def diagonalToDegreeLT (e : ℕ) : BoundedPair R e →ₗ[R] degreeLT R (e + 2) :=
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.BoundedPair
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.diagonalToDegreeLT_coe line 146
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.degree_divX_lt line 150
Source documentation
Removing the constant coefficient lowers the strict degree bound by one.
```
theorem degree_divX_lt {e : ℕ} {p : R[X]} (hp : p.degree < (e + 1 : ℕ)) :
    p.divX.degree < e := by
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.diagonalToDegreeLT_surjective line 159
Source documentation
Every polynomial of the output degree is a diagonal restriction of a bounded pair.
```
theorem diagonalToDegreeLT_surjective (e : ℕ) :
    Function.Surjective (diagonalToDegreeLT (R := R) e) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.diagonalToDegreeLT
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBounds.ker_diagonalToDegreeLT line 171