OAI/Probability/Ballisticity/Estimates/ProductNormalJointPast.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalTransience.pathPastCoordinates line 14
  2. def OAI.DirectionalTransience.pathIncrement line 17
  3. def OAI.DirectionalTransience.NormalSinglePast line 20
  4. lemma OAI.DirectionalTransience.normalJointPast_single line 26
  5. lemma OAI.DirectionalTransience.normalSinglePast_prod line 39
  6. def OAI.DirectionalTransience.pairRestricted line 72
  7. def OAI.DirectionalTransience.pairIncrement line 75
  8. lemma OAI.DirectionalTransience.fullNormalJointPast_finset line 78
  9. lemma OAI.DirectionalTransience.pairRestricted_empty_map line 104
  10. lemma OAI.DirectionalTransience.pairRestricted_singleton_zero_map line 111
  11. lemma OAI.DirectionalTransience.pairRestricted_mono_eq line 131
  12. def OAI.DirectionalTransience.pairExtend line 141
  13. lemma OAI.DirectionalTransience.pairExtend_measurable line 146
  14. lemma OAI.DirectionalTransience.pairExtend_eval line 152
  15. lemma OAI.DirectionalTransience.pairRestricted_insert_eq line 159
  16. lemma OAI.DirectionalTransience.fullNormalJointPast_finite_uniqueness line 175