OAI/Analysis/Triangular/Construction/Repetition.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AtomicTriangular.Construction.pi_eta_pos line 8
2. def OAI.AtomicTriangular.Construction.repetitionRatio line 9
3. def OAI.AtomicTriangular.Construction.repetitionNorm line 10
4. lemma OAI.AtomicTriangular.Construction.repetitionRatio_pos line 11
5. lemma OAI.AtomicTriangular.Construction.repetitionRatio_lt line 12
6. lemma OAI.AtomicTriangular.Construction.repetitionNorm_eq line 15
7. def OAI.AtomicTriangular.Construction.repetitionEnvelope line 22
8. lemma OAI.AtomicTriangular.Construction.repetitionEnvelope_nonneg line 25
9. lemma OAI.AtomicTriangular.Construction.repetitionEnvelope_enumerate line 30
10. lemma OAI.AtomicTriangular.Construction.summable_repetitionEnvelope line 46
11. lemma OAI.AtomicTriangular.Construction.tsum_repetitionEnvelope line 55
12. lemma OAI.AtomicTriangular.Construction.repetitionEnvelope_bound line 70
13. def OAI.AtomicTriangular.Construction.repetitionEntry line 81
14. lemma OAI.AtomicTriangular.Construction.repetitionEntry_bound line 84
15. def OAI.AtomicTriangular.Construction.repetitionKernel line 87
16. lemma OAI.AtomicTriangular.Construction.repetitionKernel_pair line 90
17. lemma OAI.AtomicTriangular.Construction.repetitionKernel_bounds line 97