OAI/Probability/Ballisticity/Estimates/EndpointPrefixConditionedReal.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.endpointPrefix_conditioned_real line 241
2. lemma OAI.DirectionalTransience.endpointPrefix_bad_le_tube_bad line 251
3. lemma OAI.DirectionalTransience.favorable_endpoint_gap line 261
4. lemma OAI.DirectionalTransience.endpointPrefix_firstLayer line 286
5. lemma OAI.DirectionalTransience.endpoint_rectangle_le_layerPair line 321
6. theorem OAI.DirectionalTransience.shared_raw_layer_truth_domination line 340