OAI/Probability/Ballisticity/Estimates/PairPrefix.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalTransience.ae_of_pair_prefix_probability_lower line 12
  2. lemma OAI.DirectionalTransience.shared_pair_record_cylinder_noDrop line 55
  3. def OAI.DirectionalTransience.pairPrefix line 121
  4. lemma OAI.DirectionalTransience.measurable_pairPrefix line 125
  5. lemma OAI.DirectionalTransience.pairPrefix_fiber line 129
  6. lemma OAI.DirectionalTransience.measure_partition_pairprefix line 137
  7. def OAI.DirectionalTransience.PairPrefixDetermined line 153
  8. lemma OAI.DirectionalTransience.shared_pair_record_event_noDrop_lower line 156
  9. lemma OAI.DirectionalTransience.annealedFrom_ae_of_quenched line 200
  10. lemma OAI.DirectionalTransience.sharedPairLaw_fst line 211
  11. lemma OAI.DirectionalTransience.sharedPairLaw_snd line 221
  12. lemma OAI.DirectionalTransience.shared_pair_ae line 231
  13. def OAI.DirectionalTransience.FirstLayerHit line 240
  14. lemma OAI.DirectionalTransience.measurableSet_firstLayerHit line 243
  15. lemma OAI.DirectionalTransience.firstLayerHit_prefix line 250
  16. lemma OAI.DirectionalTransience.firstLayerHit_disjoint line 257
  17. lemma OAI.DirectionalTransience.firstLayerHit_record line 270
  18. lemma OAI.DirectionalTransience.firstLayerHit_exists line 277
  19. lemma OAI.DirectionalTransience.firstLayerHit_after_prefix line 301
  20. lemma OAI.DirectionalTransience.shared_pair_layer_hits line 309
  21. def OAI.DirectionalTransience.CommonTrueAbove line 331
  22. lemma OAI.DirectionalTransience.measurableSet_commonTrueAbove line 334
  23. lemma OAI.DirectionalTransience.finite_pair_prefix_height_bound line 345
  24. lemma OAI.DirectionalTransience.pairPrefixDetermined_inter line 372
  25. lemma OAI.DirectionalTransience.pairPrefixDetermined_product line 378
  26. lemma OAI.DirectionalTransience.prefixDetermined_cylinder_of_le line 384
  27. lemma OAI.DirectionalTransience.firstLayerHit_pair_disjoint line 393
  28. lemma OAI.DirectionalTransience.shared_pair_common_true_after_prefix line 405