GrowthRates.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.QuantitativeVanDerWaerden.log_ratio_lower_of_rpow_bound line 14

Source documentation

The main real-power lower bound implies a rate uniform in the number of colors. The color-dependent integer logarithm is estimated explicitly.

theorem log_ratio_lower_of_rpow_bound {A c : ℝ} {r k : ℕ}
    (hc : 0 ≤ c) (hr : 2 ≤ r) (hk : 2 ≤ k)
    (hbound : (k : ℝ) ^ (c * k * (Nat.log 2 r : ℝ)) < A) :
    (c / (2 * Real.log 2)) * Real.log (k : ℝ) ≤
      Real.log A / ((k : ℝ) * Real.log (r : ℝ)) := by
…

theorem OAI.QuantitativeVanDerWaerden.log_ratio_lower_of_exp_bound line 46

Source documentation

The large-color exponential lower bound gives a rate independent of the progression length.

theorem log_ratio_lower_of_exp_bound {A r : ℝ} (hr : 1 < r)
    (hbound : Real.exp ((Real.log r) ^ 2 / (64 * Real.log 2)) < A) :
    Real.log r / (64 * Real.log 2) ≤ Real.log A / Real.log r := by
…

theorem OAI.QuantitativeVanDerWaerden.tendsto_iInf_atTop_of_uniform_lower line 62
Source documentation
A common eventual lower bound proves divergence of the actual real infima. Nonemptiness is explicit; the common lower bound supplies the lower-boundedness required by conditional completeness.
```
theorem tendsto_iInf_atTop_of_uniform_lower {ι : Type uIndex} [Nonempty ι]
    {F : ℕ → ι → ℝ} {g : ℕ → ℝ}
    (hg : Tendsto g atTop atTop)
    (h : ∀ᶠ n : ℕ in atTop, ∀ i, g n ≤ F n i) :
    Tendsto (fun n => ⨅ i, F n i) atTop atTop := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.F