OAI/NumberTheory/TotientAsymptotic/UnconditionalMain.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Asymptotic counting and least-preimage interval theorems.

  1. theorem OAI.TotientAsymptotic.totient_asymptotic_formula line 12

    Distinct definitions of this name: ComparatorChallenges/TotientAsymptotic.lean:118 (same statement text; different proof or body). Qualify references as OAI.TotientAsymptotic.totient_asymptotic_formula@path.

  2. theorem OAI.TotientAsymptotic.weighted_totient_asymptotic line 23

    Distinct definitions of this name: ComparatorChallenges/TotientAsymptotic.lean:128 (same statement text; different proof or body). Qualify references as OAI.TotientAsymptotic.weighted_totient_asymptotic@path.

  3. theorem OAI.TotientAsymptotic.weighted_totient_one_two line 37

    Distinct definitions of this name: ComparatorChallenges/TotientAsymptotic.lean:141 (same statement text; different proof or body). Qualify references as OAI.TotientAsymptotic.weighted_totient_one_two@path.

  4. theorem OAI.TotientAsymptotic.coefficient_nonnegative line 44

    Distinct definitions of this name: ComparatorChallenges/TotientAsymptotic.lean:147 (same statement text; different proof or body). Qualify references as OAI.TotientAsymptotic.coefficient_nonnegative@path.