OAI/Probability/SKFluctuations/ClockPowerPathLimit.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Clock Power Path Limit.

  1. def OAI.SKFluctuations.Hierarchy.stepPathPowerDistance line 17
  2. theorem OAI.SKFluctuations.Hierarchy.stepPowerDisorder_sample_comparison line 24
  3. theorem OAI.SKFluctuations.Hierarchy.stepPowerDisorder_path_comparison line 58
  4. theorem OAI.SKFluctuations.Hierarchy.stepPowerDisorder_tendsto_path line 83
  5. def OAI.SKFluctuations.Hierarchy.stepPowerMoment line 113
  6. def OAI.SKFluctuations.Hierarchy.pathPowerMoment line 117
  7. theorem OAI.SKFluctuations.Hierarchy.stepPowerMoment_path_comparison line 121
  8. theorem OAI.SKFluctuations.Hierarchy.retainedPowerMoment_tendsto line 153
  9. theorem OAI.SKFluctuations.Hierarchy.retainedPowerMoment_tendsto_all line 183
  10. def OAI.SKFluctuations.physicalPathPowerMoment line 215
  11. theorem OAI.SKFluctuations.physicalPowerMoment_eq_stepPowerMoment line 220
  12. theorem OAI.SKFluctuations.physicalRetainedPowerMoment_tendsto line 235
  13. theorem OAI.SKFluctuations.eventually_physical_band_window line 259
  14. theorem OAI.SKFluctuations.physical_window_bound_of_energy line 306
  15. theorem OAI.SKFluctuations.physicalRawRatio_close line 351
  16. theorem OAI.SKFluctuations.physical_moment_le_one line 400
  17. theorem OAI.SKFluctuations.eventually_physical_raw_bootstrap line 421
  18. def OAI.SKFluctuations.PhysicalRawWindowCover line 477
  19. theorem OAI.SKFluctuations.physicalPathPowerMoment_le_of_rawRatio line 496
  20. theorem OAI.SKFluctuations.eventually_physical_path_raw_bootstrap line 513
  21. theorem OAI.SKFluctuations.eventually_physicalRetainedBand line 554