OAI/NumberTheory/TotientAsymptotic/TailBelowPrefix.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TotientAsymptotic.tail_log_comparison line 13
2. theorem OAI.TotientAsymptotic.basic_tail_lt_last_prefix line 26

   Source documentation

   The exact arithmetic tail lies below every retained prefix prime. This is uniform in the phase; the cofactor cut grows much slower than the prefix cut.

   theorem basic_tail_lt_last_prefix : ∀ᶠ H : ℕ in atTop,
       ∀ x : ℝ, theta x ∈ Set.Ico (0 : ℝ) 1 → H < m x →
       ∀ η : RemainderDatum (L x H), IsBasicRemainder x H η →
         remainderTail x H η < remainderPrime η (R x H) := by
   …

   Mentions: OAI.TotientAsymptotic.theta, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.RemainderDatum, OAI.TotientAsymptotic.L, OAI.TotientAsymptotic.IsBasicRemainder, OAI.TotientAsymptotic.remainderTail, OAI.TotientAsymptotic.remainderPrime, OAI.TotientAsymptotic.R