OAI/Probability/SKFluctuations/PhysicalTerminalPairLaw.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Physical Terminal Pair Law.

  1. def OAI.SKFluctuations.Hierarchy.terminalPairTest line 17
  2. theorem OAI.SKFluctuations.Hierarchy.terminalPairTest_measurable line 23
  3. theorem OAI.SKFluctuations.Hierarchy.terminalPairTest_abs_le line 31
  4. theorem OAI.SKFluctuations.Hierarchy.integral_terminalFork_zero line 41
  5. theorem OAI.SKFluctuations.Hierarchy.integral_terminalFork_eq_levelPairMean line 70
  6. theorem OAI.SKFluctuations.physicalOverlapMoment_eq_stepPairDisorder line 132
  7. theorem OAI.SKFluctuations.physicalOverlapMoment_eq_stepPairMoment line 152
  8. theorem OAI.SKFluctuations.physicalRetainedOverlapMoment_tendsto line 167
  9. theorem OAI.SKFluctuations.eventually_comparison_retained_overlap_band line 196
  10. theorem OAI.SKFluctuations.completedPathOverlapMoment_le_one line 298
  11. theorem OAI.SKFluctuations.comparison_minimum_retained_overlap_moment_normalized line 328
  12. theorem OAI.SKFluctuations.Hierarchy.stepPairDisorder_zero_eq_root line 543
  13. theorem OAI.SKFluctuations.Hierarchy.pathPairMoment_mono_test line 550
  14. theorem OAI.SKFluctuations.Hierarchy.pathPairMoment_const_test line 567
  15. theorem OAI.SKFluctuations.Hierarchy.raw_rpow_normalized_interpolation line 582
  16. theorem OAI.SKFluctuations.Hierarchy.pathPairMoment_rpow_from_nat line 599