LocalTail.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Decay of the local anchored-pattern union bound

The constants in this estimate are fixed independently of the progression length and of the number of colors. The sum is finite: its upper endpoint is twice the cutoff of the construction.

def OAI.QuantitativeVanDerWaerden.Parameters.localTail line 27
Source documentation
The local union-bound sum, allowing any fixed nonnegative dimension coefficient in the pattern count.
```
def localTail (C a : ℝ) (k : ℕ) : ℝ :=
…
```
theorem OAI.QuantitativeVanDerWaerden.Parameters.localTail_nonneg line 32
theorem OAI.QuantitativeVanDerWaerden.Parameters.local_count_log_le line 40
Source documentation
The logarithm of every local counting base has the same bound on the finite interval of lengths.
```
theorem local_count_log_le {C : ℝ} (hC : 1 ≤ C) {k h : ℕ}
    (hk : 1 ≤ k) (hlog : 1 ≤ Real.log k)
    (hh : h ∈ Finset.Icc (dimension k ^ 2 + 1) (2 * cutoff k)) :
    Real.log (C * (dimension k : ℝ) * h) ≤
      (Real.log (8 * C) + 1) * Real.log k := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.Parameters.dimension, OAI.QuantitativeVanDerWaerden.Parameters.cutoff

theorem OAI.QuantitativeVanDerWaerden.Parameters.localTail_le_of_power_log_le line 74

Source documentation

A finite envelope from one numerical power-logarithm comparison.

theorem localTail_le_of_power_log_le {C a : ℝ} (hC : 1 ≤ C) (ha : 0 ≤ a)
    {k : ℕ} (hk : 1 ≤ k) (hlog : 1 ≤ Real.log k)
    (hsmall : (2 * a * (Real.log (8 * C) + 1)) *
      (k : ℝ) ^ (1 / 10 : ℝ) * Real.log k ≤
        (1 / 128 : ℝ) * (k : ℝ) ^ (1 / 5 : ℝ)) :
    localTail C a k ≤ 4 * (k : ℝ) ^ (1 / 2 : ℝ) *
      Real.exp (-(k : ℝ) ^ (1 / 5 : ℝ) / 128) := by
…

Mentions: OAI.QuantitativeVanDerWaerden.Parameters.localTail

theorem OAI.QuantitativeVanDerWaerden.Parameters.eventually_localTail_le line 136
Source documentation
The local union-bound sum has an eventual bound independent of the number of colors.
```
theorem eventually_localTail_le {C a : ℝ} (hC : 1 ≤ C) (ha : 0 ≤ a) :
    ∀ᶠ k : ℕ in atTop, localTail C a k ≤
      4 * (k : ℝ) ^ (1 / 2 : ℝ) *
        Real.exp (-(k : ℝ) ^ (1 / 5 : ℝ) / 128) := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.Parameters.localTail
theorem OAI.QuantitativeVanDerWaerden.Parameters.tendsto_localTail_zero line 152
Source documentation
The entire finite local-pattern error tends to zero.
```
theorem tendsto_localTail_zero {C a : ℝ} (hC : 1 ≤ C) (ha : 0 ≤ a) :
    Tendsto (localTail C a) atTop (𝓝 0) := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.Parameters.localTail