OAI/NumberTheory/Catalan/Energy/BarrierChebyshevLogFormula.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.InternalCatalan.barrier_log_mul_of_re_pos line 19
  2. theorem OAI.InternalCatalan.barrier_chebyshev_quadratic_log line 36
  3. theorem OAI.InternalCatalan.circle_power_add_conj line 65
  4. theorem OAI.InternalCatalan.barrier_hasSum_chebyshev_log line 80
  5. theorem OAI.InternalCatalan.barrier_summable_chebyshev_log line 107
  6. theorem OAI.InternalCatalan.barrierFiniteCoeff_T_hasSum line 118
  7. theorem OAI.InternalCatalan.barrierTailRow_T_hasSum line 135
  8. theorem OAI.InternalCatalan.barrierTail_T_hasSum line 151
  9. theorem OAI.InternalCatalan.barrierTrialT_eq_finite_log line 170
  10. theorem OAI.InternalCatalan.barrierP2_T_eq_finite_log line 187
  11. theorem OAI.InternalCatalan.barrierV2_T_eq_finite_log line 198