OAI/Combinatorics/ProgressionColoring/LargeColor.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.QuantitativeVanDerWaerden.LargeColor.half line 13
2. theorem OAI.QuantitativeVanDerWaerden.LargeColor.half_coefficient_bound line 16

   Source documentation

   The same-half bound is strict for both even and odd bases.

   theorem half_coefficient_bound {b x y z : ℕ} (_hb : 2 ≤ b)
       (hx : x < b) (hy : y < b) (hz : z < b)
       (hxy : half b x = half b y) (hzy : half b z = half b y) :
       |(x : ℤ) - 2 * y + z| < b := by
   …

   Mentions: OAI.QuantitativeVanDerWaerden.LargeColor.half

3. theorem OAI.QuantitativeVanDerWaerden.LargeColor.coefficients_zero line 28

   Source documentation

   A zero base expansion with signed coefficients strictly smaller than the base has all coefficients zero.

   theorem coefficients_zero {b : ℕ} (hb : 2 ≤ b) :
       ∀ {s : ℕ} (a : Fin s → ℤ),
         (∀ i, |a i| < (b : ℤ)) →
         (∑ i, a i * (b : ℤ) ^ (i : ℕ)) = 0 → ∀ i, a i = 0 := by
   …

4. theorem OAI.QuantitativeVanDerWaerden.LargeColor.equal_of_midpoint_equal_norm line 61

   Source documentation

   Equal sums of squares and a coordinatewise midpoint force equality.

   theorem equal_of_midpoint_equal_norm {s : ℕ} (x y z : Fin s → ℤ)
       (hm : ∀ i, x i - 2 * y i + z i = 0)
       (hxy : (∑ i, x i ^ 2) = ∑ i, y i ^ 2)
       (hzy : (∑ i, z i ^ 2) = ∑ i, y i ^ 2) : x = y := by
   …

5. def OAI.QuantitativeVanDerWaerden.LargeColor.normSq line 84
6. theorem OAI.QuantitativeVanDerWaerden.LargeColor.normSq_le line 86
7. abbrev OAI.QuantitativeVanDerWaerden.LargeColor.Color line 96
8. def OAI.QuantitativeVanDerWaerden.LargeColor.vectorColor line 98
9. theorem OAI.QuantitativeVanDerWaerden.LargeColor.card_color line 101
10. theorem OAI.QuantitativeVanDerWaerden.LargeColor.vector_eq_of_monochromatic_midpoint line 105
11. def OAI.QuantitativeVanDerWaerden.LargeColor.digits line 139
12. theorem OAI.QuantitativeVanDerWaerden.LargeColor.digits_value line 142
13. def OAI.QuantitativeVanDerWaerden.LargeColor.coloring line 146
14. theorem OAI.QuantitativeVanDerWaerden.LargeColor.coloring_avoids_three line 149
15. theorem OAI.QuantitativeVanDerWaerden.LargeColor.coloring_avoids line 170
16. theorem OAI.QuantitativeVanDerWaerden.LargeColor.exists_avoiding line 175

    Source documentation

    The exact ambient cardinality suffices to recolor into Fin r.

    theorem exists_avoiding {b s k r : ℕ} (hb : 2 ≤ b) (hk : 3 ≤ k)
        (hcolors : 2 ^ s * (s * (b - 1) ^ 2 + 1) ≤ r) :
        ∃ c : ℕ → Fin r, ¬ HasMonoAP c k (b ^ s) := by
    …

    Mentions: OAI.QuantitativeVanDerWaerden.HasMonoAP

17. theorem OAI.QuantitativeVanDerWaerden.LargeColor.pow_lt_W line 184