OAI/Probability/SKFluctuations/ReplicaProfilePairRecursion.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

Replica Profile Pair Recursion.

  1. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.profileRow_test_const_mul line 21
  2. def OAI.SKFluctuations.Hierarchy.ReplicaTree.singleProfileRow line 28
  3. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.profileRow_fresh_mark_zero line 33
  4. def OAI.SKFluctuations.Hierarchy.ReplicaTree.profilePairList line 50
  5. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.profilePairList_smooth line 55
  6. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.profilePairList_map_step_zero line 65
  7. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.profilePair_step_zero line 90
  8. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.profilePairList_map_left_zero line 117
  9. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.profilePairList_map_right_zero line 132
  10. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.profilePair_fork_zero line 147
  11. def OAI.SKFluctuations.Hierarchy.ReplicaTree.kernelIncrement line 183
  12. def OAI.SKFluctuations.Hierarchy.ReplicaTree.profilePressure line 186
  13. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.profileRow_zero line 194
  14. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.profilePair_zero line 200
  15. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.singleProfileRow_leaf_zero line 206
  16. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.singleProfileRow_add line 212
  17. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.singleProfileRow_eq_pressure line 222
  18. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.profilePair_nil_zero line 275
  19. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.expect_mul_const line 283
  20. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.expect_fork_reverse line 289
  21. def OAI.SKFluctuations.Hierarchy.ReplicaTree.profileCovarianceRate line 305
  22. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.profilePair_eq_covarianceRate line 323
  23. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.profileRow_finsetSum line 408
  24. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.profilePairExpectation_finsetSum line 417
  25. def OAI.SKFluctuations.Hierarchy.ReplicaTree.coordinateProfile line 427
  26. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.coordinateProfile_add line 431
  27. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.coordinateProfile_sub line 438
  28. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.profilePair_coordinate_const line 444
  29. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.single_source_one_response line 458
  30. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.singleProfileRow_coordinate_const line 473
  31. theorem OAI.SKFluctuations.Hierarchy.single_fin_classical line 500
  32. theorem OAI.SKFluctuations.Hierarchy.ClockExpr.eval_grad_source line 507
  33. theorem OAI.SKFluctuations.Hierarchy.ClockExpr.eval_step_coordSum line 521
  34. theorem OAI.SKFluctuations.Hierarchy.profilePressure_eq_eval line 538
  35. theorem OAI.SKFluctuations.Hierarchy.ClockExpr.eval_source_of_expect line 589
  36. theorem OAI.SKFluctuations.Hierarchy.ClockExpr.eval_source_two_of_expect line 602
  37. theorem OAI.SKFluctuations.Hierarchy.profilePair_const_eq_testedInsert line 616