PrimeScale.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.QuantitativeVanDerWaerden.Parameters.exists_power_near line 15

Source documentation

A positive power of an integer base lies within one base factor of any real target at least one.

theorem exists_power_near {P : ℕ} (hP : 2 ≤ P) {x : ℝ} (hx : 1 ≤ x) :
    ∃ n : ℕ, 0 < n ∧ x ≤ ((P ^ n : ℕ) : ℝ) ∧
      ((P ^ n : ℕ) : ℝ) ≤ (P : ℝ) * x := by
…

theorem OAI.QuantitativeVanDerWaerden.Parameters.exists_prime_above line 29
Source documentation
The elementary prime bound used in the cyclic construction.
```
theorem exists_prime_above {k : ℕ} (hk : 2 ≤ k) :
    ∃ P : ℕ, P.Prime ∧ k < P ∧ P ≤ 2 * k ^ 2 := by
…
```
structure OAI.QuantitativeVanDerWaerden.Parameters.PrimeScale line 37
Source documentation
The complete arithmetic choice of prime and prime-power base.
```
structure PrimeScale (k D : ℕ) where
…
```
theorem OAI.QuantitativeVanDerWaerden.Parameters.exists_primeScale line 49
theorem OAI.QuantitativeVanDerWaerden.Parameters.PrimeScale.isPrimePow line 76
theorem OAI.QuantitativeVanDerWaerden.Parameters.PrimeScale.two_le line 80
theorem OAI.QuantitativeVanDerWaerden.Parameters.PrimeScale.pos line 82
theorem OAI.QuantitativeVanDerWaerden.Parameters.PrimeScale.log_lower line 84
theorem OAI.QuantitativeVanDerWaerden.Parameters.PrimeScale.log_upper line 96
theorem OAI.QuantitativeVanDerWaerden.Parameters.PrimeScale.cardinal_lower line 115
Source documentation
The cardinality of the cyclic group has the required superexponential scale.
```
theorem cardinal_lower (hk : 2 ≤ k) (hD : 1 ≤ D) :
    (k : ℝ) ^ (c * k) ≤ ((s.q ^ D : ℕ) : ℝ) := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.Parameters.c