OAI/Combinatorics/ProgressionColoring/LargeColorGrowth.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.QuantitativeVanDerWaerden.LargeColor.color_count_le_quartic line 12

   Source documentation

   The ambient color count is bounded by a convenient quartic expression.

   theorem color_count_le_quartic {b s : ℕ} (hb : 1 ≤ b) :
       2 ^ s * (s * (b - 1) ^ 2 + 1) ≤ (2 ^ s) ^ 2 * b ^ 2 := by
   …

2. def OAI.QuantitativeVanDerWaerden.LargeColor.base line 26
3. def OAI.QuantitativeVanDerWaerden.LargeColor.dimension line 28
4. theorem OAI.QuantitativeVanDerWaerden.LargeColor.half_le_floor line 30
5. theorem OAI.QuantitativeVanDerWaerden.LargeColor.log_large line 36
6. theorem OAI.QuantitativeVanDerWaerden.LargeColor.base_le_exp line 42
7. theorem OAI.QuantitativeVanDerWaerden.LargeColor.base_ge_two line 46
8. theorem OAI.QuantitativeVanDerWaerden.LargeColor.dimension_argument_ge_one line 53
9. theorem OAI.QuantitativeVanDerWaerden.LargeColor.two_pow_dimension_le line 60
10. theorem OAI.QuantitativeVanDerWaerden.LargeColor.parameter_color_count line 70
11. theorem OAI.QuantitativeVanDerWaerden.LargeColor.dimension_lower line 91
12. theorem OAI.QuantitativeVanDerWaerden.LargeColor.log_base_lower line 100
13. theorem OAI.QuantitativeVanDerWaerden.LargeColor.parameter_size line 110
14. theorem OAI.QuantitativeVanDerWaerden.LargeColor.exp_bound line 126