OAI/NumberTheory/Ostmann/Arithmetic/MovingIntegerRanges.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingCutoffExponent_ge_reserve line 11
2. theorem OAI.Ostmann.eventually_moving_integer_ranges line 27

   Source documentation

   The same concrete floor cutoffs give both strict determinant rigidity and the next-frequency bound, simultaneously at every transfer depth.

   theorem eventually_moving_integer_ranges (Bs BD Bz z C : ℝ)
       (hBs : 0 ≤ Bs) (hBD : Bs + 1 ≤ BD) (hBz : 8 ≤ Bz) (hz : 1 ≤ z) :
       ∀ᶠ m : ℝ in atTop, ∀ n : ℕ, ∀ T : ℝ, ∀ M R : ℕ,
         Real.exp (T - C) ≤ M →
         Real.exp (T + spectatorStepGap BD Bz z ((2 : ℝ) ^ n) m - C) ≤ R →
         2 * naturalProductCap (T + C) * movingNaturalCutoff Bs BD Bz z m n < R ∧
         2 * movingNaturalCutoff Bs BD Bz z m n *
           naturalProductCap (T + spectatorStepGap BD Bz z ((2 : ℝ) ^ n) m + C) ≤
           movingNaturalCutoff Bs BD Bz z m (n + 1) * M := by
   …

   Mentions: OAI.Ostmann.spectatorStepGap, OAI.Ostmann.naturalProductCap, OAI.Ostmann.movingNaturalCutoff