OAI/Probability/SKFluctuations/TreeRootVariation.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

Tree Root Variation.

  1. def OAI.SKFluctuations.Hierarchy.covarianceDifference line 21
  2. theorem OAI.SKFluctuations.Hierarchy.cumulativeIncrements_affine line 24
  3. def OAI.SKFluctuations.Hierarchy.ClockTree.cumulativeFamily line 31
  4. def OAI.SKFluctuations.Hierarchy.ClockTree.cumulativeVariation line 38
  5. theorem OAI.SKFluctuations.Hierarchy.ClockTree.cumulativeFamily_actual line 49
  6. theorem OAI.SKFluctuations.Hierarchy.ClockTree.hasDerivAt_disorderWeight_fullPath line 60
  7. def OAI.SKFluctuations.Hierarchy.finiteJetEquiv line 99
  8. def OAI.SKFluctuations.Hierarchy.ClockTree.finiteDisorderRate line 106
  9. theorem OAI.SKFluctuations.Hierarchy.ClockTree.hasDerivAt_finiteDisorderWeight line 117
  10. theorem OAI.SKFluctuations.Hierarchy.ClockTree.hasDerivAt_finiteDisorderExpect line 140
  11. inductive OAI.SKFluctuations.Hierarchy.ClockExpr line 161
  12. def OAI.SKFluctuations.Hierarchy.ClockExpr.sub line 170
  13. def OAI.SKFluctuations.Hierarchy.ClockExpr.mean line 173
  14. def OAI.SKFluctuations.Hierarchy.ClockExpr.listSum line 177
  15. def OAI.SKFluctuations.Hierarchy.ClockExpr.eval line 183
  16. theorem OAI.SKFluctuations.Hierarchy.ClockExpr.eval_sub line 193
  17. theorem OAI.SKFluctuations.Hierarchy.ClockExpr.eval_mean line 198
  18. theorem OAI.SKFluctuations.Hierarchy.MassOrdered.lower line 210
  19. theorem OAI.SKFluctuations.Hierarchy.ClockExpr.eval_smooth line 218
  20. theorem OAI.SKFluctuations.Hierarchy.ClockExpr.eval_mean_zero line 232
  21. theorem OAI.SKFluctuations.Hierarchy.ClockExpr.eval_listSum line 239
  22. def OAI.SKFluctuations.Hierarchy.ClockTree.weightExpr line 249
  23. def OAI.SKFluctuations.Hierarchy.ClockTree.testExpr line 255
  24. theorem OAI.SKFluctuations.Hierarchy.ClockTree.eval_weightExpr line 261
  25. theorem OAI.SKFluctuations.Hierarchy.ClockTree.eval_testExpr line 278
  26. def OAI.SKFluctuations.Hierarchy.ClockExpr.source line 300
  27. theorem OAI.SKFluctuations.Hierarchy.ClockExpr.hasDerivAt_source line 311
  28. def OAI.SKFluctuations.Hierarchy.HeatJet.addTest line 349
  29. def OAI.SKFluctuations.Hierarchy.HeatJet.scaleTest line 363
  30. def OAI.SKFluctuations.Hierarchy.HeatJetFamily.addTest line 380
  31. def OAI.SKFluctuations.Hierarchy.HeatJetFamily.scaleTest line 390
  32. def OAI.SKFluctuations.Hierarchy.JetVariation.addTest line 400
  33. def OAI.SKFluctuations.Hierarchy.JetVariation.scaleTest line 411
  34. def OAI.SKFluctuations.Hierarchy.spinTestJet line 431
  35. theorem OAI.SKFluctuations.Hierarchy.spinTestJet_F line 439
  36. theorem OAI.SKFluctuations.Hierarchy.spinTestJet_A line 446
  37. def OAI.SKFluctuations.Hierarchy.ClockExpr.family line 452
  38. theorem OAI.SKFluctuations.Hierarchy.ClockExpr.family_actual line 463
  39. def OAI.SKFluctuations.Hierarchy.ClockExpr.variation line 503
  40. def OAI.SKFluctuations.Hierarchy.ClockExpr.grad line 527
  41. theorem OAI.SKFluctuations.Hierarchy.ClockExpr.jet_G line 530
  42. theorem OAI.SKFluctuations.Hierarchy.ClockExpr.jet_H line 542
  43. theorem OAI.SKFluctuations.Hierarchy.ClockExpr.jet_A₁ line 553
  44. theorem OAI.SKFluctuations.Hierarchy.ClockExpr.jet_A₂ line 564
  45. def OAI.SKFluctuations.Hierarchy.ClockExpr.coordSum line 585
  46. theorem OAI.SKFluctuations.Hierarchy.ClockExpr.eval_coordSum line 588
  47. def OAI.SKFluctuations.Hierarchy.ClockExpr.potentialInsert line 596
  48. def OAI.SKFluctuations.Hierarchy.ClockExpr.testedInsert line 601
  49. def OAI.SKFluctuations.Hierarchy.ClockExpr.pressureCov line 609
  50. def OAI.SKFluctuations.Hierarchy.ClockExpr.covariance line 620
  51. theorem OAI.SKFluctuations.Hierarchy.ClockExpr.eval_potentialInsert line 634
  52. theorem OAI.SKFluctuations.Hierarchy.ClockExpr.eval_testedInsert line 644