OAI/NumberTheory/Catalan/Analysis/RealEnergyKernelSeries.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.InternalCatalan.energy_scaled_pow_re line 12
2. theorem OAI.InternalCatalan.energy_hasSum_cosine_kernel line 17
3. theorem OAI.InternalCatalan.energy_summable_abs_cosine_kernel line 47
4. theorem OAI.InternalCatalan.realEnergy_circle_scaled_chord_sq line 54
5. theorem OAI.InternalCatalan.energy_hasSum_cross_kernel line 66
6. theorem OAI.InternalCatalan.energy_summable_abs_cross_kernel line 85