OAI/Probability/FirstPassage/EndpointTail.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PlanarFPP.endpointErrorTerm line 10
2. def OAI.PlanarFPP.endpointErrorTail line 11
3. lemma OAI.PlanarFPP.endpointErrorTerm_nonneg line 13
4. lemma OAI.PlanarFPP.summable_endpointErrorTerm line 17
5. lemma OAI.PlanarFPP.endpointErrorTail_tendsto line 20
6. lemma OAI.PlanarFPP.endpointErrorTail_nonneg line 23
7. lemma OAI.PlanarFPP.endpointErrorTerm_le_two line 26
8. lemma OAI.PlanarFPP.gridWidth_endpointError line 42
9. lemma OAI.PlanarFPP.endpointError_sum_le_tail line 52