OAI/Analysis/Triangular/Envelope/TargetEnvelope.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.AtomicTriangular.Construction.gaussianTarget line 11
2. def OAI.AtomicTriangular.Construction.targetEnvelope line 14
3. lemma OAI.AtomicTriangular.Construction.Q_one_pos line 17
4. lemma OAI.AtomicTriangular.Construction.targetEnvelope_nonneg line 18
5. lemma OAI.AtomicTriangular.Construction.gaussianTarget_pair_bound line 23
6. lemma OAI.AtomicTriangular.Construction.targetEnvelope_enumerate line 56
7. lemma OAI.AtomicTriangular.Construction.targetRatio_lt line 67
8. lemma OAI.AtomicTriangular.Construction.summable_targetEnvelope line 69
9. def OAI.AtomicTriangular.Construction.finiteTargetEnvelope line 76
10. def OAI.AtomicTriangular.Construction.tailTargetEnvelope line 77
11. lemma OAI.AtomicTriangular.Construction.tsum_targetEnvelope line 78
12. lemma OAI.AtomicTriangular.Construction.tailTarget_bounds line 88
13. def OAI.AtomicTriangular.Construction.tailTarget line 95
14. lemma OAI.AtomicTriangular.Construction.tailTarget_norm line 98