OAI/Probability/Ballisticity/Estimates/TupleEndpoint.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.TupleKernel.fin_tsum_product line 13
2. lemma OAI.DirectionalTransience.TupleKernel.measurable_countable_measure line 24
3. lemma OAI.DirectionalTransience.TupleKernel.measure_le_of_singletons line 38
4. lemma OAI.DirectionalTransience.TupleKernel.countable_pi_mono line 47
5. lemma OAI.DirectionalTransience.TupleKernel.countable_pi_bind line 56
6. def OAI.DirectionalTransience.rawTupleEndpointLaw line 72
7. lemma OAI.DirectionalTransience.rawTupleEndpointLaw_singleton line 76
8. lemma OAI.DirectionalTransience.rawTupleEndpointLaw_le_one line 81
9. instance OAI.DirectionalTransience.rawTupleEndpointLaw_finite line 88
10. lemma OAI.DirectionalTransience.measurable_rawTupleEndpointLaw line 94
11. def OAI.DirectionalTransience.rawTupleMixture line 104
12. lemma OAI.DirectionalTransience.rawTupleMixture_apply line 108
13. lemma OAI.DirectionalTransience.rawTupleEndpointLaw_comp_le line 113