OAI/Combinatorics/ProgressionColoring/OuterBudget.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.QuantitativeVanDerWaerden.Parameters.outer_local_sum_eq_localTail line 15

   Source documentation

   The integer anchored-pattern sum on the half-open interval is exactly the real-power local tail already estimated above.

   theorem outer_local_sum_eq_localTail (k : ℕ) :
       (∑ h ∈ Finset.Ioc (dimension k ^ 2) (2 * cutoff k),
         (((16005 * dimension k * h) ^ (14 * dimension k) : ℕ) : ℝ) *
           Real.exp (-(h : ℝ) / 64)) = localTail 16005 14 k := by
   …

   Mentions: OAI.QuantitativeVanDerWaerden.Parameters.dimension, OAI.QuantitativeVanDerWaerden.Parameters.cutoff, OAI.QuantitativeVanDerWaerden.Parameters.localTail

2. theorem OAI.QuantitativeVanDerWaerden.Parameters.eventually_outer_counted_budget line 33

   Source documentation

   The actual finite row and anchored-pattern weights obey the required incident budget. The row count may be zero.

   theorem eventually_outer_counted_budget :
       ∀ᶠ k : ℕ in atTop, ∀ L F : ℝ, 1 ≤ L → 1 ≤ F → ∀ T : ℕ,
         Real.log L ≤ (dimension k : ℝ) ^ 2 * Real.log (2 * (cutoff k : ℝ)) →
         F ≤ (k : ℝ) ^ 2 * L + 28 * (k : ℝ) ^ 3 * Real.log k →
         (T : ℝ) ≤ (16 * (3 * (k : ℝ) ^ 2 * F + 1) ^ (6 : ℕ)) ^
           (2 * dimension k) →
         ((k * T : ℕ) : ℝ) * Real.exp (-((cutoff k : ℝ) / 10 - 1) / 32) +
           (∑ h ∈ Finset.Ioc (dimension k ^ 2) (2 * cutoff k),
             (((16005 * dimension k * h) ^ (14 * dimension k) : ℕ) : ℝ) *
               Real.exp (-(h : ℝ) / 64)) ≤ 1 / 500 := by
   …

   Mentions: OAI.QuantitativeVanDerWaerden.F, OAI.QuantitativeVanDerWaerden.Parameters.dimension, OAI.QuantitativeVanDerWaerden.Parameters.cutoff

3. theorem OAI.QuantitativeVanDerWaerden.Parameters.exists_outer_counted_threshold line 71

   Source documentation

   A single absolute integer threshold works for every admissible finite direction, mesh and row count.

   theorem exists_outer_counted_threshold :
       ∃ K : ℕ, 32 ≤ K ∧ ∀ k ≥ K, ∀ L F : ℝ, 1 ≤ L → 1 ≤ F → ∀ T : ℕ,
         Real.log L ≤ (dimension k : ℝ) ^ 2 * Real.log (2 * (cutoff k : ℝ)) →
         F ≤ (k : ℝ) ^ 2 * L + 28 * (k : ℝ) ^ 3 * Real.log k →
         (T : ℝ) ≤ (16 * (3 * (k : ℝ) ^ 2 * F + 1) ^ (6 : ℕ)) ^
           (2 * dimension k) →
         ((k * T : ℕ) : ℝ) * Real.exp (-((cutoff k : ℝ) / 10 - 1) / 32) +
           (∑ h ∈ Finset.Ioc (dimension k ^ 2) (2 * cutoff k),
             (((16005 * dimension k * h) ^ (14 * dimension k) : ℕ) : ℝ) *
               Real.exp (-(h : ℝ) / 64)) ≤ 1 / 500 := by
   …

   Mentions: OAI.QuantitativeVanDerWaerden.F, OAI.QuantitativeVanDerWaerden.Parameters.dimension, OAI.QuantitativeVanDerWaerden.Parameters.cutoff