OAI/Probability/SKFluctuations/UniformActualLaterProjection.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Uniform Actual Later Projection.

  1. theorem OAI.SKFluctuations.eventually_uniform_actual_random_later_projection line 19
  2. abbrev OAI.SKFluctuations.TwoSegmentState line 99
  3. def OAI.SKFluctuations.twoSegmentStart line 103
  4. def OAI.SKFluctuations.twoSegmentEnd line 107
  5. theorem OAI.SKFluctuations.twoSegmentStart_measurable line 111
  6. theorem OAI.SKFluctuations.twoSegmentEnd_measurable line 117
  7. def OAI.SKFluctuations.twoSegmentIncrement line 123
  8. theorem OAI.SKFluctuations.twoSegmentIncrement_measurable line 128
  9. theorem OAI.SKFluctuations.actualTwoSegmentLaw_finite line 137
  10. theorem OAI.SKFluctuations.twoSegmentIncrement_moment_integrable line 147
  11. def OAI.SKFluctuations.actualForkTwoSegmentLaw line 160
  12. theorem OAI.SKFluctuations.eventually_actual_fork_projection line 170
  13. theorem OAI.SKFluctuations.Hierarchy.boundedContinuous_bddSmooth0 line 206
  14. theorem OAI.SKFluctuations.Hierarchy.actualCutField_law line 212
  15. def OAI.SKFluctuations.Hierarchy.runningMax line 238
  16. theorem OAI.SKFluctuations.Hierarchy.runningMax_self_le line 242
  17. theorem OAI.SKFluctuations.Hierarchy.runningMax_monotone line 247
  18. theorem OAI.SKFluctuations.Hierarchy.runningMax_nonneg line 250
  19. theorem OAI.SKFluctuations.Hierarchy.runningMax_le line 253
  20. theorem OAI.SKFluctuations.Hierarchy.runningMax_power_exchange line 261
  21. theorem OAI.SKFluctuations.Hierarchy.runningMax_adapted line 292
  22. theorem OAI.SKFluctuations.Hierarchy.runningMax_power_integrable line 298
  23. theorem OAI.SKFluctuations.Hierarchy.submartingale_runningMax_power_exchange line 307
  24. theorem OAI.SKFluctuations.Hierarchy.boundedSubmartingale_runningMax_moment line 346
  25. theorem OAI.SKFluctuations.Hierarchy.boundedMartingale_runningMax_square_moment line 396
  26. theorem OAI.SKFluctuations.Hierarchy.boundedMartingale_runningMax_square_Lp line 408
  27. def OAI.SKFluctuations.actualPathMaxSquare line 428
  28. theorem OAI.SKFluctuations.actualPathMaxSquare_Lp line 435
  29. theorem OAI.SKFluctuations.Hierarchy.integral_pow_le_mass line 458
  30. def OAI.SKFluctuations.Hierarchy.conditionalBlockSquare line 493
  31. theorem OAI.SKFluctuations.Hierarchy.conditionalBlockSquare_measurable line 496
  32. theorem OAI.SKFluctuations.Hierarchy.conditionalBlockSquare_joint line 500
  33. theorem OAI.SKFluctuations.Hierarchy.conditionalBlockSquare_uniform_bounds line 509
  34. theorem OAI.SKFluctuations.Hierarchy.parameter_integral_power_bound line 538
  35. theorem OAI.SKFluctuations.Hierarchy.boundedMartingale_cut_moment_mono line 591