OAI/Probability/SKFluctuations/ClockPairRepresentation.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Clock Pair Representation.

  1. def OAI.SKFluctuations.Hierarchy.ClockTree.pairClock line 23
  2. def OAI.SKFluctuations.Hierarchy.ClockTree.pairSpin line 28
  3. theorem OAI.SKFluctuations.Hierarchy.ClockTree.pairClock_expect line 35
  4. theorem OAI.SKFluctuations.Hierarchy.ClockTree.pairRootMean_eq_rootExpect line 63
  5. theorem OAI.SKFluctuations.Hierarchy.ClockTree.pairRootMean_rpow_from_second line 71
  6. theorem OAI.SKFluctuations.Hierarchy.ClockTree.rootExpect_pair_sq_le line 89
  7. theorem OAI.SKFluctuations.Hierarchy.ClockTree.profilePairTest_root_L2_envelope line 118
  8. theorem OAI.SKFluctuations.Hierarchy.ClockTree.profilePairTest_sq_le line 147
  9. theorem OAI.SKFluctuations.Hierarchy.ClockTree.rootAbsProfileJets_poweredError_le line 179
  10. theorem OAI.SKFluctuations.Hierarchy.relative_derivative_exp_comparison line 216
  11. theorem OAI.SKFluctuations.Hierarchy.ClockTree.disorderExpect_exp_comparison line 286
  12. def OAI.SKFluctuations.Hierarchy.ClockTree.erase line 327
  13. theorem OAI.SKFluctuations.Hierarchy.ClockTree.erase_realize line 333
  14. theorem OAI.SKFluctuations.Hierarchy.ClockTree.rootAbsProfileJets_triple_holder line 349
  15. def OAI.SKFluctuations.Hierarchy.pairSegmentKernel line 402
  16. def OAI.SKFluctuations.Hierarchy.segmentPairField line 410
  17. theorem OAI.SKFluctuations.Hierarchy.segmentPairField_measurable line 416
  18. theorem OAI.SKFluctuations.Hierarchy.pairSegmentKernel_markov line 426
  19. theorem OAI.SKFluctuations.Hierarchy.integral_segmentPairField_tensor line 436
  20. theorem OAI.SKFluctuations.Hierarchy.actualPairCut_law line 462
  21. theorem OAI.SKFluctuations.Hierarchy.map_compProd_eq_of_maps_eq line 490
  22. theorem OAI.SKFluctuations.Hierarchy.actualPairCut_rooted_law line 512
  23. theorem OAI.SKFluctuations.actualTwoSegmentLaw_eq_pair line 549
  24. theorem OAI.SKFluctuations.Hierarchy.hierarchyMeanPath_at_pair_left line 572
  25. theorem OAI.SKFluctuations.Hierarchy.hierarchyMeanPath_at_pair_right line 583
  26. abbrev OAI.SKFluctuations.PhysicalPathState line 600
  27. def OAI.SKFluctuations.physicalPathLaw line 603
  28. def OAI.SKFluctuations.physicalPairIncrement line 607
  29. theorem OAI.SKFluctuations.physicalPairIncrement_eq_spinPath line 614
  30. theorem OAI.SKFluctuations.physicalPairIncrement_measurable line 626