UniformTransfer.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.QuantitativeVanDerWaerden.CyclicLowerBound line 12
Source documentation
One threshold supplies actual avoiding cyclic colorings independently of the eventual number of colors. This is a proposition, not an axiom.
```
def CyclicLowerBound (c : ℝ) : Prop :=
…
```
theorem OAI.QuantitativeVanDerWaerden.uniform_lower_of_cyclicLowerBound line 18
Source documentation
The same cyclic coloring works for every number of digits.
```
theorem uniform_lower_of_cyclicLowerBound {c : ℝ} (hcyclic : CyclicLowerBound c) :
    ∃ K : ℕ, ∀ k ≥ K, ∀ r ≥ 2,
      (k : ℝ) ^ (c * k * (Nat.log 2 r : ℝ)) < (W r k : ℝ) := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.CyclicLowerBound
theorem OAI.QuantitativeVanDerWaerden.kthRoot_tendsto_of_cyclicLowerBound line 36
Source documentation
The fixed-color full limit from a proved cyclic construction.
```
theorem kthRoot_tendsto_of_cyclicLowerBound {c : ℝ} (hc : 0 < c)
    (hcyclic : CyclicLowerBound c) {r : ℕ} (hr : 2 ≤ r) :
    Tendsto (fun k : ℕ => (W r k : ℝ) ^ (1 / (k : ℝ))) atTop atTop := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.CyclicLowerBound

theorem OAI.QuantitativeVanDerWaerden.length_rate_tendsto_of_cyclicLowerBound line 44

Source documentation

The infimum over all color counts retains one absolute threshold.

theorem length_rate_tendsto_of_cyclicLowerBound {c : ℝ} (hc : 0 < c)
    (hcyclic : CyclicLowerBound c) :
    Tendsto (fun k : ℕ => ⨅ r : {r : ℕ // 2 ≤ r},
      Real.log (W r.val k : ℝ) / ((k : ℝ) * Real.log (r.val : ℝ))) atTop atTop := by
…

Mentions: OAI.QuantitativeVanDerWaerden.CyclicLowerBound