OAI/NumberTheory/Catalan/Estimates/RealEnergyChebyshev.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.InternalCatalan.energy_chord_sq_identity line 18
  2. theorem OAI.InternalCatalan.energy_chord_sq_le line 28
  3. theorem OAI.InternalCatalan.energy_damped_chord_pos line 33
  4. theorem OAI.InternalCatalan.energy_log_chord_le line 41
  5. def OAI.InternalCatalan.realEnergyCirclePoint line 61
  6. theorem OAI.InternalCatalan.realEnergyCirclePoint_norm line 64
  7. theorem OAI.InternalCatalan.realEnergyCirclePoint_add_conj line 72
  8. theorem OAI.InternalCatalan.realEnergyCirclePoint_mul_conj line 77
  9. theorem OAI.InternalCatalan.realEnergyCirclePoint_quadratic line 82
  10. theorem OAI.InternalCatalan.realEnergy_cosine_chord_product line 90
  11. def OAI.InternalCatalan.realEnergyCosineKernel line 113
  12. theorem OAI.InternalCatalan.realEnergyCosineKernel_one line 118
  13. theorem OAI.InternalCatalan.realEnergyCosineKernel_compare line 134
  14. theorem OAI.InternalCatalan.realEnergyCirclePoint_pow_re line 169
  15. theorem OAI.InternalCatalan.energy_chebyshev_abs_le_one line 195
  16. theorem OAI.InternalCatalan.realEnergyCirclePoint_pair_pow_re line 202