OAI/Probability/Ballisticity/Estimates/BudgetNormalize.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalTransience.normalizeOr line 12
  2. lemma OAI.DirectionalTransience.normalizeOr_probability line 15
  3. lemma OAI.DirectionalTransience.normalizeOr_mass line 21
  4. lemma OAI.DirectionalTransience.normalizeOr_ae line 27
  5. lemma OAI.DirectionalTransience.measurable_normalizeOr line 34
  6. abbrev OAI.DirectionalTransience.BudgetProfile line 45
  7. instance OAI.DirectionalTransience.budgetProfile_probability line 49
  8. def OAI.DirectionalTransience.BudgetProfile.toSupported line 52
  9. lemma OAI.DirectionalTransience.BudgetProfile.measurable_toSupported line 56
  10. def OAI.DirectionalTransience.tupleShiftUp line 60
  11. lemma OAI.DirectionalTransience.tupleShiftUp_support line 63
  12. def OAI.DirectionalTransience.nextBudgetProfile line 80
  13. lemma OAI.DirectionalTransience.nextBudgetProfile_mass line 94