OAI/NumberTheory/TotientAsymptotic/CollisionTail.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The summable, phase-independent tail in the prefix collision estimate.

  1. def OAI.TotientAsymptotic.collisionKernel line 15

    Source documentation

    The contribution of a suffix at distance h from the end, after restoring its common prefix and integrating the dyadic suffix estimates.

    def collisionKernel (c : ℝ) (h : ℕ) : ℝ :=
…
  2. lemma OAI.TotientAsymptotic.collisionKernel_nonneg line 18
  3. lemma OAI.TotientAsymptotic.collisionKernel_le_geometric line 22
  4. theorem OAI.TotientAsymptotic.summable_collisionKernel line 45
  5. def OAI.TotientAsymptotic.collisionTail line 53
  6. lemma OAI.TotientAsymptotic.collisionTail_nonneg line 55
  7. theorem OAI.TotientAsymptotic.collisionTail_tendsto line 59

    Source documentation

    The final error can be chosen independently of the phase and tends to zero.

    theorem collisionTail_tendsto (c : ℝ) : Tendsto (collisionTail c) atTop (nhds 0) := by
…

    Mentions: OAI.TotientAsymptotic.collisionTail