OAI/NumberTheory/Catalan/Estimates/RealEnergyDiagonal.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.realCoordinate line 22
  2. def OAI.InternalCatalan.realCoordinateInv line 24
  3. theorem OAI.InternalCatalan.coordinate_radicand_pos line 26
  4. theorem OAI.InternalCatalan.realCoordinateInv_mem line 33
  5. theorem OAI.InternalCatalan.sqrt_one_sub_realCoordinateInv_sq line 44
  6. theorem OAI.InternalCatalan.realCoordinate_mem line 54
  7. theorem OAI.InternalCatalan.realCoordinate_left_inverse line 66
  8. theorem OAI.InternalCatalan.realCoordinate_right_inverse line 78
  9. theorem OAI.InternalCatalan.realCoordinate_bijOn line 91
  10. theorem OAI.InternalCatalan.hasDerivAt_realCoordinateInv line 100
  11. theorem OAI.InternalCatalan.continuous_realCoordinateInv line 116
  12. theorem OAI.InternalCatalan.realCoordinate_weight_jacobian line 120
  13. theorem OAI.InternalCatalan.realCoordinateInv_denominator_pos line 141
  14. theorem OAI.InternalCatalan.abs_realCoordinateInv line 144
  15. theorem OAI.InternalCatalan.realCoordinateInv_sub line 151
  16. theorem OAI.InternalCatalan.energy_one_sub_mul_pos line 160
  17. theorem OAI.InternalCatalan.abs_realCoordinateInv_sub line 171
  18. theorem OAI.InternalCatalan.one_sub_realCoordinateInv_mul line 182
  19. theorem OAI.InternalCatalan.one_sub_realCoordinateInv line 189
  20. theorem OAI.InternalCatalan.realCoordinateInv_kernel_numerator_pos line 196
  21. theorem OAI.InternalCatalan.realCoordinateInv_kernel_pos line 202
  22. theorem OAI.InternalCatalan.one_sub_realCoordinateInv_pos line 208
  23. def OAI.InternalCatalan.realEnergyTau line 212
  24. def OAI.InternalCatalan.realEnergyRho line 213
  25. def OAI.InternalCatalan.realEnergySigma line 214
  26. theorem OAI.InternalCatalan.realEnergyTau_bounds line 216
  27. theorem OAI.InternalCatalan.realEnergyRho_bounds line 221
  28. theorem OAI.InternalCatalan.realEnergyRho_mem line 229
  29. theorem OAI.InternalCatalan.realEnergySigma_bounds line 234
  30. theorem OAI.InternalCatalan.realEnergySigma_mem line 246
  31. theorem OAI.InternalCatalan.realEnergyRho_mul_bounds line 251
  32. theorem OAI.InternalCatalan.realEnergySigma_mul_bounds line 267
  33. theorem OAI.InternalCatalan.prod_pair_factors line 287
  34. theorem OAI.InternalCatalan.prod_pair_const line 306
  35. theorem OAI.InternalCatalan.abs_inv_sub_inv_eq line 319
  36. theorem OAI.InternalCatalan.abs_vandermonde_inv line 326
  37. theorem OAI.InternalCatalan.prod_realCoordinateInv_kernel line 336
  38. theorem OAI.InternalCatalan.abs_vandermonde_realCoordinateInv line 343
  39. theorem OAI.InternalCatalan.energy_cross_relative_size line 366
  40. theorem OAI.InternalCatalan.realEnergy_cross_node_error line 415
  41. theorem OAI.InternalCatalan.realEnergy_cross_quadratic_le line 450
  42. theorem OAI.InternalCatalan.realEnergy_cross_kernel_le line 489
  43. theorem OAI.InternalCatalan.energy_log_opposite_sign line 505
  44. theorem OAI.InternalCatalan.energy_damped_power_pos line 525
  45. theorem OAI.InternalCatalan.realEnergy_power_kernel_le line 533
  46. theorem OAI.InternalCatalan.realEnergy_power_diagonal_nonneg_side line 566
  47. theorem OAI.InternalCatalan.realEnergy_power_diagonal_nonpos_side line 576
  48. theorem OAI.InternalCatalan.realEnergy_log_power_diagonal_ge line 593
  49. theorem OAI.InternalCatalan.realEnergy_sigma_diagonal_ge line 608
  50. theorem OAI.InternalCatalan.realEnergy_log_sigma_diagonal_ge line 621