OAI/Probability/SKFluctuations/PhysicalCommonCutSwap.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Physical Common Cut Swap.

  1. theorem OAI.SKFluctuations.Hierarchy.integral_commonKernel_swap line 15
  2. theorem OAI.SKFluctuations.Hierarchy.integral_conditionalForkTest_swap line 51
  3. theorem OAI.SKFluctuations.Hierarchy.conditionalForkTest_integrable line 110
  4. theorem OAI.SKFluctuations.Hierarchy.integral_conditionalForkTest_power_swap line 125
  5. theorem OAI.SKFluctuations.abs_dot_physicalFuturePairIncrement_le line 168
  6. theorem OAI.SKFluctuations.eventually_common_cut_observed_square_projection line 176
  7. def OAI.SKFluctuations.physicalFutureTerminalIncrement line 237
  8. theorem OAI.SKFluctuations.physicalFutureTerminalIncrement_eq_spinPath line 243
  9. theorem OAI.SKFluctuations.physicalFutureTerminalIncrement_measurable line 254
  10. theorem OAI.SKFluctuations.physicalFutureTerminalAverage line 263
  11. theorem OAI.SKFluctuations.eventually_common_cut_terminal_conditional_square_projection line 285
  12. theorem OAI.SKFluctuations.eventually_common_cut_terminal_projection_moment line 318
  13. theorem OAI.SKFluctuations.abs_dot_physicalFutureTerminalIncrement_le line 399
  14. theorem OAI.SKFluctuations.eventually_common_cut_terminal_observed_square_projection line 407
  15. def OAI.SKFluctuations.physicalCutIncrement line 468
  16. def OAI.SKFluctuations.physicalCutPairSquare line 473
  17. theorem OAI.SKFluctuations.physicalCutIncrement_measurable line 480
  18. theorem OAI.SKFluctuations.physicalCutIncrement_norm_le line 486
  19. theorem OAI.SKFluctuations.physicalCutPairSquare_nonneg line 493
  20. theorem OAI.SKFluctuations.physicalCutPairSquare_measurable line 498
  21. theorem OAI.SKFluctuations.physicalCutPairSquare_le line 510
  22. def OAI.SKFluctuations.physicalCutMass line 546
  23. theorem OAI.SKFluctuations.physicalCutMass_mem line 551
  24. theorem OAI.SKFluctuations.physicalCutMass_monotone line 564
  25. def OAI.SKFluctuations.physicalRawRatio line 575
  26. theorem OAI.SKFluctuations.physicalRawRatio_one_le line 583
  27. theorem OAI.SKFluctuations.physicalRawRatio_bound line 588
  28. theorem OAI.SKFluctuations.physicalRawRatio_moment line 605