OAI/Probability/SKFluctuations/BoundaryCostCongr.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

Boundary Cost Congr.

  1. theorem OAI.SKFluctuations.Hierarchy.boundaryCost_congr line 19
  2. theorem OAI.SKFluctuations.Hierarchy.rootBoundaryCost_congr line 37
  3. theorem OAI.SKFluctuations.Hierarchy.rootBoundaryCost_uniform line 48
  4. def OAI.SKFluctuations.Hierarchy.correctedDiagonalRoot line 62
  5. theorem OAI.SKFluctuations.Hierarchy.correctedDiagonalRoot_comparison line 71
  6. inductive OAI.SKFluctuations.Hierarchy.ClockTree line 136
  7. def OAI.SKFluctuations.Hierarchy.ClockTree.Assignment line 143
  8. def OAI.SKFluctuations.Hierarchy.ClockTree.assignmentFintype line 148
  9. def OAI.SKFluctuations.Hierarchy.MassOrdered line 155
  10. def OAI.SKFluctuations.Hierarchy.clockSteps line 159
  11. def OAI.SKFluctuations.Hierarchy.ClockTree.realize line 163
  12. def OAI.SKFluctuations.Hierarchy.ClockTree.assignmentEquiv line 169
  13. def OAI.SKFluctuations.Hierarchy.ClockTree.leaves line 175
  14. theorem OAI.SKFluctuations.Hierarchy.ClockTree.realize_leaves line 180
  15. def OAI.SKFluctuations.Hierarchy.ClockTree.weight line 189
  16. def OAI.SKFluctuations.Hierarchy.ClockTree.expect line 194
  17. theorem OAI.SKFluctuations.Hierarchy.ClockTree.expect_realize line 198
  18. theorem OAI.SKFluctuations.Hierarchy.ClockTree.weight_leaf line 205
  19. theorem OAI.SKFluctuations.Hierarchy.ClockTree.weight_step line 209
  20. theorem OAI.SKFluctuations.Hierarchy.ClockTree.weight_fork line 216
  21. theorem OAI.SKFluctuations.Hierarchy.clockSteps_ordered line 222
  22. theorem OAI.SKFluctuations.Hierarchy.ClockTree.weight_smooth line 230
  23. theorem OAI.SKFluctuations.Hierarchy.ClockTree.weight_probability line 235
  24. def OAI.SKFluctuations.Hierarchy.ClockTree.cut line 255
  25. def OAI.SKFluctuations.Hierarchy.ClockTree.cutAssignmentEquiv line 262
  26. theorem OAI.SKFluctuations.Hierarchy.clockSteps_append line 272
  27. theorem OAI.SKFluctuations.Hierarchy.clockSteps_take_drop line 284
  28. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchy_prefix line 289
  29. theorem OAI.SKFluctuations.Hierarchy.ClockTree.cut_weight line 302
  30. def OAI.SKFluctuations.Hierarchy.mixClocks line 359
  31. theorem OAI.SKFluctuations.Hierarchy.mixClocks_zero line 362
  32. theorem OAI.SKFluctuations.Hierarchy.mixClocks_succ_zero line 366
  33. theorem OAI.SKFluctuations.Hierarchy.mixClocks_succ_shift line 369
  34. theorem OAI.SKFluctuations.Hierarchy.clockSteps_mix line 374
  35. theorem OAI.SKFluctuations.Hierarchy.ClockTree.cut_mix_weight line 394
  36. theorem OAI.SKFluctuations.Hierarchy.ClockTree.cut_mix_distance line 434
  37. theorem OAI.SKFluctuations.Hierarchy.ClockTree.cut_mix_stability line 450
  38. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.diagonal_covariance_transfer line 479
  39. theorem OAI.SKFluctuations.Hierarchy.ParametricContinuous.mulTest line 547
  40. theorem OAI.SKFluctuations.Hierarchy.BoundaryTree.parametricContinuous line 560
  41. theorem OAI.SKFluctuations.Hierarchy.abs_sub_le_mul_of_deriv_interior line 584
  42. theorem OAI.SKFluctuations.Hierarchy.BoundaryTree.actual_clock_variation line 606
  43. theorem OAI.SKFluctuations.Hierarchy.linearClockContinuation_zero line 660
  44. theorem OAI.SKFluctuations.Hierarchy.linearClockTest_zero line 666
  45. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.atomicClock_zero line 672
  46. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.atomic_clock_variation line 680