OAI/Probability/Ballisticity/Estimates/CountableProdBind.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.countable_prod_bind line 14
2. lemma OAI.DirectionalTransience.rawPairEndpointLaw_comp_le line 39
3. lemma OAI.DirectionalTransience.rawPairMixture_comp_le line 60
4. def OAI.DirectionalTransience.bufferRetentionCost line 82
5. lemma OAI.DirectionalTransience.bufferRetentionCost_pos line 85
6. lemma OAI.DirectionalTransience.bufferChildNode_retained_uniform line 90
7. lemma OAI.DirectionalTransience.bufferNodeAt_retained line 124