OAI/NumberTheory/TotientAsymptotic/ExtractTail.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The finite tail witness extracted from a basic remainder.

  1. def OAI.TotientAsymptotic.extractTail line 13
  2. lemma OAI.TotientAsymptotic.extractTail_prime line 17
  3. lemma OAI.TotientAsymptotic.extractTail_log line 23
  4. lemma OAI.TotientAsymptotic.bandScale_reversed line 30
  5. lemma OAI.TotientAsymptotic.extractTail_value line 34
  6. lemma OAI.TotientAsymptotic.extractTail_threshold line 62
  7. theorem OAI.TotientAsymptotic.extractTail_isWitness line 93

    Source documentation

    A basic remainder gives one of the actual phase-dependent finite witnesses, with exactly the same tail totient; no extra tail representatives are counted.

    theorem extractTail_isWitness {x : ℝ} {H : ℕ} {η : RemainderDatum (L x H)}
    (hη : IsBasicRemainder x H η) (hPH : P H < H) (hHm : H ≤ m x) :
    IsWitness H (theta x) (extractTail x H η) := by
…

    Mentions: OAI.TotientAsymptotic.RemainderDatum, OAI.TotientAsymptotic.L, OAI.TotientAsymptotic.IsBasicRemainder, OAI.TotientAsymptotic.P, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.IsWitness, OAI.TotientAsymptotic.theta, OAI.TotientAsymptotic.extractTail