OAI/Computability/RationalHitting/PaddedRank.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RationalHitting.TestPolynomial.polynomialMap_single line 12
  2. lemma OAI.RationalHitting.TestPolynomial.taylor_matrix line 23
  3. lemma OAI.RationalHitting.TestPolynomial.taylorCoordinates_symm line 29
  4. lemma OAI.RationalHitting.TestPolynomial.reverseCoordinates_symm_apply line 34
  5. lemma OAI.RationalHitting.TestPolynomial.reverseTaylor_symm_matrix line 37
  6. def OAI.RationalHitting.TestPolynomial.full line 58

    Source documentation

    The reverse-Taylor test matrix over the univariate polynomial ring in t. Summation over all M Taylor coordinates appends only zero terms.

    def full (M : ℕ) (a : K) : Matrix (Fin M) (Fin M) K[X] := fun i j =>
…
  7. def OAI.RationalHitting.TestPolynomial.padded line 62
  8. def OAI.RationalHitting.TestPolynomial.embed line 66

    Source documentation

    The original t indeterminate embeds into the fresh Laurent indeterminate.

    def embed : K[X] →+* F K := Polynomial.eval₂RingHom HahnSeries.C (HahnSeries.single 1 1)
  9. lemma OAI.RationalHitting.TestPolynomial.embed_C line 68
  10. lemma OAI.RationalHitting.TestPolynomial.embed_X_pow line 69
  11. lemma OAI.RationalHitting.TestPolynomial.full_embed line 72
  12. lemma OAI.RationalHitting.TestPolynomial.full_natDegree_le line 91
  13. lemma OAI.RationalHitting.TestPolynomial.padded_natDegree_le line 98
  14. def OAI.RationalHitting.PaddedRank.raw line 114
  15. lemma OAI.RationalHitting.PaddedRank.raw_apply line 119
  16. def OAI.RationalHitting.PaddedRank.extend line 138
  17. lemma OAI.RationalHitting.PaddedRank.extend_low line 143
  18. lemma OAI.RationalHitting.PaddedRank.extend_injective line 149
  19. lemma OAI.RationalHitting.PaddedRank.padded_mulVec_low line 157
  20. theorem OAI.RationalHitting.PaddedRank.rank_ge line 175

    Source documentation

    The padded test matrices satisfy a rectangular rank lower bound, using an invertible witness and the expansion theorem.

    theorem rank_ge (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)) :
    q*N ≤ (raw A (fun i => embed.mapMatrix (padded M N (points i)))).rank := by
…

    Mentions: OAI.RationalHitting.PaddedRank.raw

  21. lemma OAI.RationalHitting.PaddedRank.numeric_gap line 212
  22. lemma OAI.RationalHitting.TestPolynomial.map_taylor_coeff line 236
  23. lemma OAI.RationalHitting.TestPolynomial.full_map line 241
  24. lemma OAI.RationalHitting.TestPolynomial.padded_map line 250
  25. lemma OAI.RationalHitting.TestPolynomial.eval₂_padded line 254