AffineEntropy.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.QuantitativeVanDerWaerden.Parameters.affine_count_factor_le line 10
Source documentation
The additive terms in the finite affine count fit in a factor of three.
```
theorem affine_count_factor_le {k D q : ℝ}
    (hk : 1 ≤ k) (hD : 1 ≤ D) (hq : 1 ≤ q) :
    k * (D * q ^ 2 + 1) + 1 ≤ 3 * k * D * q ^ 2 := by
…
```

theorem OAI.QuantitativeVanDerWaerden.Parameters.affine_count_le_simple line 21

Source documentation

A convenient multiplicative form of the actual finite count bound.

theorem affine_count_le_simple {k D q Tglob Taff : ℝ}
    (hk : 1 ≤ k) (hD : 1 ≤ D) (hq : 1 ≤ q)
    (hTglob : 0 ≤ Tglob)
    (hcount : Taff ≤ 25 * Tglob * (k * (D * q ^ 2 + 1) + 1) ^ 8) :
    Taff ≤ 25 * Tglob * (3 * k * D * q ^ 2) ^ 8 := by
…

theorem OAI.QuantitativeVanDerWaerden.Parameters.log_dimension_le_two_log line 32
Source documentation
The rounded dimension contributes at most twice the logarithm of k.
```
theorem log_dimension_le_two_log {k : ℕ} (hk : 2 ≤ k) :
    Real.log (dimension k : ℝ) ≤ 2 * Real.log (k : ℝ) := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.Parameters.dimension

theorem OAI.QuantitativeVanDerWaerden.Parameters.affine_entropy_bound line 48

Source documentation

The finite affine count has entropy of order k^(9/10) log k, with a constant independent of the number of colors.

theorem affine_entropy_bound {k : ℕ} (hk : 32 ≤ k)
    {Taff Tglob q A : ℝ}
    (hTaff : 1 ≤ Taff) (hTglob : 1 ≤ Tglob) (hq : 1 ≤ q) (hA : 0 ≤ A)
    (hcount : Taff ≤ 25 * Tglob *
      ((k : ℝ) * ((dimension k : ℝ) * q ^ 2 + 1) + 1) ^ 8)
    (hglobal : Real.log Tglob ≤
      A * (k : ℝ) ^ (3 / 10 : ℝ) * Real.log (k : ℝ))
    (hprime : Real.log q ≤
      4 * (k : ℝ) ^ (9 / 10 : ℝ) * Real.log (k : ℝ)) :
    Real.log Taff ≤ (A + 108) * (k : ℝ) ^ (9 / 10 : ℝ) * Real.log (k : ℝ) := by
…

Mentions: OAI.QuantitativeVanDerWaerden.Parameters.dimension