OAI/NumberTheory/Catalan/Energy/BarrierLogRatConstants.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.barrierLogH line 27
  2. theorem OAI.InternalCatalan.barrier_hasSum_odd_log line 31
  3. theorem OAI.InternalCatalan.barrier_hasSum_scaled_log line 68
  4. theorem OAI.InternalCatalan.barrier_odd_log_shift_le_geometric line 86
  5. theorem OAI.InternalCatalan.barrier_odd_log_remainder_bounds line 103
  6. theorem OAI.InternalCatalan.barrier_odd_log_remainder_bounds_eighteen line 132
  7. def OAI.InternalCatalan.barrierLogHError line 142
  8. theorem OAI.InternalCatalan.barrier_log_parameter_bounds line 144
  9. theorem OAI.InternalCatalan.barrier_logH_remainder line 152
  10. theorem OAI.InternalCatalan.barrier_logH_remainder_uniform line 169
  11. theorem OAI.InternalCatalan.barrier_logH_error_101_lt line 190
  12. def OAI.InternalCatalan.barrierScaledLogApprox line 198
  13. theorem OAI.InternalCatalan.barrier_scaled_log_abs_error line 201
  14. theorem OAI.InternalCatalan.barrier_scaled_log_abs_error_lt line 224
  15. theorem OAI.InternalCatalan.barrier_log_two_lower line 234
  16. theorem OAI.InternalCatalan.barrier_two_coarse_total_lt line 240
  17. theorem OAI.InternalCatalan.barrier_one_coarse_total_lt line 245
  18. def OAI.InternalCatalan.barrierWeightedComplexLogApprox line 250
  19. theorem OAI.InternalCatalan.barrierComplexLog_re_error line 253
  20. theorem OAI.InternalCatalan.barrierComplexArg_octant_error line 262
  21. theorem OAI.InternalCatalan.barrierComplexLog_weighted_error line 272
  22. def OAI.InternalCatalan.barrierLogHRat line 299
  23. def OAI.InternalCatalan.barrierScaledLogRat line 303
  24. theorem OAI.InternalCatalan.barrierLogHRat_cast line 306
  25. theorem OAI.InternalCatalan.barrierScaledLogRat_cast line 312
  26. theorem OAI.InternalCatalan.barrier_fixed_log_abs_error line 319
  27. theorem OAI.InternalCatalan.barrier_two_coarse_total_sharp_lt line 331
  28. theorem OAI.InternalCatalan.barrier_one_coarse_total_sharp_lt line 336
  29. theorem OAI.InternalCatalan.barrier_sharp_constants_order line 341
  30. def OAI.InternalCatalan.barrierAtanJRat line 348
  31. def OAI.InternalCatalan.barrierArgApproxRat line 351
  32. def OAI.InternalCatalan.barrierWeightedComplexLogRat line 354
  33. theorem OAI.InternalCatalan.barrierAtanJRat_cast line 357
  34. theorem OAI.InternalCatalan.barrierArgApproxRat_cast line 363
  35. theorem OAI.InternalCatalan.barrierWeightedComplexLogRat_cast line 370
  36. theorem OAI.InternalCatalan.barrier_weighted_log_error_allowance line 377
  37. theorem OAI.InternalCatalan.barrierWeightedComplexLogRat_error line 381
  38. theorem OAI.InternalCatalan.barrierLogHRat_two_eq line 414
  39. theorem OAI.InternalCatalan.barrierAtanJRat_half_eq line 418
  40. theorem OAI.InternalCatalan.barrierAtanJRat_third_eq line 422