OAI/Probability/SKFluctuations/VarianceJet.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

Variance Jet.

  1. theorem OAI.SKFluctuations.Hierarchy.varianceTest_bddSmooth line 22
  2. def OAI.SKFluctuations.Hierarchy.varianceGradient line 29
  3. theorem OAI.SKFluctuations.Hierarchy.hasDerivAt_varianceTest_source line 33
  4. theorem OAI.SKFluctuations.Hierarchy.varianceGradient_bddSmooth line 49
  5. def OAI.SKFluctuations.Hierarchy.varianceSecond line 57
  6. theorem OAI.SKFluctuations.Hierarchy.hasDerivAt_varianceGradient_source line 63
  7. theorem OAI.SKFluctuations.Hierarchy.varianceSecond_bddSmooth line 80
  8. theorem OAI.SKFluctuations.Hierarchy.hasDerivAt_varianceContinuation_source line 91
  9. theorem OAI.SKFluctuations.Hierarchy.varianceTest_const_mul line 105
  10. theorem OAI.SKFluctuations.Hierarchy.varianceTest_sum line 108
  11. theorem OAI.SKFluctuations.Hierarchy.varianceGradient_sum line 115
  12. theorem OAI.SKFluctuations.Hierarchy.hasDerivAt_varianceTest_source_vector line 135
  13. theorem OAI.SKFluctuations.Hierarchy.hasDerivAt_varianceContinuation_source_vector line 155
  14. def OAI.SKFluctuations.Hierarchy.HeatJet.varianceEvolve line 165
  15. theorem OAI.SKFluctuations.Hierarchy.dynamic_varianceGradient_joint_continuous line 197
  16. theorem OAI.SKFluctuations.Hierarchy.dynamic_varianceGradient_absBounded line 215
  17. theorem OAI.SKFluctuations.Hierarchy.dynamic_varianceSecond_joint_continuous line 231
  18. theorem OAI.SKFluctuations.Hierarchy.dynamic_varianceSecond_absBounded line 259
  19. def OAI.SKFluctuations.Hierarchy.HeatJetFamily.varianceEvolve line 287
  20. theorem OAI.SKFluctuations.Hierarchy.HeatJetFamily.continuous_signedVarianceRate line 333
  21. theorem OAI.SKFluctuations.Hierarchy.HeatJetFamily.bounded_signedVarianceRate line 345
  22. theorem OAI.SKFluctuations.Hierarchy.HeatJetFamily.continuous_signedVarianceDerivative line 357
  23. theorem OAI.SKFluctuations.Hierarchy.HeatJetFamily.bounded_signedVarianceDerivative line 368
  24. def OAI.SKFluctuations.Hierarchy.AffineVarianceRegular line 390
  25. theorem OAI.SKFluctuations.Hierarchy.AffineVarianceRegular.nonneg line 394
  26. theorem OAI.SKFluctuations.Hierarchy.AffineVarianceRegular.eventually line 400
  27. theorem OAI.SKFluctuations.Hierarchy.AffineVarianceRegular.sqrt_coefficient line 411
  28. theorem OAI.SKFluctuations.Hierarchy.AffineVarianceRegular.amplitude_regular line 418
  29. theorem OAI.SKFluctuations.Hierarchy.affineVarianceRegular_of_nonneg line 455
  30. def OAI.SKFluctuations.Cavity.actualScalarClock line 485
  31. theorem OAI.SKFluctuations.Cavity.actualScalarClock_nonneg line 490
  32. theorem OAI.SKFluctuations.Cavity.actualScalarClock_monotone line 497
  33. theorem OAI.SKFluctuations.Cavity.actualScalarClock_le line 505
  34. def OAI.SKFluctuations.Hierarchy.ClockTree.cavityLeft line 524
  35. def OAI.SKFluctuations.Hierarchy.ClockTree.cavityRight line 530
  36. def OAI.SKFluctuations.Hierarchy.ClockTree.cavityAssignment line 536
  37. theorem OAI.SKFluctuations.Hierarchy.leftSteps_clockSteps line 544
  38. theorem OAI.SKFluctuations.Hierarchy.rightSteps_clockSteps line 551
  39. theorem OAI.SKFluctuations.Hierarchy.ClockTree.weight_cavity_product line 561
  40. theorem OAI.SKFluctuations.Hierarchy.ClockTree.disorderWeight_cavity_product line 588
  41. theorem OAI.SKFluctuations.Hierarchy.ClockTree.disorderExpect_cavity_product line 625