OAI/Probability/Ballisticity/Estimates/RelativeBudget.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalTransience.relativeWordDisplacement line 12
  2. def OAI.DirectionalTransience.TupleRelativeBudget line 16
  3. def OAI.DirectionalTransience.TupleSeparated line 21
  4. def OAI.DirectionalTransience.tupleWordEndpoint line 24
  5. lemma OAI.DirectionalTransience.relativeWordDisplacement_endpoint line 28
  6. lemma OAI.DirectionalTransience.relativeWordDisplacement_append_prefix line 34
  7. lemma OAI.DirectionalTransience.relativeWordDisplacement_append_suffix line 42
  8. lemma OAI.DirectionalTransience.tupleRelativeBudget_append line 57
  9. lemma OAI.DirectionalTransience.tupleRelativeBudget_separation line 86
  10. def OAI.DirectionalTransience.relativeBudgetWordLaw line 108
  11. def OAI.DirectionalTransience.relativeBudgetEndpointLaw line 113
  12. instance OAI.DirectionalTransience.relativeBudgetWordLaw_finite line 118
  13. instance OAI.DirectionalTransience.relativeBudgetEndpointLaw_finite line 124
  14. lemma OAI.DirectionalTransience.relativeBudgetEndpointLaw_le line 130
  15. def OAI.DirectionalTransience.TupleKernel.dependentPair line 147
  16. lemma OAI.DirectionalTransience.TupleKernel.dependentPair_singleton line 151
  17. lemma OAI.DirectionalTransience.TupleKernel.restrict_singleton line 176
  18. def OAI.DirectionalTransience.rawTupleSplitLaw line 186
  19. lemma OAI.DirectionalTransience.rawTupleSplitLaw_singleton line 192
  20. def OAI.DirectionalTransience.ValidTupleSplit line 198
  21. def OAI.DirectionalTransience.tupleWordConcat line 202
  22. lemma OAI.DirectionalTransience.tupleWordConcat_injOn line 206
  23. lemma OAI.DirectionalTransience.rawTupleSplitLaw_invalid line 216
  24. lemma OAI.DirectionalTransience.rawTupleSplitLaw_valid line 225
  25. lemma OAI.DirectionalTransience.rawTupleWordLaw_comp_le line 235
  26. def OAI.DirectionalTransience.relativeBudgetSplitLaw line 244
  27. lemma OAI.DirectionalTransience.relativeBudgetWordLaw_singleton line 250
  28. lemma OAI.DirectionalTransience.relativeBudgetSplitLaw_singleton line 256
  29. lemma OAI.DirectionalTransience.relativeBudgetWordLaw_comp_le line 268