OAI/NumberTheory/CubicGauss/Recurrence.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Gaussian power factoring and the cubic-sieve exponent recurrence.

  1. lemma OAI.CubicFirstMoment.cubic_conjugate_row_energy line 16
  2. lemma OAI.CubicFirstMoment.full_power_cutoff line 23
  3. theorem OAI.CubicFirstMoment.cubic_full_power_gaussian line 53
  4. def OAI.CubicFirstMoment.recurrenceEnvelope line 117
  5. lemma OAI.CubicFirstMoment.recurrenceEnvelope_nonneg line 120
  6. lemma OAI.CubicFirstMoment.gaussian_power_factor_abstract line 123
  7. lemma OAI.CubicFirstMoment.gaussian_power_factor line 176
  8. theorem OAI.CubicFirstMoment.cubic_recurrence_thin line 216
  9. lemma OAI.CubicFirstMoment.recurrenceEnvelope_mono line 277
  10. lemma OAI.CubicFirstMoment.recurrenceEnvelope_scale line 286
  11. theorem OAI.CubicFirstMoment.cubic_recurrence line 304
  12. def OAI.CubicFirstMoment.sieveStep line 350
  13. def OAI.CubicFirstMoment.sieveThreshold line 351
  14. lemma OAI.CubicFirstMoment.sieveStep_algebra line 353
  15. lemma OAI.CubicFirstMoment.sieve_recurrence_cross line 372
  16. lemma OAI.CubicFirstMoment.sieve_recurrence_last line 394
  17. lemma OAI.CubicFirstMoment.sieve_threshold_ge line 406
  18. lemma OAI.CubicFirstMoment.recurrenceEnvelope_large line 411
  19. lemma OAI.CubicFirstMoment.recurrenceEnvelope_threshold line 419