OAI/NumberTheory/Ostmann/Arithmetic/MovingProtectedTarget.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingProtectedTarget line 10
2. theorem OAI.Ostmann.movingProtectedTarget_bounds line 15

   Source documentation

   A fixed factor in the block width leaves room for every small prime cell above exp(exp(.01 L)). It affects none of the asymptotic estimates.

   theorem movingProtectedTarget_bounds (k : ℕ) (hk : 2 ≤ k)
       (h G₀ G td totalGap : ℝ) (hh : 0 ≤ h)
       (hGlo : G₀ ≤ G) (hGhi : G ≤ G₀ + 12 * h)
       (herror : |totalGap - 2 * td| ≤ h) :
       16 * h ≤ movingProtectedTarget k (2 * G₀ + 2 ^ (k + 1) * (12 * h)) G td totalGap ∧
         movingProtectedTarget k (2 * G₀ + 2 ^ (k + 1) * (12 * h)) G td totalGap ≤ 32 * h := by
   …

   Mentions: OAI.Ostmann.movingProtectedTarget

3. theorem OAI.Ostmann.eventual_protected_target_error line 32
4. theorem OAI.Ostmann.eventual_protected_cell_target_range line 44