OAI/Probability/Ballisticity/Stationary/ArrayWindowMarks.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalTransience.arrayWindowHeight line 13
  2. def OAI.DirectionalTransience.arrayWindowCost line 15
  3. lemma OAI.DirectionalTransience.arrayWindowHeight_continuous line 18
  4. lemma OAI.DirectionalTransience.arrayWindowCost_continuous line 20
  5. def OAI.DirectionalTransience.expNeg line 23
  6. lemma OAI.DirectionalTransience.expNeg_le_one line 24
  7. lemma OAI.DirectionalTransience.expNeg_ne_top line 29
  8. lemma OAI.DirectionalTransience.expNeg_continuous line 31
  9. lemma OAI.DirectionalTransience.expNeg_toReal_continuous line 33
  10. lemma OAI.DirectionalTransience.arrayWindowHeight_actual line 38
  11. lemma OAI.DirectionalTransience.episodeCost_nonneg_real line 54
  12. lemma OAI.DirectionalTransience.arrayWindowCost_actual line 64
  13. lemma OAI.DirectionalTransience.expNeg_log_ratio line 82
  14. def OAI.DirectionalTransience.arrayProfileMass line 103
  15. lemma OAI.DirectionalTransience.arrayProfileMass_continuous line 107
  16. def OAI.DirectionalTransience.arrayUpperRows line 111
  17. lemma OAI.DirectionalTransience.arrayUpperRows_continuous line 113
  18. def OAI.DirectionalTransience.arrayKernelImage line 116
  19. lemma OAI.DirectionalTransience.arrayKernelImage_lowerSemicontinuous line 120
  20. def OAI.DirectionalTransience.arrayDiscountedProfile line 143
  21. lemma OAI.DirectionalTransience.arrayDiscountedProfile_continuous line 147
  22. def OAI.DirectionalTransience.ArrayContinuation line 158
  23. lemma OAI.DirectionalTransience.arrayContinuation_closed line 162
  24. lemma OAI.DirectionalTransience.actual_arrayProfileMass line 177
  25. lemma OAI.DirectionalTransience.actual_arrayKernelImage line 183
  26. lemma OAI.DirectionalTransience.actual_arrayContinuation line 203