OAI/Combinatorics/ProgressionColoring/CyclicModel.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.QuantitativeVanDerWaerden.CyclicGroup line 20
2. def OAI.QuantitativeVanDerWaerden.centered line 22
3. theorem OAI.QuantitativeVanDerWaerden.centered_mem line 24
4. theorem OAI.QuantitativeVanDerWaerden.centered_add_int line 29
5. theorem OAI.QuantitativeVanDerWaerden.centered_int line 35
6. def OAI.QuantitativeVanDerWaerden.xRep line 39
7. def OAI.QuantitativeVanDerWaerden.yRep line 42
8. theorem OAI.QuantitativeVanDerWaerden.xRep_mem line 46
9. theorem OAI.QuantitativeVanDerWaerden.yRep_mem line 50
10. theorem OAI.QuantitativeVanDerWaerden.quotient_integer_difference line 56

    Source documentation

    Dividing congruent integers by any divisor of the modulus gives real representatives differing by an integer.

    theorem quotient_integer_difference {N m : ℕ} (hm : 0 < m) (hdiv : m ∣ N)
        {a b : ℤ} (hab : (a : ZMod N) = (b : ZMod N)) :
        ∃ z : ℤ, (a : ℝ) / m - (b : ℝ) / m = z := by
    …

11. theorem OAI.QuantitativeVanDerWaerden.xRep_integer_offset line 70
12. theorem OAI.QuantitativeVanDerWaerden.yRep_integer_offset line 76
13. theorem OAI.QuantitativeVanDerWaerden.val_add_integer_difference line 84
14. theorem OAI.QuantitativeVanDerWaerden.xRep_add_congr line 99
15. theorem OAI.QuantitativeVanDerWaerden.yRep_add_congr line 110
16. theorem OAI.QuantitativeVanDerWaerden.representative_ap_congr line 124
17. theorem OAI.QuantitativeVanDerWaerden.xRep_ap_congr line 139
18. theorem OAI.QuantitativeVanDerWaerden.yRep_ap_congr line 147
19. theorem OAI.QuantitativeVanDerWaerden.yRep_dilation_congr line 155
20. theorem OAI.QuantitativeVanDerWaerden.yRep_lattice line 172

    Source documentation

    Every centered coordinate lies in the claimed discrete lattice.

    theorem yRep_lattice (q D dilation : ℕ) (n : CyclicGroup q D) (i : Fin D)
        (hq : 0 < q) :
        ∃ z : ℤ, (q : ℝ) ^ (i.val + 1) * yRep q D dilation n i = z := by
    …

    Mentions: OAI.QuantitativeVanDerWaerden.dilation, OAI.QuantitativeVanDerWaerden.CyclicGroup, OAI.QuantitativeVanDerWaerden.yRep

21. theorem OAI.QuantitativeVanDerWaerden.integer_eq_zero_of_abs_lt_one line 184
22. theorem OAI.QuantitativeVanDerWaerden.lattice_separation line 188
23. def OAI.QuantitativeVanDerWaerden.centeredDigit line 203

    Source documentation

    The representative at exponent zero is included as an auxiliary coordinate.

    noncomputable def centeredDigit (q a j : ℕ) : ℝ := centered ((a : ℝ) / (q : ℝ) ^ j)

    Mentions: OAI.QuantitativeVanDerWaerden.centered

24. theorem OAI.QuantitativeVanDerWaerden.centeredDigit_zero line 205
25. theorem OAI.QuantitativeVanDerWaerden.centeredDigit_recurrence line 208
26. theorem OAI.QuantitativeVanDerWaerden.centered_injective_on_unit_interval line 219
27. theorem OAI.QuantitativeVanDerWaerden.centeredDigit_separation line 235

    Source documentation

    The cyclic digit embedding separates distinct residues after multiplication by q. This proof works for every positive base, not just primes.

    theorem centeredDigit_separation {q D a b : ℕ} (hq : 0 < q)
        (ha : a < q ^ D) (hb : b < q ^ D) (hab : a ≠ b) :
        ∃ i : Fin D, 1 ≤ |(q : ℝ) *
          (centeredDigit q a (i.val + 1) - centeredDigit q b (i.val + 1))| := by
    …

    Mentions: OAI.QuantitativeVanDerWaerden.centeredDigit

28. theorem OAI.QuantitativeVanDerWaerden.yRep_coordinate_separation line 269
29. theorem OAI.QuantitativeVanDerWaerden.yRep_squared_separation line 281
30. theorem OAI.QuantitativeVanDerWaerden.prime_power_step_ne line 297
31. theorem OAI.QuantitativeVanDerWaerden.prime_power_ap_injective line 310
32. theorem OAI.QuantitativeVanDerWaerden.prime_power_ap_injective_pow line 321