OAI/NumberTheory/Catalan/Analysis/RealEnergyLogMajorants.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.InternalCatalan.energy_difference_ne_zero_of_lt line 14
  2. theorem OAI.InternalCatalan.energy_vandermonde_product_ne_zero line 18
  3. theorem OAI.InternalCatalan.energy_abs_vandermonde_pos line 27
  4. theorem OAI.InternalCatalan.log_abs_vandermonde line 32
  5. theorem OAI.InternalCatalan.energy_pair_product_pos line 49
  6. theorem OAI.InternalCatalan.log_energy_pair_product line 58
  7. theorem OAI.InternalCatalan.energy_mixed_product_pos line 75
  8. theorem OAI.InternalCatalan.log_energy_mixed_product line 84
  9. theorem OAI.InternalCatalan.energy_s_weight_product_pos line 101
  10. theorem OAI.InternalCatalan.energy_node_weight_product_pos line 108
  11. theorem OAI.InternalCatalan.energy_plain_node_weight_product_pos line 118
  12. theorem OAI.InternalCatalan.energy_quadratic_product_pos line 124
  13. theorem OAI.InternalCatalan.log_energy_s_weight_product line 128
  14. theorem OAI.InternalCatalan.log_energy_node_weight_product line 140
  15. theorem OAI.InternalCatalan.log_energy_plain_node_weight_product line 162
  16. theorem OAI.InternalCatalan.log_energy_quadratic_product line 170
  17. theorem OAI.InternalCatalan.log_realEnergyMajorantOne line 180
  18. theorem OAI.InternalCatalan.log_realEnergyMajorantTwo line 217