OAI/NumberTheory/TotientAsymptotic/StrictSlackCost.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The additional polynomial-width shell needed to discard failures of strict slack.

  1. def OAI.TotientAsymptotic.inverseSquareSum line 13
  2. lemma OAI.TotientAsymptotic.inverseSquareSum_nonneg line 15
  3. lemma OAI.TotientAsymptotic.inverseSquare_summable line 18
  4. lemma OAI.TotientAsymptotic.inverseCube_prefix_sum line 21
  5. theorem OAI.TotientAsymptotic.uniform_strict_slack_cost line 48

    Source documentation

    The strict-slack width, unlike the prime-grid width, only decays polynomially. Its total slice cost is still small enough for all cofactors.

    theorem uniform_strict_slack_cost (hren : FordRenewalInput) :
    ∃ C : ℝ, 0 < C ∧ ∀ᶠ x : ℝ in atTop, ∀ H N : ℕ,
      1 ≤ H → H ≤ m x → N ≤ m x →
      (N : ℝ)/B x*((B x)/(m x : ℝ)^4+
        ∑ i : Fin (R x H), g (i.val+1)*
          ((11/10 : ℝ)*bandScale x (i.val+1)/((m x-(i.val+1) : ℕ) : ℝ)^4)) ≤ C/H := by
…

    Mentions: OAI.TotientAsymptotic.FordRenewalInput, OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.g, OAI.TotientAsymptotic.bandScale

  6. lemma OAI.TotientAsymptotic.cofactor_inverse_cutoff_tendsto line 110