OAI/Probability/SKFluctuations/ClockRetainedSamples.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

Clock Retained Samples.

  1. def OAI.SKFluctuations.Hierarchy.retainedBefore line 17
  2. def OAI.SKFluctuations.Hierarchy.retainedAfter line 19
  3. theorem OAI.SKFluctuations.Hierarchy.retainedBefore_end line 22
  4. theorem OAI.SKFluctuations.Hierarchy.retainedAfter_end line 24
  5. theorem OAI.SKFluctuations.Hierarchy.retainedBefore_bounds line 28
  6. theorem OAI.SKFluctuations.Hierarchy.retainedMasses_ordered line 30
  7. theorem OAI.SKFluctuations.Hierarchy.retainedMasses_mesh line 35
  8. def OAI.SKFluctuations.Hierarchy.retainedPairSample line 42
  9. theorem OAI.SKFluctuations.Hierarchy.retainedPairSample_comparison line 47
  10. theorem OAI.SKFluctuations.Hierarchy.retainedPairSample_cauchy line 65
  11. def OAI.SKFluctuations.Hierarchy.pathPairDisorder line 90
  12. theorem OAI.SKFluctuations.Hierarchy.retainedPairSample_tendsto line 94
  13. theorem OAI.SKFluctuations.Hierarchy.partitionSample_cross_error line 115
  14. def OAI.SKFluctuations.Hierarchy.clockL1Distance line 145
  15. theorem OAI.SKFluctuations.Hierarchy.sampledDisorderPressure_cross_comparison line 148
  16. theorem OAI.SKFluctuations.Hierarchy.pathDisorderPressure_l1_comparison line 182
  17. theorem OAI.SKFluctuations.Hierarchy.stepClockFunction_intervalIntegrable line 214
  18. theorem OAI.SKFluctuations.Hierarchy.partitionSample_compare_integral line 220
  19. def OAI.SKFluctuations.Hierarchy.stepPathClockDistance line 236
  20. theorem OAI.SKFluctuations.Hierarchy.stepDisorderPressure_path_comparison line 240
  21. theorem OAI.SKFluctuations.Hierarchy.stepDisorderPressure_tendsto_path line 281
  22. theorem OAI.SKFluctuations.Hierarchy.clockCoordinateDistance_integral line 306
  23. theorem OAI.SKFluctuations.Hierarchy.stepClock_sample_distance line 316
  24. def OAI.SKFluctuations.Hierarchy.stepPathPairDistance line 344
  25. theorem OAI.SKFluctuations.Hierarchy.stepPairDisorder_sample_comparison line 363
  26. theorem OAI.SKFluctuations.Hierarchy.stepPairDisorder_path_comparison line 397
  27. theorem OAI.SKFluctuations.Hierarchy.stepPairDisorder_tendsto_path line 422
  28. theorem OAI.SKFluctuations.Hierarchy.partitionSample_comp line 449
  29. theorem OAI.SKFluctuations.Hierarchy.partitionSample_id_bounds line 457
  30. theorem OAI.SKFluctuations.Hierarchy.partitionSample_tendsto line 473
  31. theorem OAI.SKFluctuations.Hierarchy.uniformSample_tendsto line 496
  32. def OAI.SKFluctuations.Hierarchy.pathPairMoment line 514
  33. theorem OAI.SKFluctuations.Hierarchy.stepPairMoment_path_comparison line 518
  34. theorem OAI.SKFluctuations.Hierarchy.sample_stepPathClockDistance_le line 539
  35. theorem OAI.SKFluctuations.Hierarchy.stepPathClockDistance_nonneg line 555
  36. theorem OAI.SKFluctuations.Hierarchy.uniformMassTail_end line 562
  37. theorem OAI.SKFluctuations.Hierarchy.uniformMasses_end line 570
  38. theorem OAI.SKFluctuations.Hierarchy.sampledPairMoment_tendsto line 574
  39. theorem OAI.SKFluctuations.Hierarchy.ClockTree.disorderExpect_bound line 617
  40. theorem OAI.SKFluctuations.Hierarchy.cumulativePair_bound line 633
  41. theorem OAI.SKFluctuations.Hierarchy.stepPairMoment_bound line 639
  42. theorem OAI.SKFluctuations.Hierarchy.stepPairDisorder_bound line 649
  43. theorem OAI.SKFluctuations.Hierarchy.pathPairMoment_bound line 663