OAI/NumberTheory/Catalan/Analysis/ManuscriptActualLogScaling.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.ManuscriptPrecision.ComplexLogInputRange line 12
  2. theorem OAI.InternalCatalan.ManuscriptPrecision.range_of_norm_bounds line 16
  3. theorem OAI.InternalCatalan.ManuscriptPrecision.linear_log_argument_range line 26
  4. theorem OAI.InternalCatalan.ManuscriptPrecision.quadratic_log_argument_range line 40
  5. theorem OAI.InternalCatalan.ManuscriptPrecision.pair_log_argument_range line 62
  6. theorem OAI.InternalCatalan.ManuscriptPrecision.complex_log_input_power_range line 74
  7. theorem OAI.InternalCatalan.ManuscriptPrecision.actual_XP_log_argument_range line 81
  8. theorem OAI.InternalCatalan.ManuscriptPrecision.actual_XV_log_argument_range line 87
  9. theorem OAI.InternalCatalan.ManuscriptPrecision.actual_YV_log_argument_range line 93
  10. theorem OAI.InternalCatalan.ManuscriptPrecision.actual_P_norm_log_argument_range line 99
  11. theorem OAI.InternalCatalan.ManuscriptPrecision.actual_V_norm_log_argument_range line 106
  12. def OAI.InternalCatalan.ManuscriptPrecision.paperXPoints line 113
  13. def OAI.InternalCatalan.ManuscriptPrecision.paperYPoints line 116
  14. theorem OAI.InternalCatalan.ManuscriptPrecision.paper_point_counts line 119
  15. theorem OAI.InternalCatalan.ManuscriptPrecision.paper_X_point_margins line 122
  16. theorem OAI.InternalCatalan.ManuscriptPrecision.paper_Y_point_margins line 127
  17. def OAI.InternalCatalan.ManuscriptPrecision.XRealLogInputs line 131
  18. def OAI.InternalCatalan.ManuscriptPrecision.YRealLogInputs line 133
  19. theorem OAI.InternalCatalan.ManuscriptPrecision.actual_X_real_log_input_range line 135
  20. theorem OAI.InternalCatalan.ManuscriptPrecision.actual_Y_real_log_input_range line 147
  21. theorem OAI.InternalCatalan.ManuscriptPrecision.real_log_input_power_range line 156
  22. theorem OAI.InternalCatalan.ManuscriptPrecision.all_XP_point_log_input_ranges line 162
  23. theorem OAI.InternalCatalan.ManuscriptPrecision.all_XV_point_log_input_ranges line 169
  24. theorem OAI.InternalCatalan.ManuscriptPrecision.all_YV_point_log_input_ranges line 176
  25. theorem OAI.InternalCatalan.ManuscriptPrecision.actual_X_real_log_scaling line 184
  26. theorem OAI.InternalCatalan.ManuscriptPrecision.actual_Y_real_log_scaling line 192
  27. theorem OAI.InternalCatalan.ManuscriptPrecision.complex_log_input_scaling line 200
  28. theorem OAI.InternalCatalan.ManuscriptPrecision.rational_complex_log_input_scaling line 207