OAI/Probability/Ballisticity/Estimates/BudgetAdapted.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DirectionalTransience.SupportedTupleMeasures line 13
  2. lemma OAI.DirectionalTransience.supportedTupleMeasures_singleton line 16
  3. lemma OAI.DirectionalTransience.relativeBudgetWordLaw_rows line 23
  4. def OAI.DirectionalTransience.relativeBudgetMassENN line 41
  5. lemma OAI.DirectionalTransience.relativeBudgetMassENN_joint_rows line 45
  6. lemma OAI.DirectionalTransience.relativeBudgetMassENN_le_one line 67
  7. lemma OAI.DirectionalTransience.relativeBudgetMassENN_toReal line 75
  8. def OAI.DirectionalTransience.TupleAtHeight line 83
  9. def OAI.DirectionalTransience.budgetTraversalMass line 86
  10. lemma OAI.DirectionalTransience.budgetTraversalMass_adapted line 91
  11. def OAI.DirectionalTransience.budgetFirstThreat line 119
  12. lemma OAI.DirectionalTransience.budgetFirstThreat_stopping line 124
  13. lemma OAI.DirectionalTransience.before_budgetFirstThreat_pass line 131
  14. lemma OAI.DirectionalTransience.upwardWord_successful line 149
  15. def OAI.DirectionalTransience.upwardHitWord line 163
  16. lemma OAI.DirectionalTransience.relativeWordDisplacement_zero line 167
  17. lemma OAI.DirectionalTransience.upwardWord_budget line 173
  18. def OAI.DirectionalTransience.tupleAppendUpward line 185
  19. lemma OAI.DirectionalTransience.tupleAppendUpward_injective line 188
  20. lemma OAI.DirectionalTransience.tupleAppendUpward_budget line 194
  21. lemma OAI.DirectionalTransience.rawWordLaw_upward_atom line 205
  22. lemma OAI.DirectionalTransience.relativeBudgetWordLaw_upward line 218
  23. lemma OAI.DirectionalTransience.relativeBudgetMassENN_upward line 258