OAI/NumberTheory/Catalan/Estimates/TwoAdicQuadratic.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.n line 17
  2. def OAI.InternalCatalan.a line 18
  3. def OAI.InternalCatalan.b line 19
  4. def OAI.InternalCatalan.q line 20
  5. def OAI.InternalCatalan.g line 21
  6. def OAI.InternalCatalan.h line 22
  7. def OAI.InternalCatalan.L line 23
  8. def OAI.InternalCatalan.Cdegree line 24
  9. def OAI.InternalCatalan.H line 25
  10. def OAI.InternalCatalan.A line 26
  11. def OAI.InternalCatalan.rowOffset line 28
  12. def OAI.InternalCatalan.rowDistance line 29
  13. theorem OAI.InternalCatalan.L_eq_n_add_a line 31
  14. theorem OAI.InternalCatalan.L_eq_n_add_b_add_q line 35
  15. theorem OAI.InternalCatalan.Cdegree_eq_L_add_g line 39
  16. theorem OAI.InternalCatalan.H_eq_Cdegree_add_h line 43
  17. theorem OAI.InternalCatalan.A_eq_a_add_two_mul_g line 47
  18. theorem OAI.InternalCatalan.Cdegree_pos line 51
  19. theorem OAI.InternalCatalan.rawColumn_lt_L line 55
  20. theorem OAI.InternalCatalan.rawColumn_ge_b line 60
  21. theorem OAI.InternalCatalan.rowDistance_le line 62
  22. theorem OAI.InternalCatalan.rowDistance_lt_Cdegree line 67
  23. theorem OAI.InternalCatalan.A_le_reversed_T_min line 73
  24. theorem OAI.InternalCatalan.A_add_one_le_reversed_U_min line 79
  25. theorem OAI.InternalCatalan.contactOrder_eq line 86
  26. theorem OAI.InternalCatalan.contactOrder_ge_L line 92
  27. theorem OAI.InternalCatalan.auxiliary_rowDistance line 97
  28. theorem OAI.InternalCatalan.auxiliary_reversed_T_min line 98
  29. theorem OAI.InternalCatalan.auxiliary_reversed_U_min line 99
  30. theorem OAI.InternalCatalan.energy_abs_node_exponent line 102
  31. theorem OAI.InternalCatalan.energy_parameter_ratios line 108
  32. theorem OAI.InternalCatalan.energy_quadratic_exponent line 119
  33. theorem OAI.InternalCatalan.energy_power_two_constant line 128
  34. theorem OAI.InternalCatalan.energy_constant_after_squares line 139
  35. theorem OAI.InternalCatalan.energy_log_one_add_sq_bounds line 152
  36. theorem OAI.InternalCatalan.realEnergyFiniteCorrection_bounds line 160
  37. theorem OAI.InternalCatalan.twoAdicQuadratic_lower line 203