Main.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.QuantitativeVanDerWaerden.uniform_lower_bound line 12
Source documentation
An absolute quantitative lower bound, uniform over all color counts.
Distinct definitions of this name: ComparatorChallenges/QuantitativeVanDerWaerden.lean:26 (same statement text; different proof or body). Qualify references as OAI.QuantitativeVanDerWaerden.uniform_lower_bound@path.
```
theorem uniform_lower_bound :
    ∃ K : ℕ, ∀ k ≥ K, ∀ r ≥ 2,
      (k : ℝ) ^ ((1 / 100000 : ℝ) * k * (Nat.log 2 r : ℝ)) < (W r k : ℝ) := by
…
```

theorem OAI.QuantitativeVanDerWaerden.uniform_lower_bound_floor line 18

Source documentation

The same bound with the floor of the real base-two logarithm.

theorem uniform_lower_bound_floor :
    ∃ K : ℕ, ∀ k ≥ K, ∀ (r : ℕ), r ≥ 2 →
      (k : ℝ) ^ ((1 / 100000 : ℝ) * k *
        (⌊Real.log (r : ℝ) / Real.log 2⌋₊ : ℝ)) < (W r k : ℝ) := by
…

theorem OAI.QuantitativeVanDerWaerden.exists_uniform_lower_bound line 29

Source documentation

The existential-constant formulation, with a single absolute threshold.

theorem exists_uniform_lower_bound :
    ∃ c : ℝ, 0 < c ∧ ∃ K : ℕ, ∀ k ≥ K, ∀ r ≥ 2,
      (k : ℝ) ^ (c * k * (Nat.log 2 r : ℝ)) < (W r k : ℝ) := by
…

theorem OAI.QuantitativeVanDerWaerden.kthRoot_tendsto line 35
Source documentation
For each fixed color count at least two, the full kth-root limit diverges.
```
theorem kthRoot_tendsto {r : ℕ} (hr : 2 ≤ r) :
    Tendsto (fun k : ℕ => (W r k : ℝ) ^ (1 / (k : ℝ))) atTop atTop := by
…
```

theorem OAI.QuantitativeVanDerWaerden.length_rate_tendsto line 41

Source documentation

The actual infimum over every color count at least two diverges.

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