OAI/Probability/SKFluctuations/HierarchyPenalty.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Hierarchy Penalty.

  1. def OAI.SKFluctuations.Hierarchy.hierarchyPenalty line 21
  2. theorem OAI.SKFluctuations.Hierarchy.hierarchyPenalty_smooth line 29
  3. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchyResponse_mass_telescope line 46
  4. theorem OAI.SKFluctuations.Hierarchy.hierarchyPenalty_nonneg line 84
  5. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchyMean_const line 102
  6. def OAI.SKFluctuations.Hierarchy.featurePenalty line 116
  7. theorem OAI.SKFluctuations.Hierarchy.featurePenalty_smooth line 120
  8. theorem OAI.SKFluctuations.Hierarchy.featurePenalty_nonneg line 125
  9. theorem OAI.SKFluctuations.Hierarchy.feature_trace_telescope line 132
  10. theorem OAI.SKFluctuations.Hierarchy.shiftedMean_sum line 148
  11. theorem OAI.SKFluctuations.Hierarchy.clockDerivative_feature_trace line 158
  12. theorem OAI.SKFluctuations.Hierarchy.prefixContinuation_lipschitz line 191
  13. theorem OAI.SKFluctuations.Hierarchy.prefixTest_smooth0 line 203
  14. theorem OAI.SKFluctuations.Hierarchy.prefixTest_affine line 218
  15. theorem OAI.SKFluctuations.Hierarchy.prefixTest_nonneg line 237
  16. theorem OAI.SKFluctuations.Hierarchy.zeroContinuation_affine line 248
  17. theorem OAI.SKFluctuations.Hierarchy.rootedHierarchy_corrected_clock line 272
  18. theorem OAI.SKFluctuations.Hierarchy.corrected_clock_derivative_nonpos line 307
  19. theorem OAI.SKFluctuations.Hierarchy.rootedHierarchy_corrected_root line 333
  20. theorem OAI.SKFluctuations.Hierarchy.clockContinuation_continuousOn line 367
  21. theorem OAI.SKFluctuations.Hierarchy.clockTest_continuousOn line 380
  22. theorem OAI.SKFluctuations.Hierarchy.continuousWithinAt_testedPartition line 405
  23. theorem OAI.SKFluctuations.Hierarchy.continuousWithinAt_shiftedContinuation line 443
  24. theorem OAI.SKFluctuations.Hierarchy.continuousWithinAt_shiftedMean line 454
  25. theorem OAI.SKFluctuations.Hierarchy.continuousWithinAt_zeroContinuation line 477
  26. structure OAI.SKFluctuations.Hierarchy.ParametricContinuous line 508
  27. theorem OAI.SKFluctuations.Hierarchy.ParametricContinuous.step line 517
  28. theorem OAI.SKFluctuations.Hierarchy.ParametricContinuous.prefix line 537
  29. theorem OAI.SKFluctuations.Hierarchy.ParametricContinuous.root line 548
  30. theorem OAI.SKFluctuations.Hierarchy.parametric_continuous_clock line 590
  31. theorem OAI.SKFluctuations.Hierarchy.rootedHierarchy_corrected_clock_zero line 605
  32. theorem OAI.SKFluctuations.Hierarchy.rootedHierarchy_corrected_clock_nonneg line 636