OAI/Computability/RationalHitting/CyclotomicGrid.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RationalHitting.CyclotomicRing.modulus line 9
  2. def OAI.RationalHitting.CyclotomicRing.degree line 11
  3. def OAI.RationalHitting.CyclotomicRing.dimension line 13
  4. lemma OAI.RationalHitting.CyclotomicRing.modulus_eq_cyclotomic line 15
  5. instance OAI.RationalHitting.CyclotomicRing.modulus_irreducible line 19
  6. abbrev OAI.RationalHitting.CyclotomicRing.R line 22
  7. lemma OAI.RationalHitting.CyclotomicRing.degree_pos line 24
  8. lemma OAI.RationalHitting.CyclotomicRing.dimension_pos line 25
  9. lemma OAI.RationalHitting.CyclotomicRing.modulus_monic line 27
  10. lemma OAI.RationalHitting.CyclotomicRing.modulus_natDegree line 30
  11. def OAI.RationalHitting.CyclotomicRing.powerBasis line 33
  12. def OAI.RationalHitting.CyclotomicRing.basis line 35
  13. lemma OAI.RationalHitting.CyclotomicRing.basis_apply line 38
  14. instance OAI.RationalHitting.CyclotomicRing.dimension_neZero line 43
  15. instance OAI.RationalHitting.CyclotomicRing.charZero line 45
  16. instance OAI.RationalHitting.CyclotomicRing.finite line 49
  17. def OAI.RationalHitting.CyclotomicRing.intoComplex line 52
  18. lemma OAI.RationalHitting.CyclotomicRing.root_primitive line 57

    Source documentation

    The cyclotomic quotient is a field for the chosen powers of two. Irreducibility allows regular-representation invertibility to be proved at a single primitive root.

    lemma root_primitive (e : ℕ) : IsPrimitiveRoot (AdjoinRoot.root (modulus e)) (dimension e) := by
…

    Mentions: OAI.RationalHitting.CyclotomicRing.modulus, OAI.RationalHitting.CyclotomicRing.dimension

  19. def OAI.RationalHitting.CyclotomicRing.character line 64
  20. lemma OAI.RationalHitting.CyclotomicRing.character_primitive line 67
  21. def OAI.RationalHitting.CyclotomicRing.rho line 70
  22. lemma OAI.RationalHitting.CyclotomicRing.rho_root_apply line 73
  23. theorem OAI.RationalHitting.FiniteGrid.exists_eval_ne_zero line 90

    Source documentation

    The fixed grid, independent of the coefficients, finds a nonzero value.

    theorem exists_eval_ne_zero (p : MvPolynomial (Fin k) K) (hp : p ≠ 0)
    (S : Finset K) (hS : p.totalDegree < S.card) :
    ∃ x : Fin k → K, (∀ i, x i ∈ S) ∧ eval x p ≠ 0 := by
…
  24. lemma OAI.RationalHitting.FiniteGrid.det_totalDegree_le line 111
  25. theorem OAI.RationalHitting.FiniteGrid.simultaneous line 126

    Source documentation

    The common grid specializes a list of determinant conditions simultaneously, rather than one formula gate at a time.

    theorem simultaneous (P : List (MvPolynomial (Fin k) K))
    (hP : ∀ p ∈ P, p ≠ 0) (d : ℕ) (hd : ∀ p ∈ P, p.totalDegree ≤ d)
    (S : Finset K) (hS : P.length * d < S.card) :
    ∃ x : Fin k → K, (∀ i, x i ∈ S) ∧ ∀ p ∈ P, eval x p ≠ 0 := by
…