OAI/NumberTheory/PiExponent/Analysis/PeriodAnalytic.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponent.PeriodAnalytic.periodSeries line 11
2. def OAI.PiExponent.PeriodAnalytic.periodFunction line 15
3. theorem OAI.PiExponent.PeriodAnalytic.hasSum_coeff_C line 18
4. theorem OAI.PiExponent.PeriodAnalytic.hasSum_coeff_X line 24
5. theorem OAI.PiExponent.PeriodAnalytic.hasSum_coeff_add line 30
6. theorem OAI.PiExponent.PeriodAnalytic.hasSum_periodSeries line 36
7. theorem OAI.PiExponent.PeriodAnalytic.analyticAt_periodFunction line 44
8. theorem OAI.PiExponent.PeriodAnalytic.hasFPowerSeriesAt_periodFunction line 52
9. theorem OAI.PiExponent.PeriodAnalytic.rowTest_periodFunction_eq_coeff line 62
10. theorem OAI.PiExponent.PeriodAnalytic.rowTest_congr_sphere line 79
11. theorem OAI.PiExponent.PeriodAnalytic.periodFunction_eq_exponentialMonomial line 90
12. theorem OAI.PiExponent.PeriodAnalytic.exp_period_center line 101
13. theorem OAI.PiExponent.PeriodAnalytic.rowTest_exponentialMonomial_eq_coeff line 105
14. theorem OAI.PiExponent.PeriodAnalytic.periodMonomial_coeff_eq_rowTest line 118
15. theorem OAI.PiExponent.PeriodAnalytic.norm_binomial_product_le line 128
16. def OAI.PiExponent.PeriodAnalytic.columnFunction line 137
17. theorem OAI.PiExponent.PeriodAnalytic.differentiable_columnFunction line 142
18. theorem OAI.PiExponent.PeriodAnalytic.norm_columnFunction_le line 146