OAI/NumberTheory/Catalan/Estimates/ManuscriptCaseTwoNormSubstitutionError.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.manuscriptRatComplexMul line 57
  2. def OAI.InternalCatalan.manuscriptRatComplexPow line 60
  3. theorem OAI.InternalCatalan.manuscript_rat_complex_mul line 64
  4. theorem OAI.InternalCatalan.manuscript_rat_complex_pow line 70
  5. def OAI.InternalCatalan.manuscriptRatTail line 78
  6. def OAI.InternalCatalan.manuscriptRatTailCast line 84
  7. theorem OAI.InternalCatalan.manuscript_barrier_complex_conj line 88
  8. theorem OAI.InternalCatalan.manuscript_rat_tail_cast line 92
  9. def OAI.InternalCatalan.manuscriptP2RatTail line 108
  10. def OAI.InternalCatalan.manuscriptV2RatTail line 109
  11. theorem OAI.InternalCatalan.manuscriptP2_rat_tail_cast line 111
  12. theorem OAI.InternalCatalan.manuscriptV2_rat_tail_cast line 114
  13. def OAI.InternalCatalan.manuscriptRatTailMomentRe line 117
  14. theorem OAI.InternalCatalan.manuscript_rat_tail_moment_re line 120
  15. def OAI.InternalCatalan.manuscriptRatFiniteCross line 131
  16. theorem OAI.InternalCatalan.manuscript_rat_finite_cross_cast line 137
  17. def OAI.InternalCatalan.manuscriptCase1NormSubstituteRat line 157
  18. theorem OAI.InternalCatalan.manuscript_case1_norm_substitute_eq_finite line 161
  19. theorem OAI.InternalCatalan.manuscript_case1_norm_substitute_cutoff line 170
  20. theorem OAI.InternalCatalan.manuscriptP2_rat_finite_cross line 183
  21. theorem OAI.InternalCatalan.manuscriptP2_finite_cross line 188
  22. theorem OAI.InternalCatalan.manuscriptV2_rat_finite_cross line 198
  23. theorem OAI.InternalCatalan.manuscriptV2_finite_cross line 203
  24. def OAI.InternalCatalan.manuscriptCase1NormRoundedSubstituteRat line 222
  25. theorem OAI.InternalCatalan.manuscript_case1_norm_rounded_substitute_eq line 226
  26. theorem OAI.InternalCatalan.manuscript_case1_norm_added_rounding_error_zero line 230
  27. theorem OAI.InternalCatalan.manuscript_case1_norm_eq_substitute line 248
  28. theorem OAI.InternalCatalan.manuscript_case1_norm_substitution_error_zero line 258
  29. theorem OAI.InternalCatalan.manuscriptP2_negative_double_log_upper line 274
  30. theorem OAI.InternalCatalan.manuscriptV2_negative_double_log_upper line 280
  31. theorem OAI.InternalCatalan.manuscript_case2_norm_sharp_upper line 286
  32. def OAI.InternalCatalan.manuscriptNormPSubstituteRat line 309
  33. theorem OAI.InternalCatalan.manuscriptNormPSubstituteRat_upper line 321
  34. def OAI.InternalCatalan.manuscriptNormVSubstituteRat line 334
  35. theorem OAI.InternalCatalan.manuscriptNormVSubstituteRat_upper line 349
  36. def OAI.InternalCatalan.manuscriptCase2NormSubstituteRat line 365
  37. theorem OAI.InternalCatalan.manuscript_case2_norm_substitute_cutoff line 371
  38. theorem OAI.InternalCatalan.manuscriptNormPComposition_error line 391
  39. theorem OAI.InternalCatalan.manuscriptNormVComposition_error line 432
  40. theorem OAI.InternalCatalan.manuscript_case2_norm_composition_difference line 482
  41. theorem OAI.InternalCatalan.manuscript_case2_norm_substitution_error line 499