OAI/NumberTheory/Catalan/Analysis/ManuscriptNormLogVGroup056.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.InternalCatalan.manuscriptAtanJ_neg line 14
  2. theorem OAI.InternalCatalan.manuscript_atanJ_nonneg_interval line 22
  3. theorem OAI.InternalCatalan.manuscript_atanJ_neg_interval line 51
  4. def OAI.InternalCatalan.manuscriptAtanInterval line 60
  5. def OAI.InternalCatalan.manuscriptPiQuarterInterval line 64
  6. def OAI.InternalCatalan.manuscriptArgInterval line 67
  7. theorem OAI.InternalCatalan.manuscript_atan_interval line 71
  8. theorem OAI.InternalCatalan.manuscript_pi_quarter_interval line 93
  9. theorem OAI.InternalCatalan.manuscript_arg_interval line 103
  10. theorem OAI.InternalCatalan.manuscript_complex_arg_interval line 111
  11. def OAI.InternalCatalan.manuscriptLogHErrorRat line 126
  12. def OAI.InternalCatalan.manuscriptLogHInterval line 130
  13. def OAI.InternalCatalan.manuscriptScaledLogInterval line 133
  14. theorem OAI.InternalCatalan.manuscript_logH_interval line 137
  15. theorem OAI.InternalCatalan.manuscript_scaled_log_interval line 154
  16. theorem OAI.InternalCatalan.manuscript_fixed_log_interval line 166
  17. def OAI.InternalCatalan.manuscriptWeightedComplexLogInterval line 174
  18. theorem OAI.InternalCatalan.manuscript_weighted_complex_log_interval line 179
  19. def OAI.InternalCatalan.manuscriptP00NormLogArg line 203
  20. def OAI.InternalCatalan.manuscriptP00NormLogTerm line 206
  21. def OAI.InternalCatalan.manuscriptP00NormLogInterval line 210
  22. theorem OAI.InternalCatalan.manuscriptP00_arg_eq line 213
  23. theorem OAI.InternalCatalan.manuscriptP00_weight_eq line 218
  24. theorem OAI.InternalCatalan.manuscriptP00_exact_interval line 223
  25. theorem OAI.InternalCatalan.manuscriptP00_rounded_endpoints line 238
  26. theorem OAI.InternalCatalan.manuscriptP00_norm_log_enclosure line 248
  27. def OAI.InternalCatalan.manuscriptNormP0_1Arg line 259
  28. def OAI.InternalCatalan.manuscriptNormP0_1Term line 262
  29. def OAI.InternalCatalan.manuscriptNormP0_1Interval line 266
  30. theorem OAI.InternalCatalan.manuscriptNormP0_1_arg_eq line 269
  31. theorem OAI.InternalCatalan.manuscriptNormP0_1_weight_eq line 273
  32. theorem OAI.InternalCatalan.manuscriptNormP0_1_exact_interval line 278
  33. theorem OAI.InternalCatalan.manuscriptNormP0_1_rounded_endpoints line 293
  34. theorem OAI.InternalCatalan.manuscriptNormP0_1_enclosure line 302
  35. def OAI.InternalCatalan.manuscriptNormP0_2Arg line 312
  36. def OAI.InternalCatalan.manuscriptNormP0_2Term line 315
  37. def OAI.InternalCatalan.manuscriptNormP0_2Interval line 319
  38. theorem OAI.InternalCatalan.manuscriptNormP0_2_arg_eq line 322
  39. theorem OAI.InternalCatalan.manuscriptNormP0_2_weight_eq line 326
  40. theorem OAI.InternalCatalan.manuscriptNormP0_2_exact_interval line 331
  41. theorem OAI.InternalCatalan.manuscriptNormP0_2_rounded_endpoints line 346
  42. theorem OAI.InternalCatalan.manuscriptNormP0_2_enclosure line 355
  43. def OAI.InternalCatalan.manuscriptNormP0_3Arg line 365
  44. def OAI.InternalCatalan.manuscriptNormP0_3Term line 368
  45. def OAI.InternalCatalan.manuscriptNormP0_3Interval line 372
  46. theorem OAI.InternalCatalan.manuscriptNormP0_3_arg_eq line 375
  47. theorem OAI.InternalCatalan.manuscriptNormP0_3_weight_eq line 379
  48. theorem OAI.InternalCatalan.manuscriptNormP0_3_exact_interval line 384
  49. theorem OAI.InternalCatalan.manuscriptNormP0_3_rounded_endpoints line 399
  50. theorem OAI.InternalCatalan.manuscriptNormP0_3_enclosure line 408
  51. def OAI.InternalCatalan.manuscriptNormV12_12Arg line 418
  52. def OAI.InternalCatalan.manuscriptNormV12_12Term line 421
  53. def OAI.InternalCatalan.manuscriptNormV12_12Interval line 425
  54. theorem OAI.InternalCatalan.manuscriptNormV12_12_arg_eq line 428
  55. theorem OAI.InternalCatalan.manuscriptNormV12_12_weight_eq line 432
  56. theorem OAI.InternalCatalan.manuscriptNormV12_12_exact_interval line 437
  57. theorem OAI.InternalCatalan.manuscriptNormV12_12_rounded_endpoints line 452
  58. theorem OAI.InternalCatalan.manuscriptNormV12_12_enclosure line 461