OAI/NumberTheory/TotientAsymptotic/CofactorGrowth.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The small cofactor cost is subpolynomial in the tail cut.

  1. def OAI.TotientAsymptotic.cofactorScale line 14
  2. lemma OAI.TotientAsymptotic.cofactorScale_nonneg line 16
  3. lemma OAI.TotientAsymptotic.cofactorScale_div_log_tendsto line 20
  4. theorem OAI.TotientAsymptotic.cofactor_envelope_power_decay line 60

    Source documentation

    Every fixed negative power of H dominates the full allowed cofactor cost. This is the precise meaning of K_H = H^{o(1)} used in the discards.

    theorem cofactor_envelope_power_decay (C : ℝ) {ε : ℝ} (hε : 0 < ε) :
    Tendsto (fun H : ℕ => Real.exp (C*cofactorScale H-ε*Real.log H)) atTop (nhds 0) := by
…

    Mentions: OAI.TotientAsymptotic.cofactorScale