OAI/Probability/SKFluctuations/ActualSpinMartingale.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Actual Spin Martingale.

  1. def OAI.SKFluctuations.normalizedSpin line 20
  2. def OAI.SKFluctuations.actualSpinMean line 23
  3. theorem OAI.SKFluctuations.actualSpinMean_measurable line 28
  4. theorem OAI.SKFluctuations.actualSpinMean_condExp line 35
  5. theorem OAI.SKFluctuations.actualSpinMean_abs_le line 48
  6. theorem OAI.SKFluctuations.projectionEuclideanNorm_le_of_coordinate_bound line 56
  7. theorem OAI.SKFluctuations.actualSpinMean_norm_le line 75
  8. theorem OAI.SKFluctuations.actualSpinMean_sub_norm_le line 82
  9. theorem OAI.SKFluctuations.actualSpinMean_sub_moment_integrable line 93
  10. theorem OAI.SKFluctuations.spinProjection_actualSpinMean line 111
  11. theorem OAI.SKFluctuations.Hierarchy.martingale_finiteCoordinates line 139
  12. theorem OAI.SKFluctuations.Hierarchy.martingale_continuousLinearMap line 156
  13. theorem OAI.SKFluctuations.Hierarchy.hierarchyMeanPath_abs_le line 169
  14. def OAI.SKFluctuations.actualSpinPath line 192
  15. theorem OAI.SKFluctuations.actualSpinPath_martingale line 199
  16. theorem OAI.SKFluctuations.actualSpinPath_norm_le line 210
  17. def OAI.SKFluctuations.Hierarchy.sampledFiltration line 233
  18. theorem OAI.SKFluctuations.Hierarchy.martingale_sampled line 240
  19. def OAI.SKFluctuations.actualPathSquareSum line 255
  20. theorem OAI.SKFluctuations.actualPathSquareSum_moment line 266
  21. theorem OAI.SKFluctuations.actualPathSquareSum_Lp line 279
  22. def OAI.SKFluctuations.Hierarchy.actualCutField line 303
  23. theorem OAI.SKFluctuations.Hierarchy.actualCutField_measurable_joint line 312
  24. theorem OAI.SKFluctuations.Hierarchy.actualCutField_measurable line 322
  25. theorem OAI.SKFluctuations.Hierarchy.hierarchyMeanPath_zero line 327
  26. theorem OAI.SKFluctuations.Hierarchy.hierarchyMeanPath_at_cut line 336
  27. theorem OAI.SKFluctuations.Hierarchy.integrable_actualCutField_test line 346
  28. theorem OAI.SKFluctuations.Hierarchy.integral_actualCutField_test line 360
  29. theorem OAI.SKFluctuations.Hierarchy.hierarchyBlockVariance_eq_actualPath line 399
  30. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchyMean_even_jensen line 427
  31. theorem OAI.SKFluctuations.Hierarchy.integral_segmentLaw_laterProjection_le line 438
  32. theorem OAI.SKFluctuations.alignedFieldClock_of_physical line 473
  33. theorem OAI.SKFluctuations.random_directional_increment_integrable line 486
  34. def OAI.SKFluctuations.actualTwoSegmentLaw line 513
  35. theorem OAI.SKFluctuations.eventually_actual_random_later_projection line 525
  36. theorem OAI.SKFluctuations.eventually_uniform_random_projection_moment line 605