OAI/NumberTheory/CubicMoment/Theta/CubicThetaFiniteExponential.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

Finite rational certificates for the exponential factors in the two coordinate boxes. Every bound is checked from the positive Taylor series.

  1. lemma OAI.CubicFirstMoment.cubic_exp_neg_le_taylor line 11
  2. lemma OAI.CubicFirstMoment.cubic_primary_exp_4 line 18
  3. lemma OAI.CubicFirstMoment.cubic_primary_exp_7 line 27
  4. lemma OAI.CubicFirstMoment.cubic_primary_exp_13 line 36
  5. lemma OAI.CubicFirstMoment.cubic_primary_exp_16 line 45
  6. lemma OAI.CubicFirstMoment.cubic_primary_exp_19 line 54
  7. lemma OAI.CubicFirstMoment.cubic_primary_exp_25 line 63
  8. lemma OAI.CubicFirstMoment.cubic_primary_exp_28 line 72
  9. lemma OAI.CubicFirstMoment.cubic_primary_exp_31 line 81
  10. lemma OAI.CubicFirstMoment.cubic_primary_exp_37 line 90
  11. lemma OAI.CubicFirstMoment.cubic_primary_exp_43 line 99
  12. lemma OAI.CubicFirstMoment.cubic_primary_exp_49 line 108
  13. lemma OAI.CubicFirstMoment.cubic_primary_exp_52 line 117
  14. lemma OAI.CubicFirstMoment.cubic_primary_exp_61 line 126
  15. lemma OAI.CubicFirstMoment.cubic_primary_exp_64 line 135
  16. lemma OAI.CubicFirstMoment.cubic_primary_exp_67 line 144
  17. lemma OAI.CubicFirstMoment.cubic_primary_exp_73 line 153
  18. lemma OAI.CubicFirstMoment.cubic_primary_exp_76 line 162
  19. lemma OAI.CubicFirstMoment.cubic_primary_exp_79 line 171
  20. lemma OAI.CubicFirstMoment.cubic_primary_exp_91 line 180
  21. lemma OAI.CubicFirstMoment.cubic_primary_exp_97 line 189
  22. lemma OAI.CubicFirstMoment.cubic_primary_exp_100 line 198
  23. lemma OAI.CubicFirstMoment.cubic_primary_exp_103 line 207
  24. lemma OAI.CubicFirstMoment.cubic_primary_exp_127 line 216
  25. lemma OAI.CubicFirstMoment.cubic_primary_exp_133 line 225
  26. lemma OAI.CubicFirstMoment.cubic_primary_exp_139 line 234
  27. lemma OAI.CubicFirstMoment.cubic_primary_exp_148 line 243
  28. lemma OAI.CubicFirstMoment.cubic_primary_exp_151 line 252
  29. lemma OAI.CubicFirstMoment.cubic_primary_exp_193 line 261
  30. lemma OAI.CubicFirstMoment.cubic_primary_exp_196 line 270
  31. lemma OAI.CubicFirstMoment.cubic_primary_exp_217 line 279
  32. lemma OAI.CubicFirstMoment.cubic_primary_exp_271 line 288
  33. lemma OAI.CubicFirstMoment.cubic_ramified_exp_1 line 297
  34. lemma OAI.CubicFirstMoment.cubic_ramified_exp_3 line 306
  35. lemma OAI.CubicFirstMoment.cubic_ramified_exp_4 line 315
  36. lemma OAI.CubicFirstMoment.cubic_ramified_exp_7 line 324
  37. lemma OAI.CubicFirstMoment.cubic_ramified_exp_12 line 333