OAI/Probability/Ballisticity/Estimates/BudgetThreat.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalTransience.regularPath_translate_zero line 12
  2. lemma OAI.DirectionalTransience.regular_noDrop_hit line 26
  3. lemma OAI.DirectionalTransience.regular_noDrop_word_record line 51
  4. def OAI.DirectionalTransience.WordEnvelope line 82
  5. lemma OAI.DirectionalTransience.good_noDrop_le_WordEnvelope line 86
  6. lemma OAI.DirectionalTransience.tupleEnvelope_budget line 104
  7. lemma OAI.DirectionalTransience.tupleGood_le_relativeBudget line 114
  8. def OAI.DirectionalTransience.relativeBadMass line 145
  9. lemma OAI.DirectionalTransience.relativeBadMass_eq line 148
  10. lemma OAI.DirectionalTransience.good_add_bad_noDrop line 153
  11. lemma OAI.DirectionalTransience.relativeBadMass_nonneg line 167
  12. lemma OAI.DirectionalTransience.relativeBadMass_le_one line 170
  13. lemma OAI.DirectionalTransience.relativeGoodMass_le_noDrop line 173
  14. lemma OAI.DirectionalTransience.measurable_relativeBadMass line 177
  15. lemma OAI.DirectionalTransience.relativeBadMass_mean line 180
  16. def OAI.DirectionalTransience.tupleBadMass line 196
  17. lemma OAI.DirectionalTransience.measurable_sum_relativeBadMass line 200
  18. lemma OAI.DirectionalTransience.sum_relativeBadMass_bounds line 207
  19. lemma OAI.DirectionalTransience.tupleBadMass_nonneg line 213
  20. lemma OAI.DirectionalTransience.measurable_tupleBadMass line 217
  21. lemma OAI.DirectionalTransience.integrable_sum_relativeBadMass line 221
  22. lemma OAI.DirectionalTransience.tupleBadMass_mean line 231
  23. lemma OAI.DirectionalTransience.product_noDrop_le_good_bad line 253