OAI/Probability/GammaPassage/EndpointTail.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.GammaFPP.CrossingBridge.endpointErrorTerm line 11
2. def OAI.GammaFPP.CrossingBridge.endpointErrorTail line 12
3. lemma OAI.GammaFPP.CrossingBridge.endpointErrorTerm_nonneg line 14
4. lemma OAI.GammaFPP.CrossingBridge.summable_endpointErrorTerm line 18
5. lemma OAI.GammaFPP.CrossingBridge.endpointErrorTail_tendsto line 21
6. lemma OAI.GammaFPP.CrossingBridge.endpointErrorTail_nonneg line 24
7. lemma OAI.GammaFPP.CrossingBridge.endpointErrorTerm_le_two line 27
8. lemma OAI.GammaFPP.CrossingBridge.gridWidth_endpointError line 43
9. lemma OAI.GammaFPP.CrossingBridge.endpointError_sum_le_tail line 53