OAI/Probability/Ballisticity/Estimates/RetainedComposition.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalTransience.rawTupleMixture_mono line 13
  2. lemma OAI.DirectionalTransience.rawTupleMixture_smul line 21
  3. lemma OAI.DirectionalTransience.rawTupleMixture_comp_le line 26
  4. lemma OAI.DirectionalTransience.rawTupleEndpointLaw_zero line 41
  5. lemma OAI.DirectionalTransience.rawTupleMixture_zero line 60
  6. lemma OAI.DirectionalTransience.budgetEndpointMixture_le_raw line 66
  7. lemma OAI.DirectionalTransience.protectionMass_ennreal line 74
  8. lemma OAI.DirectionalTransience.protection_retained_succ line 82
  9. theorem OAI.DirectionalTransience.protection_retained_le_raw line 95
  10. lemma OAI.DirectionalTransience.upwardEndpoint_atom line 126
  11. lemma OAI.DirectionalTransience.tupleUpwardEndpoint_atom line 136
  12. lemma OAI.DirectionalTransience.tupleUpwardEndpoint_le line 145
  13. lemma OAI.DirectionalTransience.tupleUpwardMixture_le line 156
  14. lemma OAI.DirectionalTransience.stage_separated_mass_upward line 170