OAI/Probability/SKFluctuations/ClockSampledRate.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Clock Sampled Rate.

  1. theorem OAI.SKFluctuations.Hierarchy.sampledPairMoment_eq line 18
  2. theorem OAI.SKFluctuations.Hierarchy.massStepFunction_sub line 32
  3. theorem OAI.SKFluctuations.Hierarchy.sampledPressureRate_integral line 38
  4. theorem OAI.SKFluctuations.Hierarchy.coordinatePairTest_bound line 63
  5. theorem OAI.SKFluctuations.Hierarchy.clockDirection_bound line 71
  6. theorem OAI.SKFluctuations.Hierarchy.partitionSample_sub line 81
  7. theorem OAI.SKFluctuations.Hierarchy.clockDirection_intervalIntegrable line 86
  8. theorem OAI.SKFluctuations.Hierarchy.sampledClockDirection_l1_bound line 98
  9. theorem OAI.SKFluctuations.Hierarchy.intervalIntegrable_mul_bounded line 138
  10. theorem OAI.SKFluctuations.Hierarchy.integral_product_error_le line 147
  11. theorem OAI.SKFluctuations.Hierarchy.sampledRateCoordinate_error line 180
  12. def OAI.SKFluctuations.Hierarchy.pathPressureRate line 221
  13. def OAI.SKFluctuations.Hierarchy.pathRateApproxConstant line 225
  14. theorem OAI.SKFluctuations.Hierarchy.sampledAffineRate_error line 230
  15. theorem OAI.SKFluctuations.Hierarchy.pathDisorderPressure_hasDerivAt_bounded line 268
  16. theorem OAI.SKFluctuations.Hierarchy.pathDisorderPressure_hasDerivAt line 298
  17. theorem OAI.SKFluctuations.Hierarchy.stepPairDisorder_finsetSum line 327
  18. theorem OAI.SKFluctuations.Hierarchy.stepPairDisorder_const_mul line 343
  19. theorem OAI.SKFluctuations.Hierarchy.retainedPairSample_ordered line 359
  20. theorem OAI.SKFluctuations.Hierarchy.retainedPairSample_tendsto_all line 367
  21. theorem OAI.SKFluctuations.Hierarchy.pathPairMoment_finsetSum line 385
  22. theorem OAI.SKFluctuations.Hierarchy.pathPairMoment_const_mul line 400
  23. theorem OAI.SKFluctuations.Hierarchy.pathPairMoment_add line 425
  24. theorem OAI.SKFluctuations.Hierarchy.pathPairMoment_intervalIntegrable_all line 435
  25. theorem OAI.SKFluctuations.Hierarchy.pathPairMoment_featureKernel line 451
  26. theorem OAI.SKFluctuations.Hierarchy.pathPressureRate_integral line 464
  27. theorem OAI.SKFluctuations.Hierarchy.clockCoordinateDistance_le line 498
  28. theorem OAI.SKFluctuations.Hierarchy.sampledPairDisorder_sup_comparison line 505
  29. theorem OAI.SKFluctuations.Hierarchy.retainedPairSample_sup_comparison line 557
  30. theorem OAI.SKFluctuations.Hierarchy.pathPairDisorder_sup_comparison line 573
  31. theorem OAI.SKFluctuations.Hierarchy.pathPairMoment_sup_comparison line 588