OAI/Probability/DirectionalWalk/AxisBridges.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalZeroOne.quenched_axis_exit_sum line 12
  2. lemma OAI.DirectionalZeroOne.shiftPath_preimage_hitBefore line 39
  3. lemma OAI.DirectionalZeroOne.axis_barriers_from_top line 43
  4. lemma OAI.DirectionalZeroOne.annealed_axis_return_from_top line 52
  5. lemma OAI.DirectionalZeroOne.firstContactPairs_axis_bound line 67
  6. def OAI.DirectionalZeroOne.translateWord line 81
  7. lemma OAI.DirectionalZeroOne.wordPath_translate line 84
  8. lemma OAI.DirectionalZeroOne.wordEnd_translate line 88
  9. def OAI.DirectionalZeroOne.AxisBridgeWord line 91
  10. lemma OAI.DirectionalZeroOne.axisBridgeWord_recordWord line 95
  11. lemma OAI.DirectionalZeroOne.rawBridgeMeasure_axis_supported line 119
  12. lemma OAI.DirectionalZeroOne.AxisBridgeWord.firstHit line 128
  13. lemma OAI.DirectionalZeroOne.firstContactPairs_of_bridge_contact line 132
  14. def OAI.DirectionalZeroOne.bridgeWordContact line 195
  15. lemma OAI.DirectionalZeroOne.translate_wordCylinder line 198
  16. lemma OAI.DirectionalZeroOne.rawBridgeMeasure_contact_le line 204