OAI/Probability/Ballisticity/Estimates/WordConcatenation.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DirectionalTransience.CoordinateWord line 13
  2. def OAI.DirectionalTransience.ValidWordSplit line 16
  3. abbrev OAI.DirectionalTransience.CoordinateSplit line 24
  4. def OAI.DirectionalTransience.coordinateSplitFirst line 27
  5. def OAI.DirectionalTransience.coordinateSplitSecond line 30
  6. def OAI.DirectionalTransience.coordinateWordConcat line 34
  7. lemma OAI.DirectionalTransience.coordinateWordConcat_injective line 39
  8. lemma OAI.DirectionalTransience.TupleKernel.atomic_injection_sum_le line 54
  9. lemma OAI.DirectionalTransience.TupleKernel.countable_map_apply line 62
  10. lemma OAI.DirectionalTransience.TupleKernel.countable_restricted_map_le line 74
  11. def OAI.DirectionalTransience.rawWordPairLaw line 101
  12. lemma OAI.DirectionalTransience.rawWordPairLaw_singleton line 106
  13. lemma OAI.DirectionalTransience.rawWordPairLaw_invalid line 134
  14. lemma OAI.DirectionalTransience.rawWordPairLaw_valid line 148
  15. lemma OAI.DirectionalTransience.rawWordLaw_comp_le line 159