OAI/NumberTheory/DirichletL/ThetaProduct.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SevenEighths.ThetaProduct.rapid_product_sub line 12

    Also declared: ComparatorChallenges/HeckeSevenEighths.lean:11 (same declaration text).

  2. def OAI.SevenEighths.ThetaProduct.product line 33

    Also declared: ComparatorChallenges/HeckeSevenEighths.lean:32 (same declaration text).

  3. theorem OAI.SevenEighths.ThetaProduct.rapid_rescale line 54

    Also declared: ComparatorChallenges/HeckeSevenEighths.lean:53 (same declaration text).

  4. def OAI.SevenEighths.ThetaProduct.rescale line 67

    Also declared: ComparatorChallenges/HeckeSevenEighths.lean:66 (same declaration text).

  5. def OAI.SevenEighths.ThetaProduct.shiftedPair line 92

    Also declared: ComparatorChallenges/HeckeSevenEighths.lean:91 (same declaration text).

  6. theorem OAI.SevenEighths.ThetaProduct.shiftedPair_k line 99

    Also declared: ComparatorChallenges/HeckeSevenEighths.lean:98 (same declaration text).

  7. theorem OAI.SevenEighths.ThetaProduct.shiftedPair_f line 102

    Also declared: ComparatorChallenges/HeckeSevenEighths.lean:101 (same declaration text).

  8. theorem OAI.SevenEighths.ThetaProduct.shiftedPair_differentiableAt line 106

    Also declared: ComparatorChallenges/HeckeSevenEighths.lean:105 (same declaration text).

  9. def OAI.SevenEighths.ThetaProduct.scaledEvenPair line 112

    Also declared: ComparatorChallenges/HeckeSevenEighths.lean:111 (same declaration text).

  10. theorem OAI.SevenEighths.ThetaProduct.scaledEvenPair_f_continuous line 117

    Also declared: ComparatorChallenges/HeckeSevenEighths.lean:116 (same declaration text).

  11. theorem OAI.SevenEighths.ThetaProduct.scaledEvenPair_g_continuous line 123

    Also declared: ComparatorChallenges/HeckeSevenEighths.lean:122 (same declaration text).

  12. def OAI.SevenEighths.ThetaProduct.rectangularPair line 129

    Also declared: ComparatorChallenges/HeckeSevenEighths.lean:128 (same declaration text).

  13. theorem OAI.SevenEighths.ThetaProduct.rectangularPair_k line 135

    Also declared: ComparatorChallenges/HeckeSevenEighths.lean:134 (same declaration text).

  14. theorem OAI.SevenEighths.ThetaProduct.rectangularPair_hasSum line 139
  15. theorem OAI.SevenEighths.ThetaProduct.rectangularPair_differentiableAt line 160