OAI/Probability/SKFluctuations/ClockMassIntegral.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

Clock Mass Integral.

  1. def OAI.SKFluctuations.Hierarchy.massStepFunction line 15
  2. theorem OAI.SKFluctuations.Hierarchy.massStepFunction_intervalIntegrable line 19
  3. theorem OAI.SKFluctuations.Hierarchy.massStepFunction_integral line 30
  4. theorem OAI.SKFluctuations.Hierarchy.massStepFunction_abs_sub line 51
  5. theorem OAI.SKFluctuations.Hierarchy.boundaryCost_append_one line 58
  6. theorem OAI.SKFluctuations.Hierarchy.rootBoundaryCost_eq_integral line 75
  7. theorem OAI.SKFluctuations.Hierarchy.ClockTree.edgeBudget_eq_massStepSum line 102
  8. theorem OAI.SKFluctuations.Hierarchy.ClockTree.pairDisorder_cumulative_comparison line 109
  9. def OAI.SKFluctuations.Hierarchy.stepClockFunction line 152
  10. theorem OAI.SKFluctuations.Hierarchy.stepClockFunction_cons line 155
  11. theorem OAI.SKFluctuations.Hierarchy.stepClockFunction_before line 162
  12. theorem OAI.SKFluctuations.Hierarchy.stepClockFunction_eq line 171
  13. theorem OAI.SKFluctuations.Hierarchy.ZeroClockRefinement.clockFunction line 186
  14. theorem OAI.SKFluctuations.Hierarchy.stepDisorderPressure_l1_comparison line 197
  15. def OAI.SKFluctuations.Hierarchy.clockCoordinateDistance line 234
  16. theorem OAI.SKFluctuations.Hierarchy.clockCoordinateDistance_nonneg line 238
  17. theorem OAI.SKFluctuations.Hierarchy.stepClockValues_append_cut line 243
  18. theorem OAI.SKFluctuations.Hierarchy.massStepFunction_coordinateDistance line 250
  19. theorem OAI.SKFluctuations.Hierarchy.stepPairDisorder_sameMasses line 261
  20. theorem OAI.SKFluctuations.Hierarchy.ZeroClockRefinement.append_right line 349
  21. theorem OAI.SKFluctuations.Hierarchy.ZeroClockRefinement.append_left line 359
  22. theorem OAI.SKFluctuations.Hierarchy.ZeroClockRefinement.append line 366
  23. theorem OAI.SKFluctuations.Hierarchy.commonClockSteps_mass_le line 371
  24. theorem OAI.SKFluctuations.Hierarchy.commonClockSteps_prepost_ordered line 400
  25. theorem OAI.SKFluctuations.Hierarchy.ZeroClockRefinement.terminal line 432
  26. theorem OAI.SKFluctuations.Hierarchy.stepPairDisorder_l1_comparison line 438
  27. theorem OAI.SKFluctuations.Hierarchy.hierarchyPairMean_eq_nested line 480
  28. theorem OAI.SKFluctuations.Hierarchy.ClockTree.pairMean_eq_levelPairMean line 494
  29. theorem OAI.SKFluctuations.Hierarchy.ClockTree.pairDisorder_eq_rootLevelPairMean line 516
  30. theorem OAI.SKFluctuations.orderedPrefixPair_eq_pairDisorder line 535
  31. def OAI.SKFluctuations.Hierarchy.regularizedClock line 555
  32. theorem OAI.SKFluctuations.Hierarchy.regularizedClock_monotone line 559
  33. theorem OAI.SKFluctuations.Hierarchy.regularizedClock_strictMono line 566
  34. theorem OAI.SKFluctuations.Hierarchy.regularizedClock_affine line 574
  35. theorem OAI.SKFluctuations.Hierarchy.affineCumulative_monotone line 582
  36. theorem OAI.SKFluctuations.Hierarchy.affineCumulative_nonneg_zero line 593
  37. theorem OAI.SKFluctuations.Hierarchy.signedClockSteps_strict line 602
  38. theorem OAI.SKFluctuations.Hierarchy.massStepSum_abs_le line 619
  39. theorem OAI.SKFluctuations.Hierarchy.massStepSum_abs_bound line 628
  40. def OAI.SKFluctuations.Hierarchy.cumulativePair line 634
  41. theorem OAI.SKFluctuations.Hierarchy.cumulativePair_regularized_bound line 639