ScalarMesh.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.QuantitativeVanDerWaerden.Parameters.scalar_log_prime_slack line 11
theorem OAI.QuantitativeVanDerWaerden.Parameters.scalar_dimension_le_two_mul line 20
theorem OAI.QuantitativeVanDerWaerden.Parameters.scalar_nat_le_dimension_rpow line 30
Source documentation
The dimension cancels nine tenths of a power of the progression length.
```
theorem scalar_nat_le_dimension_rpow {k : ℕ} (hk : 1 ≤ k) :
    (k : ℝ) ≤ dimension k * (k : ℝ) ^ (9 / 10 : ℝ) := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.Parameters.dimension
theorem OAI.QuantitativeVanDerWaerden.Parameters.scalar_log_q_le line 41
Source documentation
A bound uniform over every prime power permitted by the construction.
```
theorem scalar_log_q_le {k q : ℕ} (hk : 2 ≤ k)
    (hqlog : (dimension k : ℝ) * Real.log q ≤
      c * k * Real.log k + dimension k * Real.log (2 * (k : ℝ) ^ 2)) :
    Real.log q ≤ 4 * (k : ℝ) ^ (9 / 10 : ℝ) * Real.log k := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.Parameters.dimension, OAI.QuantitativeVanDerWaerden.Parameters.c

theorem OAI.QuantitativeVanDerWaerden.Parameters.scalar_dimension_log_q_le line 72

Source documentation

The logarithmic size of the inverse small-cell offset.

theorem scalar_dimension_log_q_le {k q : ℕ} (hk : 2 ≤ k)
    (hqlog : (dimension k : ℝ) * Real.log q ≤
      c * k * Real.log k + dimension k * Real.log (2 * (k : ℝ) ^ 2)) :
    ((dimension k : ℝ) + 1) * Real.log q ≤ 13 * k * Real.log k := by
…

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

def OAI.QuantitativeVanDerWaerden.Parameters.scalarAlpha line 100
Source documentation
The actual offset q^(-(D+1)), written using a natural power.
```
def scalarAlpha (k q : ℕ) : ℝ := 1 / (q : ℝ) ^ (dimension k + 1)
```
Mentions: OAI.QuantitativeVanDerWaerden.Parameters.dimension
def OAI.QuantitativeVanDerWaerden.Parameters.scalarRadius line 103
Source documentation
The logarithmic radius of the exponential mesh.
```
def scalarRadius (k q : ℕ) : ℝ := Real.log (1 + 1 / (2 * scalarAlpha k q))
```
Mentions: OAI.QuantitativeVanDerWaerden.Parameters.scalarAlpha
def OAI.QuantitativeVanDerWaerden.Parameters.scalarMeshSize line 106
Source documentation
The actual number of positive radial mesh intervals.
```
def scalarMeshSize (k q : ℕ) : ℕ := ⌈(k : ℝ) ^ 2 * scalarRadius k q⌉₊
```
Mentions: OAI.QuantitativeVanDerWaerden.Parameters.scalarRadius
theorem OAI.QuantitativeVanDerWaerden.Parameters.scalar_q_power_ge_four line 108
theorem OAI.QuantitativeVanDerWaerden.Parameters.scalarAlpha_pos line 118
theorem OAI.QuantitativeVanDerWaerden.Parameters.scalarAlpha_le_quarter line 123
theorem OAI.QuantitativeVanDerWaerden.Parameters.scalarRadius_pos line 127
theorem OAI.QuantitativeVanDerWaerden.Parameters.scalarRadius_le_dimension_log_q line 134
Source documentation
The mesh logarithmic radius is at most the logarithm of its denominator.
```
theorem scalarRadius_le_dimension_log_q {k q : ℕ}
    (hk : 1 ≤ k) (hq : 2 ≤ q) :
    scalarRadius k q ≤ ((dimension k : ℝ) + 1) * Real.log q := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.Parameters.scalarRadius, OAI.QuantitativeVanDerWaerden.Parameters.dimension
theorem OAI.QuantitativeVanDerWaerden.Parameters.scalarRadius_le line 151
Source documentation
Explicit logarithmic radius bound for every admissible prime-power choice.
```
theorem scalarRadius_le {k q : ℕ} (hk : 2 ≤ k) (hq : 2 ≤ q)
    (hqlog : (dimension k : ℝ) * Real.log q ≤
      c * k * Real.log k + dimension k * Real.log (2 * (k : ℝ) ^ 2)) :
    scalarRadius k q ≤ 13 * k * Real.log k :=
…
```
Mentions: OAI.QuantitativeVanDerWaerden.Parameters.dimension, OAI.QuantitativeVanDerWaerden.Parameters.c, OAI.QuantitativeVanDerWaerden.Parameters.scalarRadius
theorem OAI.QuantitativeVanDerWaerden.Parameters.scalarMeshSize_upper line 159
Source documentation
An explicit bound on the number of labels in the signed radial mesh.
```
theorem scalarMeshSize_upper {k q : ℕ} (hk : 2 ≤ k) (hq : 2 ≤ q)
    (hlog : 1 ≤ Real.log k)
    (hqlog : (dimension k : ℝ) * Real.log q ≤
      c * k * Real.log k + dimension k * Real.log (2 * (k : ℝ) ^ 2)) :
    2 * (scalarMeshSize k q : ℝ) ≤ 28 * (k : ℝ) ^ 3 * Real.log k := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.Parameters.dimension, OAI.QuantitativeVanDerWaerden.Parameters.c, OAI.QuantitativeVanDerWaerden.Parameters.scalarMeshSize