OAI/Analysis/Triangular/Schwartz/Regularity.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AtomicTriangular.Construction.norm_two_sin_le line 10
2. def OAI.AtomicTriangular.Construction.stripBound line 20
3. lemma OAI.AtomicTriangular.Construction.stripBound_nonneg line 22
4. lemma OAI.AtomicTriangular.Construction.P_strip_bound line 24
5. lemma OAI.AtomicTriangular.Construction.im_le_dist_int line 44
6. lemma OAI.AtomicTriangular.Construction.uniform_basis_bound line 47
7. def OAI.AtomicTriangular.Construction.spectralBound line 84
8. lemma OAI.AtomicTriangular.Construction.spectralBound_nonneg line 86
9. lemma OAI.AtomicTriangular.Construction.finiteSpectral_strip line 88
10. lemma OAI.AtomicTriangular.Construction.tail_summand_norm_bound line 103
11. lemma OAI.AtomicTriangular.Construction.differentiable_tailInput line 116
12. lemma OAI.AtomicTriangular.Construction.tailInput_strip line 133
13. lemma OAI.AtomicTriangular.Construction.differentiable_finiteInput line 147
14. lemma OAI.AtomicTriangular.Construction.finiteInput_strip line 153
15. def OAI.AtomicTriangular.Construction.inputSchwartz line 166
16. lemma OAI.AtomicTriangular.Construction.inputSchwartz_apply line 172