OAI/Probability/SKFluctuations/ReplicaProfileStepIdentification.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

Replica Profile Step Identification.

  1. theorem OAI.SKFluctuations.Hierarchy.profileCovarianceRate_step_eq line 22
  2. def OAI.SKFluctuations.Hierarchy.ClockTree.single line 100
  3. def OAI.SKFluctuations.Hierarchy.ClockTree.singleEquiv line 104
  4. def OAI.SKFluctuations.Hierarchy.ClockTree.singleSlot line 108
  5. theorem OAI.SKFluctuations.Hierarchy.ClockTree.single_atSlot line 112
  6. def OAI.SKFluctuations.Hierarchy.ClockTree.slotEquiv line 118
  7. theorem OAI.SKFluctuations.Hierarchy.ClockTree.realize_atSlot line 124
  8. theorem OAI.SKFluctuations.Hierarchy.ClockTree.realize_splitIndex line 132
  9. structure OAI.SKFluctuations.Hierarchy.ClockTree.MarkedPlacement line 140
  10. def OAI.SKFluctuations.Hierarchy.ClockTree.MarkedPlacement.fresh line 152
  11. def OAI.SKFluctuations.Hierarchy.ClockTree.MarkedPlacement.coincide line 162
  12. def OAI.SKFluctuations.Hierarchy.ClockTree.MarkedPlacement.step line 172
  13. def OAI.SKFluctuations.Hierarchy.ClockTree.MarkedPlacement.left line 183
  14. def OAI.SKFluctuations.Hierarchy.ClockTree.MarkedPlacement.right line 196
  15. def OAI.SKFluctuations.Hierarchy.ClockTree.MarkedPlacement.realize line 211
  16. def OAI.SKFluctuations.Hierarchy.ClockTree.markedAttach line 230
  17. structure OAI.SKFluctuations.Hierarchy.ReplicaTree.SingleBranch line 249
  18. def OAI.SKFluctuations.Hierarchy.ReplicaTree.SingleBranch.canonical line 257
  19. def OAI.SKFluctuations.Hierarchy.ReplicaTree.SingleBranch.step line 263
  20. def OAI.SKFluctuations.Hierarchy.ReplicaTree.SingleBranch.fromClock line 270
  21. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.SingleBranch.fromClock_canonical line 280
  22. def OAI.SKFluctuations.Hierarchy.ReplicaTree.MarkedPlacement.freshFrom line 291
  23. theorem OAI.SKFluctuations.Hierarchy.ClockTree.MarkedPlacement.realize_step line 314
  24. theorem OAI.SKFluctuations.Hierarchy.ClockTree.MarkedPlacement.realize_coincide line 318
  25. theorem OAI.SKFluctuations.Hierarchy.ClockTree.MarkedPlacement.realize_left line 321
  26. theorem OAI.SKFluctuations.Hierarchy.ClockTree.MarkedPlacement.realize_right line 340
  27. theorem OAI.SKFluctuations.Hierarchy.ClockTree.MarkedPlacement.realize_fresh line 359
  28. theorem OAI.SKFluctuations.Hierarchy.ClockTree.markedAttach_realize line 386
  29. def OAI.SKFluctuations.Hierarchy.ReplicaTree.integratedKernel line 429
  30. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.kernelIncrement_integratedKernel line 433
  31. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.profilePair_test_finsetSum line 438
  32. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.profilePair_test_smul line 447
  33. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.profileCovarianceRate_eq_pair line 459
  34. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.profileCovarianceRate_test_finsetSum line 472
  35. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.profileCovarianceRate_test_smul line 483
  36. theorem OAI.SKFluctuations.Hierarchy.pair_indicator line 504
  37. theorem OAI.SKFluctuations.Hierarchy.profileCovarianceRate_fork_product line 512
  38. theorem OAI.SKFluctuations.Hierarchy.ClockTree.eval_weightExpr_expect line 536
  39. theorem OAI.SKFluctuations.Hierarchy.ClockTree.profileCovarianceRate_weight line 547