OAI/Probability/Ballisticity/Estimates/BudgetEndpoint.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalTransience.TupleKernel.countable_map_bind line 13
  2. lemma OAI.DirectionalTransience.TupleKernel.countable_bind_map line 26
  3. lemma OAI.DirectionalTransience.TupleKernel.dependentPair_map line 36
  4. lemma OAI.DirectionalTransience.TupleKernel.countable_bind_mono line 46
  5. lemma OAI.DirectionalTransience.tupleWordEndpoint_concat line 56
  6. lemma OAI.DirectionalTransience.relativeBudgetEndpointLaw_comp_le line 64
  7. def OAI.DirectionalTransience.budgetEndpointMixture line 78
  8. lemma OAI.DirectionalTransience.budgetEndpointMixture_apply line 82
  9. lemma OAI.DirectionalTransience.budgetEndpointMixture_univ line 88
  10. lemma OAI.DirectionalTransience.budgetEndpointMixture_comp_le line 95
  11. instance OAI.DirectionalTransience.budgetEndpointMixture_finite line 103
  12. lemma OAI.DirectionalTransience.relativeBudgetWordLaw_ae line 120
  13. lemma OAI.DirectionalTransience.relativeBudgetEndpointLaw_support line 139
  14. lemma OAI.DirectionalTransience.TupleKernel.countable_bind_ae line 157
  15. lemma OAI.DirectionalTransience.budgetEndpointMixture_support line 165
  16. lemma OAI.DirectionalTransience.tupleSeparated_mono line 173
  17. lemma OAI.DirectionalTransience.tupleSeparated_coordinate line 177