OAI/NumberTheory/Catalan/Analysis/RealEnergyLogSeries.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.InternalCatalan.energy_summable_norm_complex_power_div line 11
  2. theorem OAI.InternalCatalan.energy_hasSum_re_power_div line 23
  3. theorem OAI.InternalCatalan.energy_hasSum_re_power_div_succ line 29
  4. theorem OAI.InternalCatalan.energy_summable_abs_re_power_div line 36
  5. theorem OAI.InternalCatalan.energy_summable_re_power_div line 44
  6. theorem OAI.InternalCatalan.energy_hasSum_real_power_div line 48
  7. theorem OAI.InternalCatalan.energy_hasSum_real_power_div_succ line 58
  8. theorem OAI.InternalCatalan.energy_summable_abs_real_power_div line 64
  9. theorem OAI.InternalCatalan.energy_mul_mem_Ioo line 72
  10. theorem OAI.InternalCatalan.energy_hasSum_mul_power_div line 81
  11. theorem OAI.InternalCatalan.energy_summable_abs_mul_power_div line 87