OAI/NumberTheory/Jacobsthal/Conclusions/IteratedLogBudget.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.NumberTheoryLean.IteratedLogBudget.separation line 13

   Source documentation

   The revised cutoff makes the deletion loss smaller than the old, already proved survivor lower bound. The factor A is chosen before the limit.

   theorem separation (c : ℝ) (hc : 0 < c) :
       ∃ A : ℝ, 3 ≤ A ∧ ∀ᶠ k : ℝ in atTop,
         k * deletionBudget (terminalY (rescale A k)) (terminalCutoff (rescale A k)) <
           c * ((terminalY (rescale A k) : ℝ) *
             SmallSieveFinite.smallEuler ⌊ErdosInverseBoxHeight.sourceW
               (terminalTop (rescale A k))⌋₊ /
             (ErdosInverseBoxHeight.sourceB (terminalTop (rescale A k))) ^ 2) := by
   …

   Mentions: OAI.Erdos970.NumberTheoryLean.SmallSieveFinite.smallEuler, OAI.Erdos970.ErdosInverseBoxHeight.sourceW, OAI.Erdos970.ErdosInverseBoxHeight.sourceB