OAI/Probability/Ballisticity/Estimates/StoppedSplice.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalTransience.independent_diagonal_lintegral line 12
  2. lemma OAI.DirectionalTransience.fresh_rows_diagonal_lintegral line 27
  3. def OAI.DirectionalTransience.rowGraft line 42
  4. lemma OAI.DirectionalTransience.rowGraft_diagonal line 45
  5. lemma OAI.DirectionalTransience.rowGraft_measurable_rows line 48
  6. lemma OAI.DirectionalTransience.rowGraft_measurable line 61
  7. lemma OAI.DirectionalTransience.rowGraft_event_lintegral line 71
  8. def OAI.DirectionalTransience.stoppedRowGraft line 91
  9. lemma OAI.DirectionalTransience.stoppedRowGraft_measurable line 95
  10. theorem OAI.DirectionalTransience.stoppedRowGraft_lintegral line 103
  11. lemma OAI.DirectionalTransience.rowSigma_eq_comap line 149
  12. lemma OAI.DirectionalTransience.rowSigma_event_congr line 164
  13. lemma OAI.DirectionalTransience.rowGraft_rows line 173
  14. lemma OAI.DirectionalTransience.stoppedRowGraft_stop line 176
  15. def OAI.DirectionalTransience.StoppedRowsEvent line 182
  16. lemma OAI.DirectionalTransience.stoppedRowGraft_event line 186
  17. lemma OAI.DirectionalTransience.stoppedRowGraft_observable line 196
  18. lemma OAI.DirectionalTransience.measurable_of_stop_events line 204
  19. theorem OAI.DirectionalTransience.stoppedRowGraft_map line 210
  20. theorem OAI.DirectionalTransience.stoppedRowGraft_joint_map line 222