ScalarEntropy.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Finite scalar entropy of the global row count

The estimates below convert an explicit polynomial count into an entropy bound. All constants and the threshold depend only on the progression length; no number of colors or selected prime occurs in these statements.

theorem OAI.QuantitativeVanDerWaerden.Parameters.log_twice_cutoff_le line 17
theorem OAI.QuantitativeVanDerWaerden.Parameters.log_direction_count_le line 40
Source documentation
Entropy of the coarse direction count.
```
theorem log_direction_count_le {k : ℕ} (hk : 2 ≤ k) {L : ℝ}
    (hL : Real.log L ≤ (dimension k : ℝ) ^ 2 * Real.log (2 * (cutoff k : ℝ))) :
    Real.log L ≤ 12 * (k : ℝ) ^ (1 / 5 : ℝ) * Real.log k := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.Parameters.dimension, OAI.QuantitativeVanDerWaerden.Parameters.cutoff
theorem OAI.QuantitativeVanDerWaerden.Parameters.mesh_count_le_polynomial line 55
Source documentation
Polynomial enlargement of the direction count by the mesh construction.
```
theorem mesh_count_le_polynomial {k : ℕ} (hk : 1 ≤ k) {L F : ℝ}
    (hL : 1 ≤ L) (hF : F ≤ (k : ℝ) ^ 2 * L + 28 * (k : ℝ) ^ 3 * Real.log k) :
    F ≤ 29 * (k : ℝ) ^ 4 * L := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.F
theorem OAI.QuantitativeVanDerWaerden.Parameters.log_mesh_count_le line 74
theorem OAI.QuantitativeVanDerWaerden.Parameters.log_row_base_le line 99

theorem OAI.QuantitativeVanDerWaerden.Parameters.log_global_count_le line 132

Source documentation

A finite row-count bound gives an explicit entropy constant for every fixed polynomial exponent e; in particular this applies to exponents six and eight.

theorem log_global_count_le {k e : ℕ} (hk : 32 ≤ k) {L F T : ℝ}
    (hL : 1 ≤ L) (hFone : 1 ≤ F) (hT : 0 < T)
    (hLlog : Real.log L ≤ (dimension k : ℝ) ^ 2 * Real.log (2 * (cutoff k : ℝ)))
    (hF : F ≤ (k : ℝ) ^ 2 * L + 28 * (k : ℝ) ^ 3 * Real.log k)
    (hcount : T ≤ (16 * (3 * (k : ℝ) ^ 2 * F + 1) ^ e) ^ (2 * dimension k)) :
    Real.log T ≤ (16 + 84 * (e : ℝ)) * (k : ℝ) ^ (3 / 10 : ℝ) * Real.log k := by
…

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