OAI/Probability/SKFluctuations/PhysicalForkSumMoments.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Physical Fork Sum Moments.

  1. theorem OAI.SKFluctuations.Hierarchy.integral_conditionalForkTest_sum line 17
  2. theorem OAI.SKFluctuations.Hierarchy.fork_sum_power_le line 41
  3. theorem OAI.SKFluctuations.Hierarchy.fork_add_power_le line 98
  4. def OAI.SKFluctuations.physicalOverlapMoment line 128
  5. theorem OAI.SKFluctuations.physicalOverlapMoment_le_double_sum line 135
  6. theorem OAI.SKFluctuations.physicalCutPairPower_futureTerminal line 201
  7. theorem OAI.SKFluctuations.eventually_cut_pair_terminal_full_moment line 219
  8. theorem OAI.SKFluctuations.physicalRawRatio_half_moment line 274
  9. def OAI.SKFluctuations.physicalCoreLayerPower line 315
  10. theorem OAI.SKFluctuations.physicalCoreLayerPower_nonneg line 322
  11. theorem OAI.SKFluctuations.physicalCoreLayerPower_futurePair line 327
  12. theorem OAI.SKFluctuations.eventually_core_layer_full_moment line 343
  13. theorem OAI.SKFluctuations.physicalCoreLayerPower_futureTerminal line 410
  14. theorem OAI.SKFluctuations.eventually_core_layer_terminal_full_moment line 428
  15. theorem OAI.SKFluctuations.eventually_physical_clock_pair_full_moment line 495
  16. theorem OAI.SKFluctuations.eventually_physical_clock_core_layer_full_moment line 516
  17. def OAI.SKFluctuations.physicalOverlapLayerMoment line 547
  18. def OAI.SKFluctuations.overlapComponentEnd line 555
  19. theorem OAI.SKFluctuations.physicalOverlapLayerMoment_nonneg line 558
  20. theorem OAI.SKFluctuations.physicalOverlapLayerMoment_swap line 566
  21. theorem OAI.SKFluctuations.eventually_physical_overlap_layer_clock_moment line 583