OAI/NumberTheory/TotientAsymptotic/CofactorShellDecay.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The cofactor envelope is absorbed by every polynomial-geometric shell tail.

  1. def OAI.TotientAsymptotic.polynomialGeometricTail line 14
  2. lemma OAI.TotientAsymptotic.polynomialGeometricTail_nonneg line 17
  3. lemma OAI.TotientAsymptotic.polynomialGeometricTail_tendsto line 21
  4. lemma OAI.TotientAsymptotic.cofactor_envelope_le_self line 27
  5. lemma OAI.TotientAsymptotic.self_mul_polynomialGeometricTail_le line 36
  6. theorem OAI.TotientAsymptotic.cofactor_polynomialGeometricTail_tendsto line 55

    Source documentation

    This absorbs the entire discrete-cofactor sum in the shell estimates.

    theorem cofactor_polynomialGeometricTail_tendsto (C : ℝ) (k : ℕ)
    {r : ℝ} (hr : 0 ≤ r) (hr1 : r < 1) :
    Tendsto (fun H => Real.exp (C*cofactorScale H)*polynomialGeometricTail k r H)
      atTop (nhds 0) := by
…

    Mentions: OAI.TotientAsymptotic.cofactorScale, OAI.TotientAsymptotic.polynomialGeometricTail

  7. lemma OAI.TotientAsymptotic.cofactor_quadraticShellTail_tendsto line 67