OAI/Probability/Ballisticity/Estimates/BufferRestorationScript.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalTransience.hitWord_dirac_le_hitKernel line 15
  2. lemma OAI.DirectionalTransience.elliptic_hitWord_dirac_le_hitKernel line 34
  3. lemma OAI.DirectionalTransience.wordPath_lateral_script_end line 44
  4. lemma OAI.DirectionalTransience.wordPath_lateral_script_prefix line 52
  5. lemma OAI.DirectionalTransience.signedHeight_add_nsmul_other line 68
  6. def OAI.DirectionalTransience.bufferRestoreWord line 74
  7. lemma OAI.DirectionalTransience.elliptic_lateral_script line 96
  8. def OAI.DirectionalTransience.pairRestore line 115
  9. lemma OAI.DirectionalTransience.pairRestore_gap line 118
  10. lemma OAI.DirectionalTransience.pairRestore_height line 125
  11. lemma OAI.DirectionalTransience.rawPairEndpointLaw_restoration line 138
  12. def OAI.DirectionalTransience.bufferRestorationLaw line 157
  13. lemma OAI.DirectionalTransience.bufferRestorationLaw_le line 161
  14. lemma OAI.DirectionalTransience.bufferRestorationLaw_mass line 182
  15. lemma OAI.DirectionalTransience.bufferRestorationLaw_support line 187
  16. lemma OAI.DirectionalTransience.bufferRestorationLaw_height line 199
  17. lemma OAI.DirectionalTransience.bufferRestorationLaw_measurable line 209