OAI/NumberTheory/TotientAsymptotic/Basic.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

Arithmetic data and renewal coefficients for counting totient values.

  1. def OAI.TotientAsymptotic.IsTotient line 13

    Also declared: ComparatorChallenges/TotientAsymptotic.lean:13 (same declaration text), ComparatorChallenges/TotientCompanionZero.lean:13 (same declaration text).

  2. def OAI.TotientAsymptotic.V line 15

    Also declared: ComparatorChallenges/TotientAsymptotic.lean:15 (same declaration text).

  3. def OAI.TotientAsymptotic.ell line 19

    Also declared: ComparatorChallenges/TotientAsymptotic.lean:19 (same declaration text), ComparatorChallenges/TotientCompanionZero.lean:15 (same declaration text).

  4. def OAI.TotientAsymptotic.a line 23

    Also declared: ComparatorChallenges/TotientAsymptotic.lean:23 (same declaration text), ComparatorChallenges/TotientCompanionZero.lean:19 (same declaration text).

  5. def OAI.TotientAsymptotic.RenewalRootSet line 25

    Also declared: ComparatorChallenges/TotientAsymptotic.lean:25 (same declaration text), ComparatorChallenges/TotientCompanionZero.lean:21 (same declaration text).

  6. def OAI.TotientAsymptotic.rho line 28

    Also declared: ComparatorChallenges/TotientAsymptotic.lean:28 (same declaration text), ComparatorChallenges/TotientCompanionZero.lean:24 (same declaration text).

  7. def OAI.TotientAsymptotic.lam line 30

    Also declared: ComparatorChallenges/TotientAsymptotic.lean:30 (same declaration text), ComparatorChallenges/TotientCompanionZero.lean:26 (same declaration text).

  8. def OAI.TotientAsymptotic.gamma line 32

    Also declared: ComparatorChallenges/TotientAsymptotic.lean:32 (same declaration text), ComparatorChallenges/TotientCompanionZero.lean:28 (same declaration text).

  9. def OAI.TotientAsymptotic.g line 34

    Also declared: ComparatorChallenges/TotientAsymptotic.lean:34 (same declaration text).

  10. def OAI.TotientAsymptotic.B line 39

    Also declared: ComparatorChallenges/TotientAsymptotic.lean:39 (same declaration text).

  11. def OAI.TotientAsymptotic.psi line 40

    Also declared: ComparatorChallenges/TotientAsymptotic.lean:40 (same declaration text).

  12. def OAI.TotientAsymptotic.m line 42

    Also declared: ComparatorChallenges/TotientAsymptotic.lean:42 (same declaration text).

  13. def OAI.TotientAsymptotic.theta line 43

    Also declared: ComparatorChallenges/TotientAsymptotic.lean:43 (same declaration text).

  14. def OAI.TotientAsymptotic.G line 45

    Also declared: ComparatorChallenges/TotientAsymptotic.lean:45 (same declaration text).

  15. def OAI.TotientAsymptotic.P line 48

    Also declared: ComparatorChallenges/TotientAsymptotic.lean:48 (same declaration text), ComparatorChallenges/TotientCompanionZero.lean:30 (same declaration text).

  16. def OAI.TotientAsymptotic.alpha line 49

    Also declared: ComparatorChallenges/TotientAsymptotic.lean:49 (same declaration text), ComparatorChallenges/TotientCompanionZero.lean:31 (same declaration text).

  17. def OAI.TotientAsymptotic.largestPrimeFactor line 51

    Also declared: ComparatorChallenges/TotientAsymptotic.lean:51 (same declaration text), ComparatorChallenges/TotientCompanionZero.lean:33 (same declaration text).

  18. structure OAI.TotientAsymptotic.TailDatum line 53

    Also declared: ComparatorChallenges/TotientAsymptotic.lean:53 (same declaration text), ComparatorChallenges/TotientCompanionZero.lean:35 (same declaration text).

  19. def OAI.TotientAsymptotic.tailPrime line 57

    Also declared: ComparatorChallenges/TotientAsymptotic.lean:57 (same declaration text), ComparatorChallenges/TotientCompanionZero.lean:39 (same declaration text).

  20. def OAI.TotientAsymptotic.tailLog line 60

    Also declared: ComparatorChallenges/TotientAsymptotic.lean:60 (same declaration text), ComparatorChallenges/TotientCompanionZero.lean:42 (same declaration text).

  21. def OAI.TotientAsymptotic.IsWitness line 63

    Also declared: ComparatorChallenges/TotientAsymptotic.lean:63 (same declaration text), ComparatorChallenges/TotientCompanionZero.lean:45 (same declaration text).

  22. def OAI.TotientAsymptotic.w line 75

    Also declared: ComparatorChallenges/TotientAsymptotic.lean:75 (same declaration text), ComparatorChallenges/TotientCompanionZero.lean:57 (same declaration text).

  23. def OAI.TotientAsymptotic.witnesses line 78

    Also declared: ComparatorChallenges/TotientAsymptotic.lean:78 (same declaration text), ComparatorChallenges/TotientCompanionZero.lean:60 (same declaration text).

  24. def OAI.TotientAsymptotic.D line 81

    Also declared: ComparatorChallenges/TotientAsymptotic.lean:81 (same declaration text), ComparatorChallenges/TotientCompanionZero.lean:63 (same declaration text).

  25. def OAI.TotientAsymptotic.maxD line 84

    Also declared: ComparatorChallenges/TotientAsymptotic.lean:84 (same declaration text), ComparatorChallenges/TotientCompanionZero.lean:66 (same declaration text).

  26. def OAI.TotientAsymptotic.AH line 88

    Also declared: ComparatorChallenges/TotientAsymptotic.lean:88 (same declaration text), ComparatorChallenges/TotientCompanionZero.lean:70 (same declaration text).

  27. def OAI.TotientAsymptotic.A line 102

    Also declared: ComparatorChallenges/TotientAsymptotic.lean:102 (same declaration text), ComparatorChallenges/TotientCompanionZero.lean:84 (same declaration text).

  28. def OAI.TotientAsymptotic.mainTerm line 104

    Also declared: ComparatorChallenges/TotientAsymptotic.lean:104 (same declaration text).

  29. def OAI.TotientAsymptotic.R line 108
  30. def OAI.TotientAsymptotic.L line 109
  31. def OAI.TotientAsymptotic.bandScale line 111
  32. def OAI.TotientAsymptotic.xi line 114
  33. structure OAI.TotientAsymptotic.RemainderDatum line 117
  34. def OAI.TotientAsymptotic.remainderPrime line 121
  35. def OAI.TotientAsymptotic.remainderCoord line 124
  36. def OAI.TotientAsymptotic.IsBasicRemainder line 127
  37. def OAI.TotientAsymptotic.remainderTail line 139
  38. structure OAI.TotientAsymptotic.PrefixDatum line 142
  39. def OAI.TotientAsymptotic.IsPrefixDatum line 146
  40. def OAI.TotientAsymptotic.M line 151
  41. def OAI.TotientAsymptotic.massError line 158
  42. def OAI.TotientAsymptotic.N line 163

    Also declared: ComparatorChallenges/TotientAsymptotic.lean:106 (same declaration text), ComparatorChallenges/TotientCompanionZero.lean:86 (same declaration text).

  43. def OAI.TotientAsymptotic.fk line 168

    Also declared: ComparatorChallenges/TotientAsymptotic.lean:111 (same declaration text), ComparatorChallenges/TotientCompanionZero.lean:91 (same declaration text).

  44. lemma OAI.TotientAsymptotic.isTotient_pos line 172
  45. lemma OAI.TotientAsymptotic.ell_spec line 176
  46. lemma OAI.TotientAsymptotic.ell_le line 180
  47. lemma OAI.TotientAsymptotic.le_ell line 185
  48. lemma OAI.TotientAsymptotic.one_le_ell_ratio line 189