OAI/NumberTheory/TotientAsymptotic/PublishedFiber.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The published inverse-fiber input and its arithmetic consequences.

FordFiberPropagation d is the single-seed specialization of the construction in Kevin Ford, The distribution of totients, Ramanujan Journal 2 (1998), 67--151, arXiv:1104.3264v2 (2013), Section 5, equations (5.10)--(5.19), and the explicit full-fiber statement in Section 7.3, p. 39.

PPTBoundedFiberPropagation d additionally retains the bounded multiplier ratio from Pollack--Pomerance--Treviño, Sets of monotonicity for Euler's totient function, Ramanujan Journal 30 (2013), 379--398, Lemma 4.1, specialized to the same seed in both positions and D = d, together with Ford's Theorem 1 to replace its scale Z(x) by V(x). The lower-bound constant may depend on d; the absolute bound in the published lemma is weakened here to an existential constant for this fixed seed.

These are explicit hypotheses, not axioms. The conclusions below count large least-preimage ratios; they do not assert the companion asymptotic.

  1. def OAI.TotientAsymptotic.FullFiber line 31
  2. def OAI.TotientAsymptotic.FordFiberPropagation line 35
  3. def OAI.TotientAsymptotic.PPTBoundedFiberPropagation line 40
  4. def OAI.TotientAsymptotic.highRatioCount line 46
  5. def OAI.TotientAsymptotic.boundedHighRatioCount line 51
  6. lemma OAI.TotientAsymptotic.isTotient_of_fullFiber line 56
  7. lemma OAI.TotientAsymptotic.fullFiber_seed_inequality line 61
  8. lemma OAI.TotientAsymptotic.card_fullFibers_le_highRatioCount line 74
  9. theorem OAI.TotientAsymptotic.positive_proportion_highRatio_of_ford line 98

    Source documentation

    A single large least-preimage ratio propagates to a positive fraction of the distinct totients, conditional on Ford's published full-fiber input.

    theorem positive_proportion_highRatio_of_ford {d k : ℕ} (hd : IsTotient d)
    (hseed : k*d < ell d) (hford : FordFiberPropagation d) :
    ∃ η : ℝ, 0 < η ∧ ∀ᶠ x : ℝ in atTop, η * V x ≤ highRatioCount k x := by
…

    Mentions: OAI.TotientAsymptotic.IsTotient, OAI.TotientAsymptotic.ell, OAI.TotientAsymptotic.FordFiberPropagation, OAI.TotientAsymptotic.V, OAI.TotientAsymptotic.highRatioCount

  10. lemma OAI.TotientAsymptotic.pptBoundedFiberPropagation_implies_ford line 107
  11. lemma OAI.TotientAsymptotic.fullFiber_ratio_eq line 116
  12. lemma OAI.TotientAsymptotic.card_fullFibers_le_boundedHighRatioCount line 127
  13. theorem OAI.TotientAsymptotic.positive_proportion_boundedHighRatio_of_ppt line 156

    Source documentation

    PPT Lemma 4.1 supplies a bounded interval of positive ratios directly, without an additional tightness hypothesis about arbitrary totients.

    theorem positive_proportion_boundedHighRatio_of_ppt {d k : ℕ} (hd : IsTotient d)
    (hseed : k*d < ell d) (hppt : PPTBoundedFiberPropagation d) :
    ∃ η C : ℝ, 0 < η ∧ 0 < C ∧ ∀ᶠ x : ℝ in atTop,
      η * V x ≤ boundedHighRatioCount k C x := by
…

    Mentions: OAI.TotientAsymptotic.IsTotient, OAI.TotientAsymptotic.ell, OAI.TotientAsymptotic.PPTBoundedFiberPropagation, OAI.TotientAsymptotic.V, OAI.TotientAsymptotic.boundedHighRatioCount