OAI/NumberTheory/Catalan/Estimates/ManuscriptEnergyLimits.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.InternalCatalan.manuscript_energy_case_threshold line 13
  2. def OAI.InternalCatalan.manuscriptEnergyCaseOne line 19
  3. def OAI.InternalCatalan.manuscriptEnergyCaseTwo line 27
  4. def OAI.InternalCatalan.manuscriptMajorantSupOne line 35
  5. def OAI.InternalCatalan.manuscriptMajorantSupTwo line 39
  6. theorem OAI.InternalCatalan.manuscript_vandermonde_eq_zero_of_not_injective line 43
  7. theorem OAI.InternalCatalan.manuscript_principal_eq_zero_of_not_injective line 59
  8. theorem OAI.InternalCatalan.manuscript_majorantOne_eq_zero_of_not_injective line 64
  9. theorem OAI.InternalCatalan.manuscript_majorantTwo_eq_zero_of_not_injective line 69
  10. theorem OAI.InternalCatalan.manuscript_energy_caseOne_limsup line 74
  11. theorem OAI.InternalCatalan.manuscript_energy_caseTwo_limsup line 100
  12. def OAI.InternalCatalan.manuscriptTrialExponentialDecay line 126
  13. theorem OAI.InternalCatalan.manuscriptTrialExponentialDecay.summable line 129
  14. theorem OAI.InternalCatalan.manuscript_energy_caseOne_limsup_of_exponential_decay line 141
  15. theorem OAI.InternalCatalan.manuscript_energy_caseTwo_limsup_of_exponential_decay line 149
  16. theorem OAI.InternalCatalan.manuscript_energy_determinant_limsup line 157
  17. theorem OAI.InternalCatalan.manuscript_energy_determinant_limsup_of_exponential_decay line 176
  18. theorem OAI.InternalCatalan.manuscript_energy_caseOne_limsup_sharp line 188
  19. theorem OAI.InternalCatalan.manuscript_energy_caseTwo_limsup_sharp line 195