OAI/Probability/SKFluctuations/PhysicalFarPair.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Physical Far Pair.

  1. theorem OAI.SKFluctuations.dot_physicalPairIncrement line 16
  2. theorem OAI.SKFluctuations.abs_dot_physicalPairIncrement_le line 29
  3. theorem OAI.SKFluctuations.physicalPairConditionalSquare_power_le line 43
  4. theorem OAI.SKFluctuations.eventually_physical_conditional_square_projection line 81
  5. theorem OAI.SKFluctuations.abs_dot_physicalTerminalIncrement_le line 119
  6. theorem OAI.SKFluctuations.physicalTerminalConditionalSquare_power_le line 131
  7. theorem OAI.SKFluctuations.eventually_physical_terminal_conditional_square_projection line 169
  8. theorem OAI.SKFluctuations.Hierarchy.integral_fork_swap line 207
  9. def OAI.SKFluctuations.Hierarchy.conditionalPathAverage line 261
  10. theorem OAI.SKFluctuations.Hierarchy.conditionalPathAverage_measurable line 271
  11. theorem OAI.SKFluctuations.Hierarchy.condExp_conditionalPathAverage line 300
  12. def OAI.SKFluctuations.physicalBlockSquare line 355
  13. theorem OAI.SKFluctuations.actualSpinPath_measurable line 360
  14. theorem OAI.SKFluctuations.physicalBlockSquare_measurable line 371
  15. theorem OAI.SKFluctuations.conditionalBlockSquare_eq_physical line 380
  16. theorem OAI.SKFluctuations.conditionalBlockSquare_uniform_eq_physical line 402
  17. def OAI.SKFluctuations.physicalRadiusSquareIntegral line 414
  18. theorem OAI.SKFluctuations.actualRadiusSquareIntegral_eq_physical line 419
  19. theorem OAI.SKFluctuations.physicalNearPairProduct_Lp line 429
  20. theorem OAI.SKFluctuations.Hierarchy.conditionalPathAverage_nonneg line 461
  21. theorem OAI.SKFluctuations.Hierarchy.conditionalPathAverage_const_mul line 478
  22. theorem OAI.SKFluctuations.Hierarchy.conditionalPathAverage_mono_bounded line 493
  23. def OAI.SKFluctuations.physicalNearLayerSquare line 531
  24. theorem OAI.SKFluctuations.physicalNearLayerSquare_le line 538
  25. theorem OAI.SKFluctuations.Hierarchy.conditionalPathAverage_const line 576
  26. theorem OAI.SKFluctuations.Hierarchy.conditionalPathAverage_parameter_measurable line 591