OAI/Probability/SKFluctuations/FiniteRetainedGridReady.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

Finite Retained Grid Ready.

  1. theorem OAI.SKFluctuations.finiteRetainedGridReady line 15
  2. theorem OAI.SKFluctuations.retainedWindow_future_means line 45
  3. def OAI.SKFluctuations.Hierarchy.ClockTree.pairPower line 80
  4. def OAI.SKFluctuations.Hierarchy.ClockTree.pairPowerTest line 84
  5. def OAI.SKFluctuations.Hierarchy.ClockTree.powerClock line 90
  6. def OAI.SKFluctuations.Hierarchy.ClockTree.powerTest line 94
  7. theorem OAI.SKFluctuations.Hierarchy.ClockTree.expect_mul_constant line 102
  8. theorem OAI.SKFluctuations.Hierarchy.ClockTree.pairPower_expect line 108
  9. theorem OAI.SKFluctuations.Hierarchy.ClockTree.pairPower_bound line 123
  10. theorem OAI.SKFluctuations.Hierarchy.ClockTree.powerTest_bound line 133
  11. theorem OAI.SKFluctuations.Hierarchy.ClockTree.pairPower_leaves line 141
  12. theorem OAI.SKFluctuations.Hierarchy.ClockTree.powerClock_leaves line 147
  13. theorem OAI.SKFluctuations.Hierarchy.ClockTree.pairPower_forkCost line 154
  14. theorem OAI.SKFluctuations.Hierarchy.ClockTree.powerClock_forkCost line 163
  15. theorem OAI.SKFluctuations.Hierarchy.ClockTree.powerClock_expect line 172
  16. theorem OAI.SKFluctuations.Hierarchy.MassOrdered.suffix_end line 206
  17. def OAI.SKFluctuations.Hierarchy.stepPowerMean line 212
  18. def OAI.SKFluctuations.Hierarchy.stepPowerDisorder line 218
  19. theorem OAI.SKFluctuations.Hierarchy.ZeroClockRefinement.powerMean line 224
  20. theorem OAI.SKFluctuations.Hierarchy.ZeroClockRefinement.powerDisorder line 234
  21. theorem OAI.SKFluctuations.Hierarchy.ClockTree.powerClock_expect_stepPowerMean line 241
  22. theorem OAI.SKFluctuations.Hierarchy.ClockTree.powerDisorder_coordinates line 255
  23. theorem OAI.SKFluctuations.physicalPowerMoment_eq_stepPowerDisorder line 297
  24. theorem OAI.SKFluctuations.Hierarchy.ClockTree.powerDisorder_l1_comparison line 331
  25. theorem OAI.SKFluctuations.Hierarchy.ClockTree.powerDisorder_cumulative_comparison line 353
  26. theorem OAI.SKFluctuations.Hierarchy.stepPowerDisorder_sameMasses line 395
  27. theorem OAI.SKFluctuations.Hierarchy.stepPowerDisorder_l1_comparison line 483
  28. def OAI.SKFluctuations.Hierarchy.sampledPowerDisorder line 526
  29. theorem OAI.SKFluctuations.Hierarchy.sampledPowerDisorder_mesh_comparison line 530
  30. def OAI.SKFluctuations.Hierarchy.retainedPowerSample line 577
  31. theorem OAI.SKFluctuations.Hierarchy.retainedPowerSample_comparison line 582
  32. theorem OAI.SKFluctuations.Hierarchy.retainedPowerSample_cauchy line 600
  33. def OAI.SKFluctuations.Hierarchy.pathPowerDisorder line 625
  34. theorem OAI.SKFluctuations.Hierarchy.retainedPowerSample_tendsto line 629