OAI/Probability/SKFluctuations/FeatureClockResponse.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

Feature Clock Response.

  1. def OAI.SKFluctuations.Hierarchy.featureClockResponse line 20
  2. theorem OAI.SKFluctuations.Hierarchy.featureClockResponse_bound line 26
  3. theorem OAI.SKFluctuations.Hierarchy.parametric_featureClock line 45
  4. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.clockResponse_smooth0 line 66
  5. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.parametric_clockTest line 76
  6. theorem OAI.SKFluctuations.Hierarchy.finite_law_variation_dual line 105
  7. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.clockTest_atomic line 125
  8. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.clockResponse_atomic line 146
  9. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.atomic_clockResponse_variation line 165
  10. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.atomic_clockTest_probability line 178
  11. inductive OAI.SKFluctuations.Hierarchy.BoundaryTree line 210
  12. def OAI.SKFluctuations.Hierarchy.BoundaryTree.Assignment line 218
  13. def OAI.SKFluctuations.Hierarchy.BoundaryTree.assignmentFintype line 224
  14. def OAI.SKFluctuations.Hierarchy.BoundaryTree.weight line 233
  15. def OAI.SKFluctuations.Hierarchy.BoundaryTree.response line 242
  16. theorem OAI.SKFluctuations.Hierarchy.BoundaryTree.parametric line 252
  17. theorem OAI.SKFluctuations.Hierarchy.BoundaryTree.weight_smooth0 line 271
  18. theorem OAI.SKFluctuations.Hierarchy.BoundaryTree.response_smooth0 line 280
  19. theorem OAI.SKFluctuations.Hierarchy.BoundaryTree.probability line 289
  20. theorem OAI.SKFluctuations.Hierarchy.BddSmooth.abs_zero line 322
  21. theorem OAI.SKFluctuations.Hierarchy.sum_abs_shiftedMean_le line 327
  22. theorem OAI.SKFluctuations.Hierarchy.finite_law_score_fork line 342
  23. theorem OAI.SKFluctuations.Hierarchy.finite_law_subtraction_bound line 366
  24. def OAI.SKFluctuations.Hierarchy.PrefixOrdered line 389
  25. theorem OAI.SKFluctuations.Hierarchy.PrefixOrdered.positive line 393
  26. theorem OAI.SKFluctuations.Hierarchy.PrefixOrdered.bounds line 404
  27. def OAI.SKFluctuations.Hierarchy.BoundaryTree.budget line 412
  28. def OAI.SKFluctuations.Hierarchy.BoundaryTree.score line 419
  29. theorem OAI.SKFluctuations.Hierarchy.BoundaryTree.score_smooth0 line 425
  30. theorem OAI.SKFluctuations.Hierarchy.BoundaryTree.score_step line 436
  31. theorem OAI.SKFluctuations.Hierarchy.BoundaryTree.score_variation line 464
  32. theorem OAI.SKFluctuations.Hierarchy.finite_law_addition_bound line 518
  33. def OAI.SKFluctuations.Hierarchy.BoundaryTree.expect line 527
  34. theorem OAI.SKFluctuations.Hierarchy.BoundaryTree.expect_hasDerivAt line 532
  35. theorem OAI.SKFluctuations.Hierarchy.BoundaryTree.tested_response_bound line 542
  36. def OAI.SKFluctuations.Hierarchy.ReplicaTree.atomicClock line 563
  37. def OAI.SKFluctuations.Hierarchy.ReplicaTree.atomicResponse line 569
  38. theorem OAI.SKFluctuations.Hierarchy.BoundaryTree.actual_inserted_response_variation line 577
  39. def OAI.SKFluctuations.Hierarchy.interpolate line 624
  40. theorem OAI.SKFluctuations.Hierarchy.interpolate_derivative line 628
  41. theorem OAI.SKFluctuations.Hierarchy.parametric_interpolate line 634
  42. theorem OAI.SKFluctuations.Hierarchy.parametricTest_interpolate line 643
  43. theorem OAI.SKFluctuations.Hierarchy.ParametricRegular.restrict line 661
  44. theorem OAI.SKFluctuations.Hierarchy.ParametricTest.restrict line 667