OAI/Probability/SKFluctuations/PhysicalNearPairIntegral.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

Physical Near Pair Integral.

  1. theorem OAI.SKFluctuations.physicalNearLayerSquare_nonneg line 15
  2. theorem OAI.SKFluctuations.physicalBlockSquare_nonneg line 21
  3. theorem OAI.SKFluctuations.physicalNearLayerSquare_measurable line 27
  4. theorem OAI.SKFluctuations.physicalNearLayerSquare_le_runningMax line 50
  5. theorem OAI.SKFluctuations.physicalBlockSquare_le_four line 79
  6. theorem OAI.SKFluctuations.physicalBlockSquare_joint line 98
  7. def OAI.SKFluctuations.physicalNearRadiusIntegral line 110
  8. theorem OAI.SKFluctuations.physicalNearRadiusIntegral_nonneg line 115
  9. theorem OAI.SKFluctuations.physicalRadiusSquareIntegral_measurable line 123
  10. theorem OAI.SKFluctuations.physicalRadiusSquareIntegral_bound line 135
  11. theorem OAI.SKFluctuations.physicalNearRadiusIntegral_le line 145
  12. theorem OAI.SKFluctuations.physicalRadiusSquareIntegral_nonneg line 173
  13. theorem OAI.SKFluctuations.physicalNearRadiusIntegral_Lp line 181
  14. theorem OAI.SKFluctuations.Hierarchy.hierarchyMeanPath_comp line 252
  15. theorem OAI.SKFluctuations.actualSpinPath_comp line 272
  16. theorem OAI.SKFluctuations.actualSpinPath_cons line 280
  17. theorem OAI.SKFluctuations.actualSpinPath_coordinate_measurable line 288
  18. def OAI.SKFluctuations.Hierarchy.continuationState line 308
  19. theorem OAI.SKFluctuations.Hierarchy.continuationState_fst line 316
  20. theorem OAI.SKFluctuations.Hierarchy.continuationState_measurable line 326
  21. theorem OAI.SKFluctuations.Hierarchy.hierarchyMeanPath_after_prefix line 337
  22. theorem OAI.SKFluctuations.Hierarchy.conditionalPathAverage_continuation line 351
  23. theorem OAI.SKFluctuations.actualSpinPath_after_prefix line 370
  24. def OAI.SKFluctuations.physicalFuturePairIncrement line 379
  25. theorem OAI.SKFluctuations.physicalFuturePairIncrement_eq_spinPath line 385
  26. theorem OAI.SKFluctuations.physicalFuturePairIncrement_measurable line 396
  27. theorem OAI.SKFluctuations.physicalFuturePairAverage line 405
  28. theorem OAI.SKFluctuations.eventually_common_cut_conditional_square_projection line 427
  29. theorem OAI.SKFluctuations.eventually_common_cut_projection_moment line 460
  30. theorem OAI.SKFluctuations.Hierarchy.bounded_integral_power_le line 541
  31. theorem OAI.SKFluctuations.Hierarchy.conditionalPathAverage_abs_le line 557
  32. theorem OAI.SKFluctuations.Hierarchy.conditionalPathAverage_power_le line 586
  33. def OAI.SKFluctuations.Hierarchy.conditionalForkTest line 615
  34. theorem OAI.SKFluctuations.Hierarchy.conditionalForkTest_measurable line 622