MovingSeparatedModulusRange.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The regular product and separated arithmetic modulus share one cutoff

theorem OAI.Ostmann.movingArithmeticModuli_with_regular_giant_range line 13

Source documentation

The regular primes are included before absorbing the logarithmic budget. This retains the slack between the nongiant and giant progression scales.

theorem movingArithmeticModuli_with_regular_giant_range (n : ℕ) (F K H : ℝ)
    (hF : 0 ≤ F) (hK : 0 ≤ K) (hH : 0 ≤ H) :
    ∀ᶠ L : ℝ in atTop, ∀ (m r : ℕ) (p : Fin m → ℕ) (P : Finset ℕ) (reg : ℕ),
      (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))) →
      (reg : ℝ) ≤ Real.exp (H * L * Real.exp ((11 / 1000 : ℝ) * L)) →
      reg * (∏ b, movingArithmeticModuli r p P Finset.univ b) ≤
        giantProgressionCutoff L := by
…

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

theorem OAI.Ostmann.movingPattern_regular_exp_range line 67
theorem OAI.Ostmann.movingPattern_actual_separated_modulus_range line 103
Source documentation
The actual frequency tree, internal image and regular product fit the same giant cutoff, rather than two separately exhausted budgets.
```
theorem movingPattern_actual_separated_modulus_range (n r₀ k : ℕ)
    (Cfreq : ℝ) (hCfreq : 0 ≤ Cfreq) :
    ∀ᶠ L : ℝ in atTop, let m := spectatorBulkCount k L
…
```
Mentions: OAI.Ostmann.spectatorBulkCount