OAI/Probability/Ballisticity/Estimates/EndpointPrefix.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DirectionalTransience.EndpointPrefix line 236
2. lemma OAI.DirectionalTransience.measurableSet_endpointPrefix line 239
3. lemma OAI.DirectionalTransience.coordinate_hitAt_record line 242
4. lemma OAI.DirectionalTransience.jointTubeMass_le_endpoint line 293
5. lemma OAI.DirectionalTransience.endpointPrefix_conditioned_recenter line 310
6. lemma OAI.DirectionalTransience.integral_product_lower_of_small_bad line 343
7. lemma OAI.DirectionalTransience.scalar_pair_tail_one_side line 372
8. lemma OAI.DirectionalTransience.annealedFrom_real_integral line 404
9. lemma OAI.DirectionalTransience.sharedPairLaw_real_rectangle line 412
10. lemma OAI.DirectionalTransience.shared_endpoint_overlap line 423