OAI/Probability/SKFluctuations/CavityClockZero.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Cavity Clock Zero.

  1. theorem OAI.SKFluctuations.Hierarchy.clockSteps_zeroRow line 22
  2. theorem OAI.SKFluctuations.Hierarchy.ClockTree.weight_zeroRow line 30
  3. theorem OAI.SKFluctuations.Hierarchy.cumulativeIncrements_zeroRow line 51
  4. theorem OAI.SKFluctuations.Hierarchy.ClockTree.disorderWeight_zeroRow line 59
  5. theorem OAI.SKFluctuations.Hierarchy.ClockTree.disorderExpect_zeroRow line 79
  6. def OAI.SKFluctuations.Hierarchy.HeatJet.productTest line 97
  7. def OAI.SKFluctuations.Hierarchy.HeatJetFamily.productTest line 117
  8. def OAI.SKFluctuations.Hierarchy.HeatJet.constantFamily line 133
  9. def OAI.SKFluctuations.Hierarchy.spinWeightJet line 151
  10. theorem OAI.SKFluctuations.Hierarchy.spinWeightJet_F line 158
  11. theorem OAI.SKFluctuations.Hierarchy.spinWeightJet_A line 165
  12. def OAI.SKFluctuations.Hierarchy.ClockTree.weightFamily line 171
  13. theorem OAI.SKFluctuations.Hierarchy.ClockTree.weightFamily_actual line 182
  14. structure OAI.SKFluctuations.Hierarchy.JetVariation line 219
  15. def OAI.SKFluctuations.Hierarchy.HeatJet.constantVariation line 231
  16. def OAI.SKFluctuations.Hierarchy.JetVariation.productTest line 241
  17. def OAI.SKFluctuations.Hierarchy.JetVariation.pressureRate line 252
  18. def OAI.SKFluctuations.Hierarchy.JetVariation.testRate line 257
  19. theorem OAI.SKFluctuations.Hierarchy.JetVariation.continuous_pressureRate line 263
  20. theorem OAI.SKFluctuations.Hierarchy.JetVariation.bounded_pressureRate line 270
  21. theorem OAI.SKFluctuations.Hierarchy.JetVariation.continuous_testRate line 276
  22. theorem OAI.SKFluctuations.Hierarchy.JetVariation.bounded_testRate line 289
  23. def OAI.SKFluctuations.Hierarchy.JetVariation.varianceEvolve line 301
  24. theorem OAI.SKFluctuations.Hierarchy.hasDerivAt_face_variance_test line 330
  25. theorem OAI.SKFluctuations.Hierarchy.hasDerivAt_face_varianceContinuation line 353
  26. theorem OAI.SKFluctuations.Hierarchy.hasDerivAt_face_dynamic_varianceContinuation line 384
  27. theorem OAI.SKFluctuations.Hierarchy.hasDerivAt_face_dynamic_varianceTest line 454
  28. def OAI.SKFluctuations.Hierarchy.JetVariation.faceVarianceEvolve line 544
  29. def OAI.SKFluctuations.Hierarchy.ClockTree.faceWeightVariation line 575
  30. theorem OAI.SKFluctuations.Hierarchy.ClockTree.hasDerivAt_weight_fullNonnegativePath line 589
  31. theorem OAI.SKFluctuations.Hierarchy.ClockTree.hasDerivAt_expect_fullNonnegativePath line 603