OAI/NumberTheory/Catalan/Analysis/RealPlaceLimsup.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.manuscriptNormalizedLogSize line 14
  2. theorem OAI.InternalCatalan.manuscriptNormalizedLogSize_zero line 18
  3. theorem OAI.InternalCatalan.manuscriptNormalizedLogSize_of_ne_zero line 22
  4. def OAI.InternalCatalan.manuscriptDeterminantLogSize line 27
  5. theorem OAI.InternalCatalan.manuscriptDeterminantLogSize_of_eq_zero line 30
  6. theorem OAI.InternalCatalan.manuscriptDeterminantLogSize_of_ne_zero line 34
  7. theorem OAI.InternalCatalan.manuscript_limsup_le_of_eventually_le line 39
  8. theorem OAI.InternalCatalan.determinant_real_place_limsup line 62
  9. theorem OAI.InternalCatalan.real_place_limsup_constant_lt_threshold line 74
  10. theorem OAI.InternalCatalan.determinant_real_place_limsup_lt_threshold line 80
  11. theorem OAI.InternalCatalan.real_place_separate_case_constants line 85