OAI/Probability/SKGap/Terminal/SpinChebyshev.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGapCutoff.spinChebyshev line 173
2. lemma OAI.SKGapCutoff.spinChebyshev_zero line 176
3. lemma OAI.SKGapCutoff.spinChebyshev_one line 177
4. lemma OAI.SKGapCutoff.spinChebyshev_recurrence line 178
5. lemma OAI.SKGapCutoff.spinChebyshev_cos line 182
6. lemma OAI.SKGapCutoff.abs_sin_nat_mul_le line 191
7. lemma OAI.SKGapCutoff.spinChebyshev_abs_le line 208
8. lemma OAI.SKGapCutoff.spinChebyshev_series_majorant line 230
9. lemma OAI.SKGapCutoff.spinChebyshev_term_bound line 237
10. lemma OAI.SKGapCutoff.spinChebyshev_series_summable line 243
11. lemma OAI.SKGapCutoff.spinChebyshev_series_uniform line 249
12. lemma OAI.SKGapCutoff.spinChebyshev_generating_series line 257
13. lemma OAI.SKGapCutoff.semicircle_integral line 285
14. lemma OAI.SKGapCutoff.semicircleDensity_two_cos line 297
15. lemma OAI.SKGapCutoff.semicircle_integral_angular line 305
16. lemma OAI.SKGapCutoff.integral_cos_integer_frequency line 332
17. lemma OAI.SKGapCutoff.integral_sin_nat_frequencies line 338
18. theorem OAI.SKGapCutoff.spinChebyshev_orthonormal line 366
19. lemma OAI.SKGapCutoff.semicircle_ae_mem line 383
20. theorem OAI.SKGapCutoff.spinCovariance_density_moment line 390
21. lemma OAI.SKGapCutoff.spinChebyshev_degree line 427
22. lemma OAI.SKGapCutoff.spinChebyshev_leadingCoeff line 441
23. lemma OAI.SKGapCutoff.spinChebyshev_span line 452
24. lemma OAI.SKGapCutoff.integrable_of_continuousOn_semicircle_support line 459
25. lemma OAI.SKGapCutoff.integrable_spinCovariance_polynomial line 465
26. theorem OAI.SKGapCutoff.spinCovariance_polynomial_of_moments line 471