OAI/Probability/SKFluctuations/VarianceTestZeroRoot.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Variance Test Zero Root.

  1. theorem OAI.SKFluctuations.Hierarchy.varianceTest_zero_root line 21
  2. theorem OAI.SKFluctuations.Hierarchy.dynamic_zeroContinuation_continuous line 28
  3. theorem OAI.SKFluctuations.Hierarchy.hasDerivAt_dynamic_zeroContinuation line 40
  4. theorem OAI.SKFluctuations.Hierarchy.rootedHierarchy_affine_variation line 122
  5. theorem OAI.SKFluctuations.Hierarchy.rootedHierarchy_corrected_affine_variation line 156
  6. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchyMean_reindex_steps line 233
  7. theorem OAI.SKFluctuations.Hierarchy.hierarchyPairMean_reindex_steps line 247
  8. theorem OAI.SKFluctuations.Hierarchy.pathKernelPenalty_reindex line 255
  9. theorem OAI.SKFluctuations.Hierarchy.rootedHierarchy_corrected_affine_variation_finite line 286
  10. def OAI.SKFluctuations.Hierarchy.affineCumulative line 357
  11. theorem OAI.SKFluctuations.Hierarchy.signedClockSteps_at line 361
  12. theorem OAI.SKFluctuations.Hierarchy.disorderPressure_hasDerivAt line 376
  13. theorem OAI.SKFluctuations.Hierarchy.levelPairMean_linear line 424
  14. theorem OAI.SKFluctuations.Hierarchy.rootLevelPairMean_linear line 444
  15. theorem OAI.SKFluctuations.Hierarchy.massStepSum_linear line 461
  16. theorem OAI.SKFluctuations.Hierarchy.massStepSum_const line 468
  17. theorem OAI.SKFluctuations.Hierarchy.massStepSum_mono line 474
  18. theorem OAI.SKFluctuations.Hierarchy.massStepSum_nonneg line 483
  19. def OAI.SKFluctuations.orderedPrefixPair line 497
  20. def OAI.SKFluctuations.orderedPrefixS line 503
  21. def OAI.SKFluctuations.orderedPrefixB line 506
  22. theorem OAI.SKFluctuations.affine_orderedClock line 509
  23. theorem OAI.SKFluctuations.orderedSKPressure_hasDerivAt line 517
  24. theorem OAI.SKFluctuations.orderedPrefix_bounds line 590
  25. def OAI.SKFluctuations.orderedCompensatedSquare line 609
  26. theorem OAI.SKFluctuations.orderedCompensatedSquare_nonneg line 614
  27. theorem OAI.SKFluctuations.orderedCompensatedSquare_le line 618
  28. def OAI.SKFluctuations.finiteCompensatedSweep line 628
  29. theorem OAI.SKFluctuations.massStepSum_compensated line 633
  30. theorem OAI.SKFluctuations.finiteCompensatedSweep_hasDerivAt line 643
  31. theorem OAI.SKFluctuations.compensatedRate_bounds line 679