OAI/Probability/Ballisticity/Estimates/BudgetClipping.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalTransience.signedHeight_sub' line 13
  2. lemma OAI.DirectionalTransience.recordOrZeroPrefix_wordFirstHit line 18
  3. def OAI.DirectionalTransience.CentralWordBudget line 57
  4. lemma OAI.DirectionalTransience.tubePrefix_word_budget line 61
  5. lemma OAI.DirectionalTransience.tubePrefix_le_centralWordBudget line 79
  6. lemma OAI.DirectionalTransience.tupleCentral_budget line 94
  7. lemma OAI.DirectionalTransience.tupleTubeMass_le_relativeBudget line 104
  8. lemma OAI.DirectionalTransience.rawWordLaw_le_one line 121
  9. lemma OAI.DirectionalTransience.relativeBudgetWordLaw_le_one line 126
  10. def OAI.DirectionalTransience.relativeBudgetMass line 134
  11. lemma OAI.DirectionalTransience.tupleTubeMass_le_relativeBudgetMass line 138
  12. theorem OAI.DirectionalTransience.initial_relativeBudget_clipping line 158