OAI/Analysis/Triangular/Taylor/CoefficientSpectral.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AtomicTriangular.Construction.finiteColumn_even line 11
2. lemma OAI.AtomicTriangular.Construction.finiteColumn_odd line 17
3. lemma OAI.AtomicTriangular.Construction.sum_fin22_pairs line 23
4. lemma OAI.AtomicTriangular.Construction.finiteSpectral_coefficient line 32
5. lemma OAI.AtomicTriangular.Construction.finiteSpectral_coefficient_apply line 42
6. lemma OAI.AtomicTriangular.Construction.tailSpectral_coefficient line 48
7. lemma OAI.AtomicTriangular.Construction.tailSpectral_zero_coeff line 51
8. lemma OAI.AtomicTriangular.Construction.complex_smul_clm_bound line 55
9. lemma OAI.AtomicTriangular.Construction.tail_pair_norm119 line 62
10. lemma OAI.AtomicTriangular.Construction.norm_series_bound line 73
11. lemma OAI.AtomicTriangular.Construction.tailSeries_norm line 78
12. lemma OAI.AtomicTriangular.Construction.tailSpectral_zero_constant line 85
13. lemma OAI.AtomicTriangular.Construction.tailSpectral_zero_constant_norm line 95
14. lemma OAI.AtomicTriangular.Construction.finiteSpectral_wave_bound line 99