OAI/Probability/SKFluctuations/HasDerivWithinAtVectorHeatContinuation.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Has Deriv Within At Vector Heat Continuation.

  1. theorem OAI.SKFluctuations.GaussianCalculus.hasDerivWithinAt_vector_heat_continuation line 22
  2. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchyMean_sum line 98
  3. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchyMean_const_mul_ordered line 123
  4. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchyMean_feature_components line 143
  5. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchy_hasDerivWithinAt_clock line 169
  6. theorem OAI.SKFluctuations.Hierarchy.hasDerivAt_continuation_local line 203
  7. structure OAI.SKFluctuations.Hierarchy.ParametricRegular line 277
  8. theorem OAI.SKFluctuations.Hierarchy.ParametricRegular.step line 285
  9. def OAI.SKFluctuations.Hierarchy.prefixContinuation line 315
  10. def OAI.SKFluctuations.Hierarchy.prefixTest line 320
  11. theorem OAI.SKFluctuations.Hierarchy.ParametricRegular.prefix line 325
  12. theorem OAI.SKFluctuations.Hierarchy.prefixContinuation_hierarchy line 338
  13. theorem OAI.SKFluctuations.Hierarchy.isotropicGaussian_preserving line 357
  14. theorem OAI.SKFluctuations.Hierarchy.integral_isotropicGaussian line 372
  15. def OAI.SKFluctuations.Hierarchy.clockContinuation line 380
  16. def OAI.SKFluctuations.Hierarchy.clockTest line 383
  17. theorem OAI.SKFluctuations.Hierarchy.clockContinuation_eq line 386
  18. theorem OAI.SKFluctuations.Hierarchy.clockTest_eq line 395
  19. def OAI.SKFluctuations.Hierarchy.clockDerivative line 407
  20. theorem OAI.SKFluctuations.Hierarchy.parametric_clock line 420
  21. theorem OAI.SKFluctuations.Hierarchy.ParametricRegular.root line 491
  22. theorem OAI.SKFluctuations.Hierarchy.rootedHierarchy_inserted_clock line 540
  23. theorem OAI.SKFluctuations.GaussianCalculus.ExpNormBounded.lipschitz line 577
  24. theorem OAI.SKFluctuations.GaussianCalculus.ExpNormBounded.bddSmooth line 592
  25. def OAI.SKFluctuations.Hierarchy.clockRoot line 604
  26. theorem OAI.SKFluctuations.Hierarchy.clockRoot_eq line 607
  27. theorem OAI.SKFluctuations.Hierarchy.hasDerivWithinAt_clockRoot line 616