OAI/NumberTheory/TotientAsymptotic/PPTStructureInput.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The qualitative all-preimage structural condition.

  1. def OAI.TotientAsymptotic.ExtractedStructureInput line 13
  2. lemma OAI.TotientAsymptotic.preimageExceptionCount_le_totientCount line 19
  3. lemma OAI.TotientAsymptotic.ppt_natural_exponential_tendsto line 28
  4. lemma OAI.TotientAsymptotic.ppt_natural_gaussian_tendsto line 33
  5. theorem OAI.TotientAsymptotic.extractedStructureInput_of_small line 44
  6. theorem OAI.TotientAsymptotic.extractedStructureInput_of_ford line 60

    Source documentation

    Preserve the original quantitative Ford-based conditional route while the unconditional proof needs only this smaller qualitative conclusion.

    theorem extractedStructureInput_of_ford (hscale : FordScaleBounds)
    (h10 : FordTheorem10Input) (h16 : FordTheorem16Input) :
    ExtractedStructureInput := by
…

    Mentions: OAI.TotientAsymptotic.FordScaleBounds, OAI.TotientAsymptotic.FordTheorem10Input, OAI.TotientAsymptotic.FordTheorem16Input, OAI.TotientAsymptotic.ExtractedStructureInput