OAI/Combinatorics/ProgressionColoring/GrowthConsequences.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.QuantitativeVanDerWaerden.uniform_length_rate_tendsto line 11

   Source documentation

   A single threshold for all color counts yields divergence of the actual infimum over all integers r ≥ 2.

   theorem uniform_length_rate_tendsto
       {F : ℕ → ℕ → ℝ} {c : ℝ} {K : ℕ} (hc : 0 < c)
       (hbound : ∀ k ≥ K, ∀ r ≥ 2,
         (k : ℝ) ^ (c * k * (Nat.log 2 r : ℝ)) < F r k) :
       Tendsto (fun k : ℕ => ⨅ r : {r : ℕ // 2 ≤ r},
         Real.log (F r.val k) / ((k : ℝ) * Real.log (r.val : ℝ))) atTop atTop := by
   …

   Mentions: OAI.QuantitativeVanDerWaerden.F

2. theorem OAI.QuantitativeVanDerWaerden.uniform_color_rate_tendsto line 29

   Source documentation

   The superpolynomial color estimate is uniform in every progression length at least three, including the real infimum conclusion.

   theorem uniform_color_rate_tendsto
       {F : ℕ → ℕ → ℝ} {R : ℕ}
       (hbound : ∀ r ≥ R, ∀ k ≥ 3,
         Real.exp ((Real.log (r : ℝ)) ^ 2 / (64 * Real.log 2)) < F r k) :
       Tendsto (fun r : ℕ => ⨅ k : {k : ℕ // 3 ≤ k},
         Real.log (F r k.val) / Real.log (r : ℝ)) atTop atTop := by
   …

   Mentions: OAI.QuantitativeVanDerWaerden.F

3. theorem OAI.QuantitativeVanDerWaerden.fixed_color_kthRoot_tendsto line 48

   Source documentation

   Every fixed number of colors at least two has the full kth-root limit.

   theorem fixed_color_kthRoot_tendsto
       {F : ℕ → ℕ → ℝ} {c : ℝ} {K : ℕ} (hc : 0 < c)
       (hbound : ∀ k ≥ K, ∀ r ≥ 2,
         (k : ℝ) ^ (c * k * (Nat.log 2 r : ℝ)) < F r k)
       {r : ℕ} (hr : 2 ≤ r) :
       Tendsto (fun k : ℕ => (F r k) ^ (1 / (k : ℝ))) atTop atTop := by
   …

   Mentions: OAI.QuantitativeVanDerWaerden.F

4. theorem OAI.QuantitativeVanDerWaerden.polynomial_ratio_tendsto_of_exp_sq_log line 62

   Source documentation

   A quadratic logarithmic lower bound dominates every fixed power. This statement even allows an arbitrary real exponent.

   theorem polynomial_ratio_tendsto_of_exp_sq_log
       {F : ℕ → ℝ} {C : ℝ} (hC : 0 < C) (A : ℝ)
       (hbound : ∀ᶠ r : ℕ in atTop,
         Real.exp ((Real.log (r : ℝ)) ^ 2 / C) < F r) :
       Tendsto (fun r : ℕ => F r / (r : ℝ) ^ A) atTop atTop := by
   …

   Mentions: OAI.QuantitativeVanDerWaerden.F