OAI/Probability/SKFluctuations/ClockPathPairMeasurable.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

Clock Path Pair Measurable.

  1. theorem OAI.SKFluctuations.Hierarchy.monotoneOn_ae_continuous line 17
  2. theorem OAI.SKFluctuations.Hierarchy.sampledPairMoment_ae_tendsto line 22
  3. theorem OAI.SKFluctuations.Hierarchy.pathPairMoment_aestronglyMeasurable line 38
  4. theorem OAI.SKFluctuations.Hierarchy.pathPairMoment_intervalIntegrable line 50
  5. theorem OAI.SKFluctuations.Hierarchy.clockCoordinateDistance_intervalIntegrable line 74
  6. theorem OAI.SKFluctuations.Hierarchy.stepPairMoment_l1_path_comparison line 85
  7. theorem OAI.SKFluctuations.Hierarchy.sampledPairMoment_l1_bound line 126
  8. theorem OAI.SKFluctuations.Hierarchy.disorderPressure_regularized_bound line 157
  9. def OAI.SKFluctuations.Hierarchy.pressureRate line 186
  10. theorem OAI.SKFluctuations.Hierarchy.pressureRate_regularized_bound line 190
  11. theorem OAI.SKFluctuations.Hierarchy.disorderPressure_regularized_hasDerivAt line 206
  12. theorem OAI.SKFluctuations.Hierarchy.disorderPressure_hasDerivAt_nonneg_bounded line 248
  13. theorem OAI.SKFluctuations.Hierarchy.disorderPressure_hasDerivAt_nonneg line 291
  14. theorem OAI.SKFluctuations.Hierarchy.ClockTree.expect_zeroShift_integrable line 328
  15. theorem OAI.SKFluctuations.Hierarchy.ClockTree.disorderExpect_finsetSum line 337
  16. theorem OAI.SKFluctuations.Hierarchy.ClockTree.disorderExpect_const_mul line 353
  17. def OAI.SKFluctuations.Hierarchy.coordinatePairTest line 362
  18. theorem OAI.SKFluctuations.Hierarchy.cumulativePair_featureKernel line 366
  19. theorem OAI.SKFluctuations.Hierarchy.massStepFunction_mul line 376
  20. theorem OAI.SKFluctuations.Hierarchy.massStepFunction_sum line 382
  21. theorem OAI.SKFluctuations.Hierarchy.pressureRate_integral line 394
  22. theorem OAI.SKFluctuations.Hierarchy.partitionValues_zero line 423
  23. def OAI.SKFluctuations.Hierarchy.partitionPoint line 426
  24. theorem OAI.SKFluctuations.Hierarchy.partitionValues_point line 429
  25. theorem OAI.SKFluctuations.Hierarchy.partitionPoint_mem line 437
  26. theorem OAI.SKFluctuations.Hierarchy.partitionPoint_mono line 447
  27. theorem OAI.SKFluctuations.Hierarchy.partitionValues_mono line 457
  28. theorem OAI.SKFluctuations.Hierarchy.sampledDisorderPressure_eq line 469
  29. def OAI.SKFluctuations.Hierarchy.affineClockPath line 494
  30. theorem OAI.SKFluctuations.Hierarchy.affineClockPath_coe line 498
  31. theorem OAI.SKFluctuations.Hierarchy.affineClockPath_monotone line 504
  32. theorem OAI.SKFluctuations.Hierarchy.affineClockPath_variation line 511
  33. theorem OAI.SKFluctuations.Hierarchy.affineClockPath_variation_le line 522
  34. theorem OAI.SKFluctuations.Hierarchy.sampledAffinePressure_hasDerivAt line 533