Rectangular.lean`

20 declarations, 0 contain sorry, 0 declared as axioms

def OAI.RationalHitting.Rectangular.blockEval line 13
Source documentation
The ordinary Kronecker evaluation, with the two vector indices curried in reverse order. This is only a coordinate convention.
```
def blockEval {w q e : ℕ} (A : Fin w → Matrix (Fin q) (Fin q) F)
    (X : Fin w → Matrix (Fin e) (Fin e) F) :
    (Fin e → Fin q → F) →ₗ[F] (Fin e → Fin q → F) where
…
```
lemma OAI.RationalHitting.Rectangular.no_shrunk_subspace line 30

lemma OAI.RationalHitting.Rectangular.blockEval_injective_of_leftInverse line 76

Source documentation

Full-rank blocks preserve the dimension of a common input subspace; this form avoids any unwarranted specialization of Laurent-series coefficients.

lemma blockEval_injective_of_leftInverse {w q e : ℕ}
    (A : Fin w → Matrix (Fin q) (Fin q) F)
    (X : Fin w → Matrix (Fin e) (Fin e) F)
    (J : (Fin e → Fin q → F) →ₗ[F] (Fin e → Fin q → F))
    (hJ : J.comp (blockEval A X) = LinearMap.id) :
    Function.Injective (blockEval A X) := by
…

Mentions: OAI.RationalHitting.Rectangular.blockEval

def OAI.RationalHitting.Rectangular.componentSpace line 89
def OAI.RationalHitting.Rectangular.component line 92
def OAI.RationalHitting.Rectangular.coefficientMatrix line 95
lemma OAI.RationalHitting.Rectangular.span_component_top line 99
lemma OAI.RationalHitting.Rectangular.rank_coefficientMatrix line 105
lemma OAI.RationalHitting.Rectangular.coefficientMatrix_expansion line 117
def OAI.RationalHitting.Rectangular.imageCombination line 124
Source documentation
The output map of the wk possible component images.
```
def imageCombination {w k : ℕ} (T : Fin w → P →ₗ[F] Q) (u : Fin k → P) :
    (Fin w × Fin k → F) →ₗ[F] Q :=
…
```

def OAI.RationalHitting.Rectangular.concatMatrix line 129

Source documentation

The concatenated coefficient matrix.

def concatMatrix {w q k : ℕ} (A : Fin w → Matrix (Fin q) (Fin q) F)
    (P : Matrix (Fin q) (Fin k) F) : Matrix (Fin q) (Fin w × Fin k) F :=
…

lemma OAI.RationalHitting.Rectangular.concat_row_relation line 133
lemma OAI.RationalHitting.Rectangular.rank_concat_lt line 149
lemma OAI.RationalHitting.Rectangular.coefficient_image_le_concat line 172
lemma OAI.RationalHitting.Rectangular.component_image_le_range line 184
theorem OAI.RationalHitting.Rectangular.kernel_impossible line 202
Source documentation
A kernel vector with sufficiently expansive component span contradicts any invertible block evaluation of the same coefficient matrices.
```
theorem kernel_impossible {w q k e : ℕ} (hw : 1 ≤ w) (he : 0 < e)
    (A : Fin w → Matrix (Fin q) (Fin q) F) (T : Fin w → P →ₗ[F] Q)
    (X : Fin w → Matrix (Fin e) (Fin e) F)
    (hX : Function.Injective (blockEval A X))
    (f : Fin q → P) (b : Basis (Fin k) F (componentSpace (F := F) f))
…
```
Mentions: OAI.RationalHitting.Rectangular.blockEval, OAI.RationalHitting.Rectangular.componentSpace
def OAI.RationalHitting.Rectangular.blockMatrix line 226
lemma OAI.RationalHitting.Rectangular.blockMatrix_mulVec line 230
lemma OAI.RationalHitting.Rectangular.blockEval_injective_of_isUnit line 251

theorem OAI.RationalHitting.RectangularExpansion.rectangular_kernel_zero line 278

Source documentation

The rectangular Taylor tests have no nonzero kernel component family when the same coefficients have an invertible matrix witness.

theorem rectangular_kernel_zero (w B M N q e : ℕ) (hw : 1 ≤ w) (hN : 1 ≤ N)
    (hMN : M = N + 2*w^3*B) (hq : q ≤ B) (he : 0 < e)
    (points : Fin w → K) (hp : Function.Injective points)
    (A : Fin w → Matrix (Fin q) (Fin q) (F K))
    (X : Fin w → Matrix (Fin e) (Fin e) (F K))
    (hX : Function.Injective (blockEval A X))
    (f : Fin q → Fin M → F K)
    (hf : ∀ α j, N ≤ j.val → f α j = 0)
    (hker : ∀ α, ∑ i, ∑ γ, A i α γ • testMap M (points i) (f γ) = 0) : f = 0 := by
…