OAI/Probability/SKFluctuations/ActualPathScore.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

Actual Path Score.

  1. theorem OAI.SKFluctuations.Hierarchy.scaledTransitionLaw_eq line 20
  2. def OAI.SKFluctuations.Hierarchy.hierarchyScores line 41
  3. theorem OAI.SKFluctuations.Hierarchy.hierarchyScores_measurable line 49
  4. theorem OAI.SKFluctuations.Hierarchy.hierarchyScores_hasSubgaussianMGF line 67
  5. def OAI.SKFluctuations.Hierarchy.hierarchyPathScore line 82
  6. theorem OAI.SKFluctuations.Hierarchy.hierarchyPathScore_hasSubgaussianMGF line 89
  7. def OAI.SKFluctuations.Hierarchy.forwardKernel line 113
  8. theorem OAI.SKFluctuations.Hierarchy.forwardKernel_apply line 118
  9. theorem OAI.SKFluctuations.Hierarchy.forwardKernel_isMarkov line 125
  10. theorem OAI.SKFluctuations.Hierarchy.measurable_finCons line 133
  11. def OAI.SKFluctuations.Hierarchy.forwardTailKernel line 141
  12. theorem OAI.SKFluctuations.Hierarchy.forwardLaw_cons line 148
  13. theorem OAI.SKFluctuations.Hierarchy.integral_forwardLaw_cons line 192
  14. def OAI.SKFluctuations.Hierarchy.subgaussianMomentConstant line 226
  15. theorem OAI.SKFluctuations.Hierarchy.abs_pow_le_two_exp line 229
  16. theorem OAI.SKFluctuations.Hierarchy.subgaussian_integrable_abs_natPow line 244
  17. theorem OAI.SKFluctuations.Hierarchy.subgaussian_abs_natPow_le line 254
  18. theorem OAI.SKFluctuations.Hierarchy.subgaussian_even_moment_le line 273
  19. theorem OAI.SKFluctuations.Hierarchy.orderedSteps_append_right line 318
  20. def OAI.SKFluctuations.Hierarchy.segmentTransitions line 324
  21. def OAI.SKFluctuations.Hierarchy.segmentScores line 332
  22. theorem OAI.SKFluctuations.Hierarchy.segmentTransitions_measurable line 341
  23. theorem OAI.SKFluctuations.Hierarchy.segmentTransitions_normalized line 351
  24. theorem OAI.SKFluctuations.Hierarchy.segmentScores_measurable line 361
  25. def OAI.SKFluctuations.Hierarchy.segmentLaw line 379
  26. theorem OAI.SKFluctuations.Hierarchy.segmentLaw_isProbability line 385
  27. def OAI.SKFluctuations.Hierarchy.segmentPathScore line 393
  28. theorem OAI.SKFluctuations.Hierarchy.segmentScores_hasSubgaussianMGF line 398
  29. theorem OAI.SKFluctuations.Hierarchy.segmentPathScore_hasSubgaussianMGF line 415
  30. theorem OAI.SKFluctuations.Hierarchy.segmentPathScore_even_moment line 426
  31. theorem OAI.SKFluctuations.Hierarchy.integral_scaledTransition_mean line 438
  32. theorem OAI.SKFluctuations.Hierarchy.BddSmooth.integrable_comp_measurable line 474
  33. theorem OAI.SKFluctuations.Hierarchy.integral_segmentLaw_cons line 484
  34. theorem OAI.SKFluctuations.Hierarchy.integral_segmentLaw_mean line 499
  35. theorem OAI.SKFluctuations.Hierarchy.polynomial_young_split line 531
  36. theorem OAI.SKFluctuations.Hierarchy.weighted_odd_score_young line 547
  37. theorem OAI.SKFluctuations.Hierarchy.BddSmooth.natPow line 566
  38. theorem OAI.SKFluctuations.Hierarchy.BddSmooth.abs_natPow_zero line 570
  39. def OAI.SKFluctuations.Hierarchy.hierarchyCenteredEvenMoment line 576
  40. theorem OAI.SKFluctuations.Hierarchy.hierarchyCenteredEvenMoment_smooth_zero line 581
  41. theorem OAI.SKFluctuations.Hierarchy.hierarchy_projection_one_step line 590