OAI/Computability/RationalHitting/IntegralLift.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RationalHitting.CyclotomicRing.root_degree line 9
2. lemma OAI.RationalHitting.CyclotomicRing.root_pow_reduce line 16
3. lemma OAI.RationalHitting.CyclotomicRing.rho_root_pow line 26

   Source documentation

   Every regular-representation entry of a cyclotomic monomial is 0 or ±1. This also gives an explicit integral computation with a division and remainder.

   lemma rho_root_pow (e k : ℕ) (i j : Fin (degree e)) :
       rho e (AdjoinRoot.root (modulus e)^k) i j =
         if (k+j.val) % degree e = i.val then (-1 : ℚ)^((k+j.val)/degree e) else 0 := by
   …

   Mentions: OAI.RationalHitting.CyclotomicRing.degree, OAI.RationalHitting.CyclotomicRing.rho, OAI.RationalHitting.CyclotomicRing.modulus

4. lemma OAI.RationalHitting.CyclotomicRing.rho_character line 37
5. def OAI.RationalHitting.CyclotomicRing.signedEntry line 42
6. lemma OAI.RationalHitting.CyclotomicRing.rho_character_integral line 45
7. lemma OAI.RationalHitting.CyclotomicRing.signedEntry_abs line 49
8. def OAI.RationalHitting.IntegralTest.full line 63

   Source documentation

   Integer computation of the exact expanded Taylor-reversal matrix at t.

   def full (M : ℕ) (a t : ℤ) : Matrix (Fin M) (Fin M) ℤ := fun i j =>
   …

9. def OAI.RationalHitting.IntegralTest.padded line 67
10. lemma OAI.RationalHitting.IntegralTest.coeff_bound line 70
11. lemma OAI.RationalHitting.IntegralTest.full_bound line 81
12. lemma OAI.RationalHitting.IntegralTest.padded_bound line 101
13. lemma OAI.RationalHitting.IntegralTest.full_cast line 115
14. lemma OAI.RationalHitting.IntegralTest.padded_cast line 122
15. lemma OAI.RationalHitting.ThreeLift.eval_uni line 137
16. lemma OAI.RationalHitting.ThreeLift.eval_lift line 144
17. def OAI.RationalHitting.IntegralLift.entry line 170

    Source documentation

    The fixed signed-monomial integer formula for M times a regular lift entry.

    def entry (e : ℕ) (T : Matrix (ZMod (dimension e)) (ZMod (dimension e)) ℤ)
        (p r : ℤ) (u v : ZMod (dimension e)) (i j : Fin (degree e)) : ℤ :=
    …

18. lemma OAI.RationalHitting.IntegralLift.entry_bound line 175
19. lemma OAI.RationalHitting.IntegralLift.rho_rat_mul line 216
20. lemma OAI.RationalHitting.IntegralLift.rho_div_nat line 220
21. lemma OAI.RationalHitting.IntegralLift.entry_spec line 226
22. def OAI.RationalHitting.Generator.coordinate line 270

    Source documentation

    Fixed row-major block coordinate.

    def coordinate (e : ℕ) : ZMod (CyclotomicRing.dimension e) × Fin (CyclotomicRing.degree e) ≃ Fin (D e) :=
    …

    Mentions: OAI.RationalHitting.CyclotomicRing.dimension, OAI.RationalHitting.CyclotomicRing.degree, OAI.RationalHitting.Generator.D

23. lemma OAI.RationalHitting.Generator.regular_apply line 274
24. def OAI.RationalHitting.Generator.integerTest line 281

    Source documentation

    Exact integer Taylor matrices, with the same fixed order of residues.

    def integerTest (N e : ℕ) (a t : ℤ) :
        Matrix (ZMod (CyclotomicRing.dimension e)) (ZMod (CyclotomicRing.dimension e)) ℤ :=
    …

    Mentions: OAI.RationalHitting.CyclotomicRing.dimension

25. def OAI.RationalHitting.Generator.U line 288

    Source documentation

    The common-denominator-cleared regular matrices used in exact arithmetic.

    def U (n N e : ℕ) (x : Fin 3 → ℕ) (a : Fin (n+1)) : Matrix (Fin (D e)) (Fin (D e)) ℤ :=
    …

    Mentions: OAI.RationalHitting.Generator.D

26. lemma OAI.RationalHitting.Generator.U_cast line 293
27. lemma OAI.RationalHitting.Generator.U_bound line 315
28. lemma OAI.RationalHitting.Generator.scaled_normalization line 335
29. lemma OAI.RationalHitting.Generator.tupleAt_integer line 343
30. lemma OAI.RationalHitting.Generator.U_det_ne_zero line 350