OAI/Probability/Ballisticity/Estimates/FinitePastDecorrelation.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DirectionalTransience.shared_finite_past_increment_decorrelation line 16
  2. abbrev OAI.DirectionalTransience.RealPathPair line 67
  3. abbrev OAI.DirectionalTransience.JointPastTimes line 68
  4. def OAI.DirectionalTransience.jointPastIncrementMap line 70
  5. def OAI.DirectionalTransience.jointPastProductTest line 86
  6. lemma OAI.DirectionalTransience.weak_joint_past_integral line 91
  7. lemma OAI.DirectionalTransience.joint_past_identity_of_prelimit line 111
  8. def OAI.DirectionalTransience.sharedLinearPairPath line 130
  9. lemma OAI.DirectionalTransience.measurable_sharedLinearPairPath line 135
  10. lemma OAI.DirectionalTransience.recordLinearPath_grid line 140
  11. lemma OAI.DirectionalTransience.jointPastIncrementMap_grid line 146