LargeColorConsequences.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Unconditional growth in the number of colors

These conclusions use the actual digit norm coloring and proved finite upper bound. They do not assume the uniform two-color construction used for growth in the progression length.

theorem OAI.QuantitativeVanDerWaerden.color_rate_tendsto line 19

Source documentation

Uniform divergence over every integer progression length at least three.

theorem color_rate_tendsto :
    Tendsto (fun r : ℕ => ⨅ k : {k : ℕ // 3 ≤ k},
      Real.log (W r k.val : ℝ) / Real.log (r : ℝ)) atTop atTop := by
…

theorem OAI.QuantitativeVanDerWaerden.fixed_length_polynomial_ratio_tendsto line 27
Source documentation
For every fixed progression length at least three, the number grows faster than every fixed real power of the number of colors.
```
theorem fixed_length_polynomial_ratio_tendsto {k : ℕ} (hk : 3 ≤ k) (A : ℝ) :
    Tendsto (fun r : ℕ => (W r k : ℝ) / (r : ℝ) ^ A) atTop atTop := by
…
```