OAI/Probability/Ballisticity/Estimates/BudgetAlgebra.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalTransience.relativeBudgetWordLaw_zero_univ line 12
  2. lemma OAI.DirectionalTransience.relativeBudgetMassENN_zero line 34
  3. lemma OAI.DirectionalTransience.relativeBudgetWordLaw_mono line 40
  4. lemma OAI.DirectionalTransience.relativeBudgetMassENN_mono line 47
  5. lemma OAI.DirectionalTransience.relativeBudgetMassENN_restart_comp line 52
  6. lemma OAI.DirectionalTransience.budgetFirstThreat_eq_measurable line 63
  7. lemma OAI.DirectionalTransience.budgetFirstThreat_lt_threat line 79
  8. lemma OAI.DirectionalTransience.budgetFirstThreat_mass_lower line 94
  9. def OAI.DirectionalTransience.budgetRetryEvent line 122
  10. lemma OAI.DirectionalTransience.rowSigma_below_mono_nat line 130
  11. lemma OAI.DirectionalTransience.budgetRetryEvent_probability line 138