OAI/NumberTheory/TotientAsymptotic/Prefactor.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The finite-tail prefactor, including its dependence on the moving phase.

  1. lemma OAI.TotientAsymptotic.G_step line 13
  2. lemma OAI.TotientAsymptotic.G_sub_eq_product line 24
  3. lemma OAI.TotientAsymptotic.sub_div_self_tendsto line 38
  4. lemma OAI.TotientAsymptotic.normalized_prefactor_step line 50
  5. lemma OAI.TotientAsymptotic.normalized_prefactor_limit line 74
  6. theorem OAI.TotientAsymptotic.prefactor_error line 93

    Source documentation

    The prefactor in the exact intersection volume has the finite-tail limit specified in the manuscript, even though the phase itself need not converge.

    theorem prefactor_error (hford : FordRenewalInput) (H : ℕ) :
    Tendsto (fun x : ℝ => G x (R x H)/G x (m x) -
      rho^(H*(H-1)/2)*(gamma/alpha (theta x))^H) atTop (nhds 0) := by
…

    Mentions: OAI.TotientAsymptotic.FordRenewalInput, OAI.TotientAsymptotic.G, OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.rho, OAI.TotientAsymptotic.gamma, OAI.TotientAsymptotic.alpha, OAI.TotientAsymptotic.theta