OAI/NumberTheory/TotientAsymptotic/UniquePrefix.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TotientAsymptotic.exceptionalTotients line 12
2. def OAI.TotientAsymptotic.nonuniqueValues line 15
3. def OAI.TotientAsymptotic.discardedTuples line 19
4. lemma OAI.TotientAsymptotic.unique_prefix_finite_comparison line 23
5. lemma OAI.TotientAsymptotic.common_prefix_inverse_fiber line 59

   Source documentation

   All inverse images of an ordinary value have the same displayed prime prefix. This uses all-preimage extraction, not merely existence of a witness.

   lemma common_prefix_inverse_fiber {H : ℕ} (hPH : P H < H) (hP : 1 ≤ P H) :
       ∀ᶠ x : ℝ in atTop,
       ∀ τ ∈ tupleFinset x H x \ discardedTuples x H,
       (Set.InjOn (fun σ : TotientTuple (R x H) => tupleValue σ) (↑(tupleFinset x H x \ discardedTuples x H))) →
       tupleValue τ ∈ totientValues x \ nonuniqueValues x H →
       ∀ n : ℕ, 0 < n → n.totient=tupleValue τ →
         ∃ w : ℕ, 0 < w ∧ w.totient=τ.tail.d ∧ n=tuplePrimeProduct τ*w := by
   …

   Mentions: OAI.TotientAsymptotic.P, OAI.TotientAsymptotic.tupleFinset, OAI.TotientAsymptotic.discardedTuples, OAI.TotientAsymptotic.TotientTuple, OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.tupleValue, OAI.TotientAsymptotic.totientValues, OAI.TotientAsymptotic.nonuniqueValues, OAI.TotientAsymptotic.w, OAI.TotientAsymptotic.tuplePrimeProduct