OAI/Probability/Ballisticity/Geometry/WindowProjection.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DirectionalTransience.CurrentProfiles line 14
  2. abbrev OAI.DirectionalTransience.CurrentWindow line 17
  3. def OAI.DirectionalTransience.rawCurrentProfiles line 21
  4. lemma OAI.DirectionalTransience.rawCurrentProfileCoordinate_measurable line 25
  5. lemma OAI.DirectionalTransience.rawCurrentProfiles_measurable line 37
  6. def OAI.DirectionalTransience.rawCurrentProjection line 41
  7. lemma OAI.DirectionalTransience.rawCurrentProjection_measurable line 46
  8. def OAI.DirectionalTransience.currentWindowReference line 54
  9. instance OAI.DirectionalTransience.currentWindowReference_markov line 60
  10. lemma OAI.DirectionalTransience.rawCurrentProjection_kl_le line 65
  11. def OAI.DirectionalTransience.actualCurrentWindow line 74
  12. lemma OAI.DirectionalTransience.actualCurrentWindow_measurable line 80
  13. lemma OAI.DirectionalTransience.globalHorizontalCoordinate_stoppedObservation line 95
  14. lemma OAI.DirectionalTransience.actualCurrentWindow_raw line 110
  15. theorem OAI.DirectionalTransience.actualCurrentWindow_law line 126