UniformBudget.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

One absolute threshold for the numerical budgets

The constants in the finite counting bounds are fixed arguments here. The threshold is uniform in the prime-power base, the label counts, and the eventual number of colors. The finite geometric and counting constructions supply the displayed numerical bounds; none is hidden inside the threshold assertion.

theorem OAI.QuantitativeVanDerWaerden.Parameters.integer_affine_risk_le_max line 21

theorem OAI.QuantitativeVanDerWaerden.Parameters.eventually_sparse_budget line 35

Source documentation

Uniform budget for the exact integer exponents in finite sparse perturbation. The base enters only through its proved logarithmic bound.

theorem eventually_sparse_budget {C : ℝ} (hC : 0 ≤ C) :
    ∀ᶠ k : ℕ in atTop, ∀ q : ℕ, 0 < q → ∀ T : ℝ,
      (dimension k : ℝ) * Real.log q ≤
        c * k * Real.log k + (dimension k : ℝ) * Real.log (2 * (k : ℝ) ^ 2) →
      Real.log (max 1 T) ≤ C * (k : ℝ) ^ (9 / 10 : ℝ) * Real.log k →
      2 * (((q ^ dimension k : ℕ) : ℝ)) ^ 2 *
          flipProbability k ^ ((k + 399) / 400) +
        2 * T * (1 - flipProbability k) ^ ((k + 3) / 4) < 1 := by
…

Mentions: OAI.QuantitativeVanDerWaerden.Parameters.dimension, OAI.QuantitativeVanDerWaerden.Parameters.c, OAI.QuantitativeVanDerWaerden.Parameters.flipProbability

theorem OAI.QuantitativeVanDerWaerden.Parameters.eventually_incident_envelope line 56
Source documentation
The row and anchored local weights together eventually obey the incident weight bound of the asymmetric local lemma. Any fixed polynomial exponent is allowed; in particular this includes the proved 14D pattern bound.
```
theorem eventually_incident_envelope {G C a : ℝ}
    (hG : 0 ≤ G) (hC : 1 ≤ C) (ha : 0 ≤ a) :
    ∀ᶠ k : ℕ in atTop, rowEnvelope G k + localTail C a k < 1 / 500 := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.Parameters.rowEnvelope, OAI.QuantitativeVanDerWaerden.Parameters.localTail
theorem OAI.QuantitativeVanDerWaerden.Parameters.eventually_incident_budget line 62
theorem OAI.QuantitativeVanDerWaerden.Parameters.exists_uniform_threshold line 74
Source documentation
One absolute integer threshold satisfies the geometric scales and both probability budgets simultaneously. No color-count parameter occurs here.
```
theorem exists_uniform_threshold {G A C a : ℝ}
    (hG : 0 ≤ G) (hA : 0 ≤ A) (hC : 1 ≤ C) (ha : 0 ≤ a) :
    ∃ K : ℕ, ∀ k ≥ K,
      32 ≤ k ∧ BasicScales k ∧ GeometryScales k ∧
      rowEnvelope G k + localTail C a k < 1 / 500 ∧
      richEnvelope k + affineEnvelope A k < 1 := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.Parameters.BasicScales, OAI.QuantitativeVanDerWaerden.Parameters.GeometryScales, OAI.QuantitativeVanDerWaerden.Parameters.rowEnvelope, OAI.QuantitativeVanDerWaerden.Parameters.localTail, OAI.QuantitativeVanDerWaerden.Parameters.richEnvelope, OAI.QuantitativeVanDerWaerden.Parameters.affineEnvelope