OAI/Probability/SKFluctuations/PhysicalPinnedWindow.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

Physical Pinned Window.

  1. theorem OAI.SKFluctuations.terminalScore_spin_zero line 15
  2. theorem OAI.SKFluctuations.terminalScore_spin_succ line 24
  3. theorem OAI.SKFluctuations.physicalPinnedPair_fst_eq_window line 32
  4. theorem OAI.SKFluctuations.actualSpinPath_rooted_martingale line 73
  5. theorem OAI.SKFluctuations.physicalPinnedPair_sqnorm_le line 85
  6. theorem OAI.SKFluctuations.physicalPinnedPair_fst_memLp line 136
  7. theorem OAI.SKFluctuations.integral_physicalPinnedPair_fst line 154
  8. theorem OAI.SKFluctuations.physical_window_square_moment_le line 192
  9. theorem OAI.SKFluctuations.rootedHierarchyPathLaw_eq_physical line 248
  10. theorem OAI.SKFluctuations.integral_physical_window_mean_le line 254
  11. theorem OAI.SKFluctuations.physical_raw_window_bound line 281
  12. theorem OAI.SKFluctuations.orderedOverlap_normalized line 339
  13. theorem OAI.SKFluctuations.hierarchyPairMean_overlap_eq_norm line 345
  14. theorem OAI.SKFluctuations.actualSpinPath_norm_sq_at_cut line 358
  15. theorem OAI.SKFluctuations.physicalSecondMoment_eq_stepPairDisorder line 370
  16. def OAI.SKFluctuations.physicalPathSecondMoment line 403
  17. theorem OAI.SKFluctuations.physicalSecondMoment_eq_stepPairMoment line 408
  18. theorem OAI.SKFluctuations.physicalRetainedSecondMoment_tendsto line 424
  19. theorem OAI.SKFluctuations.Hierarchy.levelPairMean_prefix line 454
  20. theorem OAI.SKFluctuations.Hierarchy.stepPairMean_eq_levelPairMean line 465
  21. theorem OAI.SKFluctuations.physicalSecondMoment_eq_rootLevelPairMean line 480
  22. theorem OAI.SKFluctuations.physicalPathSecondMoment_mono line 494
  23. theorem OAI.SKFluctuations.physicalRetainedSecondMoment_eventually_uniform line 502
  24. def OAI.SKFluctuations.Hierarchy.retainMasses line 533
  25. theorem OAI.SKFluctuations.Hierarchy.retainMasses_ordered line 536
  26. theorem OAI.SKFluctuations.Hierarchy.retainMasses_mesh line 545
  27. theorem OAI.SKFluctuations.Hierarchy.retainMasses_end line 555
  28. theorem OAI.SKFluctuations.Hierarchy.mem_retainMasses line 564
  29. def OAI.SKFluctuations.Hierarchy.finiteCutMasses line 573
  30. theorem OAI.SKFluctuations.Hierarchy.finiteCutMasses_ordered line 576
  31. theorem OAI.SKFluctuations.Hierarchy.finiteCutMasses_mesh line 580
  32. theorem OAI.SKFluctuations.Hierarchy.finiteCutMasses_end line 585
  33. theorem OAI.SKFluctuations.Hierarchy.finiteCutMasses_nodes line 589
  34. theorem OAI.SKFluctuations.finiteRetainedMeans_eventually line 597