OAI/Probability/DirectionalWalk/PosteriorMax.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalZeroOne.runningMax line 12
  2. lemma OAI.DirectionalZeroOne.runningMax_nonneg line 15
  3. lemma OAI.DirectionalZeroOne.runningMax_le line 19
  4. lemma OAI.DirectionalZeroOne.measurable_runningMax line 23
  5. lemma OAI.DirectionalZeroOne.dyadic_cover line 27
  6. lemma OAI.DirectionalZeroOne.martingale_maximal_real line 40
  7. lemma OAI.DirectionalZeroOne.integrable_runningMax line 55
  8. lemma OAI.DirectionalZeroOne.integral_runningMax_bound line 63
  9. def OAI.DirectionalZeroOne.posteriorMax line 102
  10. lemma OAI.DirectionalZeroOne.posterior_coord_le_one line 105
  11. lemma OAI.DirectionalZeroOne.integral_posteriorMax_bound line 111
  12. def OAI.DirectionalZeroOne.shiftedFiltration line 146
  13. lemma OAI.DirectionalZeroOne.martingale_shift_indicator line 152
  14. lemma OAI.DirectionalZeroOne.runningMax_future_bound line 165
  15. lemma OAI.DirectionalZeroOne.posterior_future_energy line 180
  16. def OAI.DirectionalZeroOne.crossingEvent line 228
  17. lemma OAI.DirectionalZeroOne.crossingEvent_measurable line 231
  18. lemma OAI.DirectionalZeroOne.crossingEvent_disjoint line 240
  19. lemma OAI.DirectionalZeroOne.union_crossingEvent line 249
  20. lemma OAI.DirectionalZeroOne.crossingEvent_overshoot line 262
  21. lemma OAI.DirectionalZeroOne.increasing_energy_tail_step line 270
  22. lemma OAI.DirectionalZeroOne.increasing_energy_geometric_tail line 333
  23. lemma OAI.DirectionalZeroOne.runningMax_mono line 352
  24. lemma OAI.DirectionalZeroOne.runningMax_step line 358
  25. lemma OAI.DirectionalZeroOne.posteriorMax_mono line 369
  26. lemma OAI.DirectionalZeroOne.posteriorMax_step line 374
  27. lemma OAI.DirectionalZeroOne.posteriorMax_adapted line 383
  28. lemma OAI.DirectionalZeroOne.posteriorMax_integrable line 392
  29. lemma OAI.DirectionalZeroOne.posteriorMax_geometric_tail line 402
  30. lemma OAI.DirectionalZeroOne.energy_exp_cover line 420
  31. lemma OAI.DirectionalZeroOne.geometric_three_quarter_sum line 448
  32. lemma OAI.DirectionalZeroOne.geometric_tail_exponential line 456
  33. lemma OAI.DirectionalZeroOne.integrable_exp_of_bound line 520
  34. lemma OAI.DirectionalZeroOne.posteriorMax_nonneg line 528
  35. lemma OAI.DirectionalZeroOne.posteriorMax_le_card line 532