OAI/NumberTheory/Catalan/Estimates/RealEnergyTwoProduct.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.InternalCatalan.energy_row_weight_coordinate line 13
  2. theorem OAI.InternalCatalan.prod_energy_row_weight_coordinate line 21
  3. theorem OAI.InternalCatalan.energy_quadratic_weight_cancel line 34
  4. theorem OAI.InternalCatalan.prod_energy_quadratic_weight_cancel line 46
  5. theorem OAI.InternalCatalan.energy_abs_node_weight_cancel line 56
  6. def OAI.InternalCatalan.realPrincipalIntegrand line 75
  7. def OAI.InternalCatalan.realEnergyMajorantOne line 84
  8. def OAI.InternalCatalan.realEnergyMajorantTwo line 89
  9. theorem OAI.InternalCatalan.principal_kernel_product_pos line 94
  10. theorem OAI.InternalCatalan.principal_s_weight_pos line 103
  11. theorem OAI.InternalCatalan.principal_t_weight_nonneg line 110
  12. theorem OAI.InternalCatalan.realPrincipalIntegrand_nonneg line 119
  13. theorem OAI.InternalCatalan.realPrincipalIntegrand_pos line 130
  14. theorem OAI.InternalCatalan.abs_sheetRealIntegrand_eq line 171
  15. theorem OAI.InternalCatalan.abs_sheetRealIntegrand_le_majorantOne line 189
  16. theorem OAI.InternalCatalan.realPrincipalIntegrand_coordinate line 208
  17. theorem OAI.InternalCatalan.energy_one_quadratic_weight line 240
  18. theorem OAI.InternalCatalan.realEnergyMajorantOne_coordinate line 252
  19. theorem OAI.InternalCatalan.energy_abs_node_weight_two_cancel line 310
  20. theorem OAI.InternalCatalan.prod_energy_abs_node_weight_two_cancel line 321
  21. theorem OAI.InternalCatalan.realEnergyMajorantTwo_coordinate line 335