OAI/Probability/Ballisticity/Estimates/BudgetMeasurable.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalTransience.relativeBudgetEndpointLaw_rows line 13
  2. lemma OAI.DirectionalTransience.budgetEndpointMixture_joint_rows line 20
  3. lemma OAI.DirectionalTransience.budgetProfileMass_joint_rows line 44
  4. lemma OAI.DirectionalTransience.nextBudgetProfile_measurable_rows line 60
  5. lemma OAI.DirectionalTransience.nextBudgetProfile_measurable_below line 74
  6. lemma OAI.DirectionalTransience.measurableSet_profileBudgetThreat_upper line 90
  7. lemma OAI.DirectionalTransience.fresh_random_budget_threat line 110
  8. lemma OAI.DirectionalTransience.rawTupleEndpointLaw_rows line 150
  9. lemma OAI.DirectionalTransience.rawTupleMixture_joint_rows line 168
  10. lemma OAI.DirectionalTransience.rawTupleEndpointLaw_support line 187
  11. lemma OAI.DirectionalTransience.rawTupleMixture_support line 199
  12. lemma OAI.DirectionalTransience.rawTupleMixture_univ_le line 207
  13. instance OAI.DirectionalTransience.rawTupleMixture_finite line 213
  14. abbrev OAI.DirectionalTransience.LayerTupleProfile line 218
  15. instance OAI.DirectionalTransience.layerTupleProfile_probability line 222
  16. def OAI.DirectionalTransience.LayerTupleProfile.toSupported line 225
  17. lemma OAI.DirectionalTransience.LayerTupleProfile.measurable_toSupported line 229
  18. def OAI.DirectionalTransience.BudgetProfile.toLayerProfile line 232
  19. def OAI.DirectionalTransience.fullTupleProfile line 236
  20. lemma OAI.DirectionalTransience.fullTupleProfile_mass line 250
  21. lemma OAI.DirectionalTransience.fullTupleProfile_measurable line 256