MovingPatternModulusRange.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The full pattern modulus and the separate giant progression cutoff

def OAI.Ostmann.giantProgressionCutoff line 14
Source documentation
The giant comparison includes internal prime squares; the external bulk comparison keeps bulkProgressionCutoff L.
```
noncomputable def giantProgressionCutoff (L : ℝ) : ℕ := bulkProgressionCutoff (10 * L)
```
Mentions: OAI.Ostmann.bulkProgressionCutoff
theorem OAI.Ostmann.giantProgressionCutoff_bounds line 16
theorem OAI.Ostmann.movingArithmeticModuli_exp_bound line 24

theorem OAI.Ostmann.movingArithmeticModuli_giant_range line 54

Source documentation

The actual number of internal classes is fixed by the tree depth. Thus internal squares fit the giant cutoff, uniformly in the pattern and its sampled prime assignment.

theorem movingArithmeticModuli_giant_range (n : ℕ) (F K : ℝ)
    (hF : 0 ≤ F) (hK : 0 ≤ K) :
    ∀ᶠ L : ℝ in atTop, ∀ (m r : ℕ) (p : Fin m → ℕ) (P : Finset ℕ),
      (m : ℝ) ≤ K * L → P.card ≤ 4 * n * 2 ^ n →
      (r : ℝ) ≤ Real.exp (F * m) →
      (∀ q ∈ P, (q : ℝ) ≤ Real.exp (Real.exp ((11 / 1000 : ℝ) * L))) →
      (∀ i, (p i : ℝ) ≤ Real.exp (Real.exp ((1 / 1000 : ℝ) * L))) →
      (∏ b, movingArithmeticModuli r p P Finset.univ b) ≤ giantProgressionCutoff L := by
…

Mentions: OAI.Ostmann.movingArithmeticModuli, OAI.Ostmann.giantProgressionCutoff