OAI/Probability/SKFluctuations/ClockPathPressureSup.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Clock Path Pressure Sup.

  1. theorem OAI.SKFluctuations.Hierarchy.clockL1Distance_le line 18
  2. theorem OAI.SKFluctuations.Hierarchy.pathDisorderPressure_sup_comparison line 36
  3. theorem OAI.SKFluctuations.Hierarchy.affineClockPath_zero line 50
  4. theorem OAI.SKFluctuations.Hierarchy.affineClockPath_one line 54
  5. theorem OAI.SKFluctuations.Hierarchy.affineClockPath_difference line 59
  6. theorem OAI.SKFluctuations.Hierarchy.pathDisorderPressure_affine_continuousOn line 67
  7. theorem OAI.SKFluctuations.Hierarchy.intervalIntegral_mul_abs_le line 107
  8. theorem OAI.SKFluctuations.Hierarchy.pathPressureRate_sup_comparison line 124
  9. theorem OAI.SKFluctuations.Hierarchy.pathDisorderPressure_taylor line 189
  10. theorem OAI.SKFluctuations.Hierarchy.pathPressureRate_const_mul line 233
  11. theorem OAI.SKFluctuations.Hierarchy.pathPressureRate_direction_integrable line 240
  12. theorem OAI.SKFluctuations.Hierarchy.pathPressureRate_sub line 249
  13. theorem OAI.SKFluctuations.Hierarchy.pathPressureRate_bound line 264
  14. theorem OAI.SKFluctuations.Hierarchy.pathPressureRate_tendsto line 295
  15. theorem OAI.SKFluctuations.Hierarchy.pathDisorderPressure_slope_error line 337
  16. theorem OAI.SKFluctuations.Hierarchy.pathDisorderPressure_hasDerivWithinAt_curve line 377
  17. theorem OAI.SKFluctuations.Hierarchy.pathPressureRate_integral_direction line 434
  18. theorem OAI.SKFluctuations.Hierarchy.pathPairMoment_mul_intervalIntegrable line 450
  19. def OAI.SKFluctuations.orderedPathClock line 470
  20. theorem OAI.SKFluctuations.orderedPathClock_monotone line 473
  21. def OAI.SKFluctuations.orderedSKPathPressure line 481
  22. theorem OAI.SKFluctuations.orderedPathClock_l1 line 486
  23. theorem OAI.SKFluctuations.orderedSKPathPressure_l1_comparison line 506
  24. def OAI.SKFluctuations.orderedPathPair line 537
  25. def OAI.SKFluctuations.orderedPathS line 539
  26. def OAI.SKFluctuations.orderedPathB line 541
  27. theorem OAI.SKFluctuations.orderedPathPair_linear line 544
  28. theorem OAI.SKFluctuations.orderedPathPair_direction_integrable line 555
  29. theorem OAI.SKFluctuations.pathPressureRate_ordered line 569
  30. def OAI.SKFluctuations.affineNNPath line 622
  31. theorem OAI.SKFluctuations.affineNNPath_monotone line 625
  32. theorem OAI.SKFluctuations.orderedSKPathPressure_hasDerivAt line 632