OAI/Probability/SKFluctuations/PotentialHeatTrace.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

Potential Heat Trace.

  1. def OAI.SKFluctuations.Hierarchy.potentialHeatTrace line 20
  2. def OAI.SKFluctuations.Hierarchy.testedHeatTrace line 23
  3. theorem OAI.SKFluctuations.Hierarchy.hasDerivWithinAt_clockTest line 29
  4. theorem OAI.SKFluctuations.GaussianCalculus.ExpNormBounded.continuous_integral_affine line 134
  5. theorem OAI.SKFluctuations.Hierarchy.sqrt_coe_toNNReal line 172
  6. theorem OAI.SKFluctuations.Hierarchy.clockTest_eq_all line 178
  7. theorem OAI.SKFluctuations.Hierarchy.clockTest_continuous line 190
  8. def OAI.SKFluctuations.Hierarchy.clockGradient line 213
  9. theorem OAI.SKFluctuations.Hierarchy.hasDerivAt_clockTest_source line 217
  10. theorem OAI.SKFluctuations.Hierarchy.clockGradient_continuous line 233
  11. theorem OAI.SKFluctuations.Hierarchy.clockGradient_bddSmooth line 240
  12. def OAI.SKFluctuations.Hierarchy.clockSecond line 250
  13. theorem OAI.SKFluctuations.Hierarchy.hasDerivAt_clockGradient_source line 256
  14. theorem OAI.SKFluctuations.Hierarchy.clockSecond_continuous line 273
  15. theorem OAI.SKFluctuations.Hierarchy.clockSecond_bddSmooth line 282
  16. theorem OAI.SKFluctuations.Hierarchy.clockContinuation_eq_all line 300
  17. theorem OAI.SKFluctuations.Hierarchy.clockContinuation_continuous line 309
  18. theorem OAI.SKFluctuations.Hierarchy.hasDerivAt_clockContinuation_source line 320
  19. theorem OAI.SKFluctuations.Hierarchy.linearGaussian_id line 334
  20. theorem OAI.SKFluctuations.Hierarchy.clockContinuation_add line 338
  21. theorem OAI.SKFluctuations.Hierarchy.clockTest_add line 347
  22. theorem OAI.SKFluctuations.Hierarchy.isotropicGaussian_zero line 356
  23. theorem OAI.SKFluctuations.Hierarchy.clockTest_zero line 360
  24. theorem OAI.SKFluctuations.Hierarchy.clockContinuation_zero line 365
  25. theorem OAI.SKFluctuations.Hierarchy.clockTest_add_test line 371
  26. theorem OAI.SKFluctuations.Hierarchy.clockTest_const_mul line 376
  27. theorem OAI.SKFluctuations.Hierarchy.clockTest_sum line 379
  28. theorem OAI.SKFluctuations.Hierarchy.clockGradient_sum line 391
  29. theorem OAI.SKFluctuations.Hierarchy.clockSecond_add_drift line 413
  30. theorem OAI.SKFluctuations.GaussianCalculus.hasDerivAt_bivariate_chain line 444
  31. def OAI.SKFluctuations.Hierarchy.clockTestDerivative line 470
  32. theorem OAI.SKFluctuations.Hierarchy.potentialHeatTrace_bddSmooth line 477
  33. theorem OAI.SKFluctuations.Hierarchy.testedHeatTrace_bddSmooth line 485
  34. theorem OAI.SKFluctuations.Hierarchy.clockTestDerivative_continuous line 496
  35. theorem OAI.SKFluctuations.Hierarchy.hasDerivAt_clockTest_joint line 508
  36. theorem OAI.SKFluctuations.Hierarchy.clockTestDerivative_eq_generator line 557
  37. theorem OAI.SKFluctuations.Hierarchy.hasDerivAt_clockTest_source_vector line 576
  38. def OAI.SKFluctuations.Hierarchy.AbsBounded line 603
  39. theorem OAI.SKFluctuations.Hierarchy.AbsBounded.add line 605
  40. theorem OAI.SKFluctuations.Hierarchy.AbsBounded.neg line 609
  41. theorem OAI.SKFluctuations.Hierarchy.AbsBounded.sub line 611
  42. theorem OAI.SKFluctuations.Hierarchy.AbsBounded.mul line 613
  43. theorem OAI.SKFluctuations.Hierarchy.AbsBounded.const_mul line 618
  44. theorem OAI.SKFluctuations.Hierarchy.AbsBounded.sum line 621
  45. theorem OAI.SKFluctuations.Hierarchy.clockTest_absBounded line 627
  46. theorem OAI.SKFluctuations.Hierarchy.clockGradient_absBounded line 636
  47. theorem OAI.SKFluctuations.Hierarchy.clockSecond_absBounded line 643
  48. theorem OAI.SKFluctuations.Hierarchy.clockTestDerivative_absBounded line 652