OAI/NumberTheory/TotientAsymptotic/WitnessPrefix.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The exact banded, perturbed regions represented by the arithmetic fibers.

  1. def OAI.TotientAsymptotic.PrefixPrimeBands line 12
  2. lemma OAI.TotientAsymptotic.attachTail_prefix_coord line 16
  3. lemma OAI.TotientAsymptotic.attachTail_tail_prime line 22
  4. lemma OAI.TotientAsymptotic.attachTail_tail_coord line 30
  5. lemma OAI.TotientAsymptotic.attachTail_tail_basic line 38
  6. lemma OAI.TotientAsymptotic.attachTail_cofactor_basic line 79
  7. lemma OAI.TotientAsymptotic.attachTail_prefix_sum line 90
  8. theorem OAI.TotientAsymptotic.basic_attach_iff_region line 98
  9. theorem OAI.TotientAsymptotic.prefixDatum_iff_banded_region line 150

    Source documentation

    Membership in the arithmetic fiber is precisely the banded union of the manuscript's perturbed prefix regions. Witness multiplicities disappear.

    theorem prefixDatum_iff_banded_region {x : ℝ} {H d : ℕ}
    (hPH : P H < H) (hHm : H ≤ m x) (p : Fin (R x H) → ℕ) :
    IsPrefixDatum x H ⟨p,d⟩ ↔ PrefixPrimeBands x H p ∧
      ∃ η ∈ witnesses H (theta x) d, primePrefixCoord p ∈ perturbedTailPrefixRegion x H η := by
…

    Mentions: OAI.TotientAsymptotic.P, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.IsPrefixDatum, OAI.TotientAsymptotic.PrefixPrimeBands, OAI.TotientAsymptotic.witnesses, OAI.TotientAsymptotic.theta, OAI.TotientAsymptotic.primePrefixCoord, OAI.TotientAsymptotic.perturbedTailPrefixRegion