OAI/NumberTheory/Catalan/Estimates/ManuscriptCaseOneX4PointRounding.lean

GitHub source file

81 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.InternalCatalan.manuscript_interval_abs_sub_le_width line 11
  2. theorem OAI.InternalCatalan.manuscript_interval_abs_sub_lt_of_width line 21
  3. theorem OAI.InternalCatalan.manuscript_interval_abs_sub_le_rounded_width line 28
  4. theorem OAI.InternalCatalan.manuscript_interval_abs_sub_lt_of_rounded_width line 36
  5. def OAI.InternalCatalan.manuscriptComplexLogApprox line 55
  6. theorem OAI.InternalCatalan.manuscript_real_log_error_le_101h0 line 58
  7. theorem OAI.InternalCatalan.manuscript_complex_log_norm_error_lt line 67
  8. theorem OAI.InternalCatalan.manuscript_finite_error_sum_le line 100
  9. theorem OAI.InternalCatalan.manuscript_list_abs_sum_le_of_error line 110
  10. theorem OAI.InternalCatalan.manuscript_list_error_sum_le line 128
  11. theorem OAI.InternalCatalan.manuscript_weighted_complex_difference_le line 141
  12. theorem OAI.InternalCatalan.manuscript_finite_weighted_complex_error_le line 148
  13. theorem OAI.InternalCatalan.manuscript_list_weighted_complex_error_le line 158
  14. theorem OAI.InternalCatalan.manuscript_sum_error_lt_norm_allowance_of_mass line 169
  15. theorem OAI.InternalCatalan.manuscript_sum_error_lt_X_allowance_of_mass line 181
  16. theorem OAI.InternalCatalan.manuscript_sum_error_lt_Y_allowance_of_mass line 191
  17. theorem OAI.InternalCatalan.manuscript_three_error_allowances_lt_coarse line 201
  18. theorem OAI.InternalCatalan.manuscript_list_error_lt_norm_allowance_of_mass line 206
  19. theorem OAI.InternalCatalan.manuscript_list_error_lt_X_allowance_of_mass line 217
  20. theorem OAI.InternalCatalan.manuscript_list_error_lt_Y_allowance_of_mass line 226
  21. def OAI.InternalCatalan.manuscriptTermRoundStep line 235
  22. theorem OAI.InternalCatalan.manuscript_series_rounding_error_le line 237
  23. theorem OAI.InternalCatalan.manuscript_H_rounding_error_le line 245
  24. theorem OAI.InternalCatalan.manuscript_J_rounding_error_le line 259
  25. theorem OAI.InternalCatalan.manuscript_scaled_real_rounding_error_le_of_series_bounds line 269
  26. theorem OAI.InternalCatalan.manuscript_complex_rounding_error_le_of_series_bounds line 285
  27. theorem OAI.InternalCatalan.manuscript_rounding_sum_lt_of_mass line 326
  28. theorem OAI.InternalCatalan.manuscript_list_rounding_sum_lt_of_mass line 337
  29. def OAI.InternalCatalan.manuscriptRoundDownRat line 360
  30. def OAI.InternalCatalan.manuscriptRoundUpRat line 363
  31. theorem OAI.InternalCatalan.manuscript_round_rat_enclosure line 366
  32. theorem OAI.InternalCatalan.manuscript_round_step_cast line 399
  33. theorem OAI.InternalCatalan.manuscript_round_down_cast_error_le line 403
  34. theorem OAI.InternalCatalan.manuscript_round_up_cast_error_le line 408
  35. def OAI.InternalCatalan.manuscriptHInnerRat line 413
  36. def OAI.InternalCatalan.manuscriptJTermRat line 416
  37. def OAI.InternalCatalan.manuscriptRoundedHRat line 419
  38. def OAI.InternalCatalan.manuscriptRoundedJRat line 422
  39. def OAI.InternalCatalan.manuscriptRoundedScaledLogRat line 425
  40. def OAI.InternalCatalan.manuscriptRoundedArgRat line 428
  41. def OAI.InternalCatalan.manuscriptRoundedComplexLog line 432
  42. theorem OAI.InternalCatalan.manuscript_round_sum_cast line 436
  43. theorem OAI.InternalCatalan.manuscript_rounded_H_error_le line 441
  44. theorem OAI.InternalCatalan.manuscript_rounded_J_error_le line 454
  45. theorem OAI.InternalCatalan.manuscript_rounded_scaled_log_error_le line 466
  46. theorem OAI.InternalCatalan.manuscript_rounded_complex_log_error_le line 480
  47. def OAI.InternalCatalan.manuscriptRoundedWeightedComplexLogRat line 516
  48. def OAI.InternalCatalan.manuscriptRoundedXFieldRat line 519
  49. def OAI.InternalCatalan.manuscriptRoundedYFieldRat line 524
  50. theorem OAI.InternalCatalan.manuscript_rat_add_rounding_error line 528
  51. theorem OAI.InternalCatalan.manuscript_rat_mul_rounding_error line 538
  52. theorem OAI.InternalCatalan.manuscript_rounded_scaled_rat_error_le line 546
  53. theorem OAI.InternalCatalan.manuscript_rounded_weighted_complex_log_error_le line 553
  54. theorem OAI.InternalCatalan.manuscript_rounded_x_field_error_le line 586
  55. theorem OAI.InternalCatalan.manuscript_rounded_y_field_error_le line 614
  56. def OAI.InternalCatalan.manuscriptCase1X0SubstituteRat line 646
  57. theorem OAI.InternalCatalan.manuscript_case1X0_substitute_interval line 649
  58. theorem OAI.InternalCatalan.manuscript_case1X0_substitute_cutoff line 655
  59. def OAI.InternalCatalan.manuscriptCase1X1SubstituteRat line 672
  60. theorem OAI.InternalCatalan.manuscript_case1X1_substitute_interval line 675
  61. theorem OAI.InternalCatalan.manuscript_case1X1_substitute_cutoff line 681
  62. def OAI.InternalCatalan.manuscriptCase1X2SubstituteRat line 698
  63. theorem OAI.InternalCatalan.manuscript_case1X2_substitute_interval line 701
  64. theorem OAI.InternalCatalan.manuscript_case1X2_substitute_cutoff line 707
  65. def OAI.InternalCatalan.manuscriptCase1X3SubstituteRat line 724
  66. theorem OAI.InternalCatalan.manuscript_case1X3_substitute_interval line 727
  67. theorem OAI.InternalCatalan.manuscript_case1X3_substitute_cutoff line 733
  68. def OAI.InternalCatalan.manuscriptCase1X0RoundedSubstituteRat line 750
  69. theorem OAI.InternalCatalan.manuscript_case1X0_additional_rounding_error line 753
  70. theorem OAI.InternalCatalan.manuscript_case1X0_actual_substitution_error line 776
  71. def OAI.InternalCatalan.manuscriptCase1X1RoundedSubstituteRat line 797
  72. theorem OAI.InternalCatalan.manuscript_case1X1_additional_rounding_error line 800
  73. theorem OAI.InternalCatalan.manuscript_case1X1_actual_substitution_error line 823
  74. def OAI.InternalCatalan.manuscriptCase1X2RoundedSubstituteRat line 844
  75. theorem OAI.InternalCatalan.manuscript_case1X2_additional_rounding_error line 847
  76. theorem OAI.InternalCatalan.manuscript_case1X2_actual_substitution_error line 870
  77. def OAI.InternalCatalan.manuscriptCase1X3RoundedSubstituteRat line 891
  78. theorem OAI.InternalCatalan.manuscript_case1X3_additional_rounding_error line 894
  79. theorem OAI.InternalCatalan.manuscript_case1X3_actual_substitution_error line 917
  80. def OAI.InternalCatalan.manuscriptCase1X4RoundedSubstituteRat line 938
  81. theorem OAI.InternalCatalan.manuscript_case1X4_additional_rounding_error line 941