OAI/Analysis/Triangular/Construction/RepetitionOperators.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AtomicTriangular.Construction.repetitionNorm_nonneg line 10
2. abbrev OAI.AtomicTriangular.Construction.TrigonometricCoefficients line 14
3. def OAI.AtomicTriangular.Construction.AallKernel line 15
4. def OAI.AtomicTriangular.Construction.AallOperator line 17
5. lemma OAI.AtomicTriangular.Construction.AallOperator_norm line 20
6. def OAI.AtomicTriangular.Construction.Akernel line 22
7. def OAI.AtomicTriangular.Construction.Aoperator line 24
8. lemma OAI.AtomicTriangular.Construction.Aoperator_norm line 27
9. def OAI.AtomicTriangular.Construction.CallKernel line 29
10. def OAI.AtomicTriangular.Construction.CallOperator line 31
11. lemma OAI.AtomicTriangular.Construction.CallOperator_norm line 34
12. def OAI.AtomicTriangular.Construction.beta line 36
13. def OAI.AtomicTriangular.Construction.delta line 37
14. lemma OAI.AtomicTriangular.Construction.AC_bound line 38
15. lemma OAI.AtomicTriangular.Construction.AC_all_bound line 44