OAI/Probability/Ballisticity/Estimates/RawPair.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.hitKernel_height_zero line 14
2. lemma OAI.DirectionalTransience.rawPairEndpointLaw_zero line 47
3. lemma OAI.DirectionalTransience.rawPairMixture_zero line 51
4. lemma OAI.DirectionalTransience.pairKernelMass_zero_of_supported line 58
5. def OAI.DirectionalTransience.bufferStageRetainedLaw line 75
6. lemma OAI.DirectionalTransience.bufferFirstFailure_eq_top_of_pass line 87
7. lemma OAI.DirectionalTransience.bufferStageEvent_iff_last_tests line 98
8. lemma OAI.DirectionalTransience.bufferStageRetainedLaw_le line 118
9. lemma OAI.DirectionalTransience.bufferStageRetainedLaw_mass_lower line 140