OAI/Probability/SKFluctuations/ReplicaCovarianceVariation.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

Replica Covariance Variation.

  1. theorem OAI.SKFluctuations.Hierarchy.ClockExpr.variation_actual line 22
  2. theorem OAI.SKFluctuations.Hierarchy.ClockExpr.hasDerivAt_covariance line 107
  3. def OAI.SKFluctuations.Hierarchy.ClockExpr.iterCov line 121
  4. theorem OAI.SKFluctuations.Hierarchy.ClockExpr.iteratedDeriv_eval line 126
  5. theorem OAI.SKFluctuations.Hierarchy.ClockExpr.iteratedDeriv_hasDerivAt line 144
  6. def OAI.SKFluctuations.Hierarchy.ClockExpr.rootEval line 165
  7. def OAI.SKFluctuations.Hierarchy.ClockExpr.rootCov line 170
  8. theorem OAI.SKFluctuations.Hierarchy.varianceTest_add' line 177
  9. theorem OAI.SKFluctuations.Hierarchy.ClockExpr.rootEval_add line 184
  10. theorem OAI.SKFluctuations.Hierarchy.ClockExpr.rootEval_scale line 193
  11. theorem OAI.SKFluctuations.Hierarchy.ClockExpr.rootEval_coordSum line 198
  12. theorem OAI.SKFluctuations.Hierarchy.ClockExpr.hasDerivAt_rootCov line 210
  13. theorem OAI.SKFluctuations.Hierarchy.ClockExpr.eval_step_add line 257
  14. theorem OAI.SKFluctuations.Hierarchy.ClockExpr.eval_step_scale line 269
  15. theorem OAI.SKFluctuations.Hierarchy.ClockExpr.rootCov_eval_add line 276
  16. theorem OAI.SKFluctuations.Hierarchy.ClockExpr.rootCov_eval_scale line 287
  17. theorem OAI.SKFluctuations.Hierarchy.ClockExpr.eval_step_linear line 305
  18. theorem OAI.SKFluctuations.Hierarchy.ClockExpr.pressureCov_direction_linear line 320
  19. theorem OAI.SKFluctuations.Hierarchy.ClockExpr.covariance_direction_linear line 353
  20. theorem OAI.SKFluctuations.Hierarchy.ClockExpr.rootCov_direction_linear line 398
  21. def OAI.SKFluctuations.Hierarchy.ClockExpr.iterRootCov line 419
  22. theorem OAI.SKFluctuations.Hierarchy.ClockExpr.iteratedDeriv_rootEval line 424
  23. theorem OAI.SKFluctuations.Hierarchy.ClockExpr.iteratedDeriv_root_hasDerivAt line 443
  24. theorem OAI.SKFluctuations.Hierarchy.ClockExpr.rootEval_mean_zero line 464
  25. theorem OAI.SKFluctuations.Hierarchy.ClockExpr.rootEval_listSum line 474
  26. theorem OAI.SKFluctuations.Hierarchy.ClockTree.rootEval_weightExpr line 489
  27. theorem OAI.SKFluctuations.Hierarchy.ClockTree.rootEval_testExpr line 502
  28. theorem OAI.SKFluctuations.Hierarchy.ClockExpr.rootCov_rootEval_direction_linear line 524
  29. abbrev OAI.SKFluctuations.Hierarchy.ClockPolynomial line 538
  30. def OAI.SKFluctuations.Hierarchy.ClockPolynomial.rootEval line 544
  31. def OAI.SKFluctuations.Hierarchy.ClockPolynomial.insert line 549
  32. def OAI.SKFluctuations.Hierarchy.ClockPolynomial.coeffDeriv line 553
  33. def OAI.SKFluctuations.Hierarchy.ClockPolynomial.multiplyX line 556
  34. def OAI.SKFluctuations.Hierarchy.ClockPolynomial.affineInsert line 559
  35. theorem OAI.SKFluctuations.Hierarchy.ClockPolynomial.rootEval_append line 565
  36. theorem OAI.SKFluctuations.Hierarchy.ClockPolynomial.rootEval_multiplyX line 572
  37. theorem OAI.SKFluctuations.Hierarchy.ClockPolynomial.rootEval_affineInsert line 582
  38. theorem OAI.SKFluctuations.Hierarchy.ClockPolynomial.hasDerivAt_frozen line 596
  39. theorem OAI.SKFluctuations.Hierarchy.ClockPolynomial.hasDerivAt_diagonal line 610
  40. theorem OAI.SKFluctuations.Hierarchy.ClockExpr.rootEval_continuous line 642