OAI/Probability/Ballisticity/Estimates/BufferTree.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalTransience.bufferNodeAt line 15
  2. lemma OAI.DirectionalTransience.bufferNodeAt_radius line 22
  3. lemma OAI.DirectionalTransience.bufferNodeAt_valid line 30
  4. def OAI.DirectionalTransience.bufferNodeDecision line 42
  5. lemma OAI.DirectionalTransience.mem_bufferChildNode_iff line 47
  6. def OAI.DirectionalTransience.bufferHistory line 58
  7. lemma OAI.DirectionalTransience.bufferHistory_length line 65
  8. lemma OAI.DirectionalTransience.bufferNodeAt_active_iff_history line 73
  9. abbrev OAI.DirectionalTransience.BufferWords line 99
  10. def OAI.DirectionalTransience.bufferTreeSuccess line 101
  11. lemma OAI.DirectionalTransience.bufferTreeSuccess_measurable line 107
  12. lemma OAI.DirectionalTransience.bufferWords_partition line 125
  13. lemma OAI.DirectionalTransience.bufferTreeSuccess_iff_decision line 154
  14. def OAI.DirectionalTransience.bufferWordSuccesses line 174
  15. lemma OAI.DirectionalTransience.bufferWordSuccesses_history line 178
  16. lemma OAI.DirectionalTransience.buffer_failureWeight_on_branch line 191