OAI/Probability/SKFluctuations/ActualConditionalHierarchy.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Actual Conditional Hierarchy.

  1. instance OAI.SKFluctuations.Hierarchy.forwardPathNonempty line 21
  2. instance OAI.SKFluctuations.Hierarchy.forwardPathStandardBorel line 26
  3. theorem OAI.SKFluctuations.Hierarchy.condExp_prefix_hierarchy line 38
  4. theorem OAI.SKFluctuations.Hierarchy.condExp_prefix_hierarchy_fixed line 58
  5. def OAI.SKFluctuations.Hierarchy.forwardPrefixSpace line 86
  6. theorem OAI.SKFluctuations.Hierarchy.forwardPrefixSpace_zero line 93
  7. theorem OAI.SKFluctuations.Hierarchy.forwardPrefixSpace_le line 98
  8. theorem OAI.SKFluctuations.Hierarchy.forwardPrefixSpace_mono line 113
  9. def OAI.SKFluctuations.Hierarchy.forwardFiltration line 136
  10. theorem OAI.SKFluctuations.Hierarchy.kernel_compProd_comap line 150
  11. theorem OAI.SKFluctuations.Hierarchy.hierarchyPathLaw_cons line 163
  12. theorem OAI.SKFluctuations.Hierarchy.condExp_measurableEquiv line 189
  13. def OAI.SKFluctuations.Hierarchy.hierarchyMeanPath line 219
  14. theorem OAI.SKFluctuations.Hierarchy.hierarchyMeanPath_measurable line 232
  15. theorem OAI.SKFluctuations.Hierarchy.integrable_terminal_hierarchyPathLaw line 255
  16. theorem OAI.SKFluctuations.Hierarchy.condExp_hierarchyMeanPath line 272
  17. theorem OAI.SKFluctuations.Hierarchy.hierarchyMeanPath_martingale line 319
  18. def OAI.SKFluctuations.Hierarchy.segmentKernel line 345
  19. theorem OAI.SKFluctuations.Hierarchy.segmentKernel_apply line 350
  20. theorem OAI.SKFluctuations.Hierarchy.segmentKernel_markov line 357
  21. theorem OAI.SKFluctuations.Hierarchy.hierarchyCenteredEvenMoment_measurable line 367
  22. theorem OAI.SKFluctuations.spinProjection_measurable line 391
  23. theorem OAI.SKFluctuations.projectionEuclideanNorm_measurable line 399
  24. theorem OAI.SKFluctuations.random_projection_moment_integrable line 404
  25. theorem OAI.SKFluctuations.eventually_random_projection_moment line 441
  26. theorem OAI.SKFluctuations.Hierarchy.integral_centered_hierarchyPathKernel line 493
  27. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchyMean_measurable_joint line 504
  28. theorem OAI.SKFluctuations.random_terminal_residual_integral line 522
  29. def OAI.SKFluctuations.actualSegmentTailLaw line 572
  30. theorem OAI.SKFluctuations.eventually_actual_random_terminal_projection line 584