OAI/Probability/Ballisticity/Estimates/TwoStopSplice.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalTransience.stop_observable line 12
  2. lemma OAI.DirectionalTransience.upperField_joint_measurable line 26
  3. lemma OAI.DirectionalTransience.belowHeight_mono line 32
  4. theorem OAI.DirectionalTransience.twoStopSplice_fresh line 39
  5. instance OAI.DirectionalTransience.row_standardBorel line 93
  6. def OAI.DirectionalTransience.stoppedObservation line 97
  7. lemma OAI.DirectionalTransience.stoppedObservation_measurable line 101
  8. lemma OAI.DirectionalTransience.rowGraft_fixed_measurable_rows line 107
  9. lemma OAI.DirectionalTransience.stoppedObservation_observable line 113
  10. lemma OAI.DirectionalTransience.stoppedObservation_nested line 128
  11. lemma OAI.DirectionalTransience.stoppedObservation_nested_stop line 140
  12. lemma OAI.DirectionalTransience.stoppedObservation_regraft line 149