OAI/Probability/SKFluctuations/ReplicaProfileDifferentiation.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Replica Profile Differentiation.

  1. theorem OAI.SKFluctuations.Hierarchy.ClockTree.profileCovarianceRate_expand line 23
  2. theorem OAI.SKFluctuations.Hierarchy.ClockTree.hasDerivAt_profileCovarianceRate line 49
  3. theorem OAI.SKFluctuations.Hierarchy.ClockTree.hasDerivAt_profilePair line 82
  4. theorem OAI.SKFluctuations.Hierarchy.ClockTree.MarkedPlacement.realize_restrict line 116
  5. theorem OAI.SKFluctuations.Hierarchy.ClockTree.MarkedPlacement.realize_spin line 123
  6. theorem OAI.SKFluctuations.Hierarchy.ClockTree.MarkedPlacement.realize_embed line 129
  7. def OAI.SKFluctuations.Hierarchy.ClockTree.profilePairTest line 137
  8. def OAI.SKFluctuations.Hierarchy.ClockTree.profilePair line 145
  9. theorem OAI.SKFluctuations.Hierarchy.ClockTree.profilePair_realize line 152
  10. def OAI.SKFluctuations.Hierarchy.ClockExpr.homSum line 191
  11. theorem OAI.SKFluctuations.Hierarchy.ClockExpr.eval_homSum line 195
  12. theorem OAI.SKFluctuations.Hierarchy.ClockExpr.covariance_eval_homSum line 204
  13. def OAI.SKFluctuations.Hierarchy.ClockTree.homTest line 214
  14. theorem OAI.SKFluctuations.Hierarchy.ClockTree.eval_homTest line 220
  15. theorem OAI.SKFluctuations.Hierarchy.ClockTree.covariance_eval_homTest line 232
  16. theorem OAI.SKFluctuations.Hierarchy.ClockTree.rootCov_eq_profilePair line 242
  17. theorem OAI.SKFluctuations.Hierarchy.ClockExpr.rootEval_homSum line 290
  18. def OAI.SKFluctuations.Hierarchy.ClockTree.rootExpect line 304
  19. theorem OAI.SKFluctuations.Hierarchy.ClockTree.rootExpect_eq_integral line 310
  20. def OAI.SKFluctuations.Hierarchy.ClockTree.profileExpr line 324
  21. theorem OAI.SKFluctuations.Hierarchy.ClockTree.eval_profileExpr line 331
  22. def OAI.SKFluctuations.Hierarchy.ClockTree.rootProfilePair line 341
  23. theorem OAI.SKFluctuations.Hierarchy.ClockTree.rootEval_profileExpr line 349
  24. theorem OAI.SKFluctuations.Hierarchy.ClockTree.hasDerivAt_rootProfilePair line 361
  25. def OAI.SKFluctuations.Hierarchy.ClockTree.rootProfileJets line 396
  26. theorem OAI.SKFluctuations.Hierarchy.hasDerivAt_listSum line 407
  27. theorem OAI.SKFluctuations.Hierarchy.ClockTree.hasDerivAt_rootProfileJets line 418
  28. theorem OAI.SKFluctuations.Hierarchy.ClockTree.iteratedDeriv_rootProfileJets line 439
  29. theorem OAI.SKFluctuations.Hierarchy.ClockTree.markedAttach_variation line 476
  30. theorem OAI.SKFluctuations.Hierarchy.ClockTree.markedAttach_leaves line 484
  31. theorem OAI.SKFluctuations.Hierarchy.ClockTree.marked_list_weight_abs_le line 495
  32. theorem OAI.SKFluctuations.Hierarchy.ClockTree.rootExpect_abs_le line 509
  33. def OAI.SKFluctuations.Hierarchy.ClockTree.jetVariation line 533
  34. theorem OAI.SKFluctuations.Hierarchy.ClockTree.jetVariation_nonneg line 537
  35. theorem OAI.SKFluctuations.Hierarchy.ClockTree.marked_pair_weight_abs_le line 544
  36. theorem OAI.SKFluctuations.Hierarchy.ClockTree.rootProfileJets_abs_le line 577