OAI/Probability/SKFluctuations/OrderedSKCumulativeChord.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

Ordered S K Cumulative Chord.

  1. theorem OAI.SKFluctuations.orderedSK_cumulative_chord line 21
  2. theorem OAI.SKFluctuations.Hierarchy.massStepSum_sub line 85
  3. def OAI.SKFluctuations.finiteCompensatedPressure line 104
  4. theorem OAI.SKFluctuations.finiteCompensatedPressure_mono line 111
  5. theorem OAI.SKFluctuations.finiteCompensatedPressure_lower line 143
  6. theorem OAI.SKFluctuations.Hierarchy.hierarchyPairMean_square line 169
  7. def OAI.SKFluctuations.Hierarchy.levelPairMean line 188
  8. theorem OAI.SKFluctuations.Hierarchy.levelPairMean_smooth line 195
  9. theorem OAI.SKFluctuations.Hierarchy.levelPairMean_const line 209
  10. theorem OAI.SKFluctuations.Hierarchy.levelPairMean_mono line 223
  11. theorem OAI.SKFluctuations.Hierarchy.levelPairMean_square line 238
  12. def OAI.SKFluctuations.Hierarchy.rootLevelPairMean line 268
  13. theorem OAI.SKFluctuations.Hierarchy.rootLevelPairMean_mono line 272
  14. theorem OAI.SKFluctuations.Hierarchy.rootLevelPairMean_const line 282
  15. theorem OAI.SKFluctuations.Hierarchy.rootLevelPairMean_square line 290
  16. theorem OAI.SKFluctuations.Hierarchy.hierarchyPairMean_sum line 309
  17. theorem OAI.SKFluctuations.Hierarchy.hierarchyPairMean_const_mul line 319
  18. theorem OAI.SKFluctuations.orderedOverlap_abs_le_one line 333
  19. theorem OAI.SKFluctuations.hierarchyPairMean_overlap_nonneg line 345
  20. theorem OAI.SKFluctuations.levelPairMean_overlap_nonneg line 358
  21. theorem OAI.SKFluctuations.rootLevelPairMean_SK_bounds line 373
  22. theorem OAI.SKFluctuations.Hierarchy.massStepSum_smooth line 403
  23. theorem OAI.SKFluctuations.Hierarchy.shiftedMean_massStepSum line 413
  24. theorem OAI.SKFluctuations.Hierarchy.zeroContinuation_massStepSum line 427
  25. def OAI.SKFluctuations.Hierarchy.clockPairReward line 440
  26. theorem OAI.SKFluctuations.Hierarchy.clockPairReward_eq_massStepSum line 448
  27. theorem OAI.SKFluctuations.Hierarchy.clockPairReward_smooth line 464
  28. theorem OAI.SKFluctuations.Hierarchy.zero_clockPairReward_eq_massStepSum line 472
  29. def OAI.SKFluctuations.Hierarchy.interpolatedIncrements line 491
  30. theorem OAI.SKFluctuations.Hierarchy.affineSteps_signedClock_eq line 495
  31. theorem OAI.SKFluctuations.Hierarchy.pathKernelPenalty_signedClock_eq line 504
  32. theorem OAI.SKFluctuations.Hierarchy.root_pathKernelPenalty_eq_massStepSum line 527
  33. theorem OAI.SKFluctuations.GaussianCalculus.hasDerivAt_integral_scaledSource line 547
  34. theorem OAI.SKFluctuations.GaussianCalculus.hasDerivAt_signed_zeroContinuation line 583