OAI/Probability/Ballisticity/Walk/Rows.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TailDecorrelation.rows line 15
  2. lemma OAI.TailDecorrelation.rows_mono line 18
  3. lemma OAI.TailDecorrelation.rows_le line 24
  4. lemma OAI.TailDecorrelation.rows_univ line 30
  5. def OAI.TailDecorrelation.dataRows line 35
  6. lemma OAI.TailDecorrelation.dataRows_mono line 39
  7. lemma OAI.TailDecorrelation.dataRows_le line 43
  8. lemma OAI.TailDecorrelation.dataRows_univ line 46
  9. lemma OAI.TailDecorrelation.rows_eq_iSup_two line 51
  10. lemma OAI.TailDecorrelation.independent_rows line 56
  11. lemma OAI.TailDecorrelation.independent_row_functions line 65
  12. lemma OAI.TailDecorrelation.row_function_integral_mul line 75
  13. lemma OAI.TailDecorrelation.dataRows_section line 87
  14. def OAI.TailDecorrelation.prefixRows line 96
  15. lemma OAI.TailDecorrelation.prefixRows_finite line 98
  16. lemma OAI.TailDecorrelation.prefixRows_mono line 101
  17. lemma OAI.TailDecorrelation.iUnion_prefixRows line 105
  18. def OAI.TailDecorrelation.dataFiltration line 110
  19. lemma OAI.TailDecorrelation.iSup_dataFiltration line 115
  20. lemma OAI.TailDecorrelation.likelihood_approximation line 136
  21. lemma OAI.TailDecorrelation.bounded_likelihood_approximation line 145
  22. lemma OAI.TailDecorrelation.integrable_bounded_nonneg line 194
  23. lemma OAI.TailDecorrelation.eventually_integral_le_of_pointwise_eventually line 200
  24. lemma OAI.TailDecorrelation.bounded_escape_product line 243
  25. def OAI.TailDecorrelation.EscapingLocalApproximation line 300
  26. lemma OAI.TailDecorrelation.bounded_product_approximation_pointwise line 308
  27. lemma OAI.TailDecorrelation.bounded_decorrelation line 317