OAI/Probability/Ballisticity/Estimates/JointPastMoments.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalTransience.pairPastCoordinates line 14
  2. def OAI.DirectionalTransience.pairPathIncrement line 18
  3. lemma OAI.DirectionalTransience.jointPastIncrementMap_eq line 21
  4. def OAI.DirectionalTransience.NormalJointPast line 25
  5. lemma OAI.DirectionalTransience.normal_past_of_uc_tests line 31
  6. lemma OAI.DirectionalTransience.product_law_integral_mul line 43
  7. lemma OAI.DirectionalTransience.product_law_integrable_mul line 55
  8. lemma OAI.DirectionalTransience.normalJointPast_moment line 67
  9. lemma OAI.DirectionalTransience.gaussianReal_second_moment line 87
  10. lemma OAI.DirectionalTransience.normalJointPast_hasLaw line 93
  11. lemma OAI.DirectionalTransience.normalJointPast_integrable_abs_pow line 104
  12. lemma OAI.DirectionalTransience.normalJointPast_absolute_third_moment line 114
  13. lemma OAI.DirectionalTransience.normalJointPast_mean line 126
  14. lemma OAI.DirectionalTransience.normalJointPast_second line 133