OAI/Probability/Ballisticity/Crossings/PastCutoffs.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalTransience.nearDiagonalCutoff line 14
  2. lemma OAI.DirectionalTransience.nearDiagonalCutoff_unit line 25
  3. lemma OAI.DirectionalTransience.nearDiagonalCutoff_one line 28
  4. lemma OAI.DirectionalTransience.nearDiagonalCutoff_zero line 34
  5. lemma OAI.DirectionalTransience.nearDiagonalCutoff_uc line 40
  6. def OAI.DirectionalTransience.farDiagonalCutoff line 47
  7. lemma OAI.DirectionalTransience.farDiagonalCutoff_unit line 49
  8. lemma OAI.DirectionalTransience.farDiagonalCutoff_uc line 54
  9. lemma OAI.DirectionalTransience.farDiagonalCutoff_zero line 57
  10. def OAI.DirectionalTransience.currentGapTest line 62
  11. lemma OAI.DirectionalTransience.normalJointPast_gap_second line 65
  12. lemma OAI.DirectionalTransience.abs_mul_le_half_squares line 73
  13. lemma OAI.DirectionalTransience.normalJointPast_cross_integrable line 77
  14. lemma OAI.DirectionalTransience.normalJointPast_weighted_cross_integrable line 103
  15. lemma OAI.DirectionalTransience.normalJointPast_weighted_clip_integrable line 113
  16. lemma OAI.DirectionalTransience.normalJointPast_unclip_error line 131