OAI/Probability/SKFluctuations/HasDerivAtDynamicVarianceContinuation.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Has Deriv At Dynamic Variance Continuation.

  1. theorem OAI.SKFluctuations.Hierarchy.hasDerivAt_dynamic_varianceContinuation line 21
  2. theorem OAI.SKFluctuations.Hierarchy.dynamic_varianceTest_joint_continuous line 110
  3. theorem OAI.SKFluctuations.Hierarchy.dynamic_varianceTest_absBounded line 125
  4. def OAI.SKFluctuations.Hierarchy.affineVariation line 145
  5. theorem OAI.SKFluctuations.Hierarchy.affineVariation_regular line 156
  6. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchy_affine_variation line 192
  7. def OAI.SKFluctuations.Hierarchy.featureKernel line 234
  8. def OAI.SKFluctuations.Hierarchy.pathKernelPenalty line 239
  9. theorem OAI.SKFluctuations.Hierarchy.pathKernelPenalty_smooth line 247
  10. theorem OAI.SKFluctuations.Hierarchy.kernelPenalty_add line 259
  11. theorem OAI.SKFluctuations.Hierarchy.affineVariation_kernel_telescope line 266
  12. def OAI.SKFluctuations.Hierarchy.PathKernelBound line 311
  13. def OAI.SKFluctuations.Hierarchy.pathKernelCost line 317
  14. theorem OAI.SKFluctuations.Hierarchy.pathKernelPenalty_lower line 321
  15. theorem OAI.SKFluctuations.Hierarchy.affineVariation_le_cost line 350
  16. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchy_affine_chord_pos line 370
  17. def OAI.SKFluctuations.Hierarchy.bumpSignedSteps line 404
  18. theorem OAI.SKFluctuations.Hierarchy.bumpSignedSteps_nil line 408
  19. theorem OAI.SKFluctuations.Hierarchy.bumpSignedSteps_cons line 410
  20. theorem OAI.SKFluctuations.Hierarchy.bumpSignedSteps_zero line 414
  21. theorem OAI.SKFluctuations.Hierarchy.bumpSignedSteps_neg line 418
  22. theorem OAI.SKFluctuations.Hierarchy.bumpSignedSteps_ordered line 423
  23. theorem OAI.SKFluctuations.Hierarchy.PathKernelBound.bump line 431
  24. theorem OAI.SKFluctuations.Hierarchy.pathKernelCost_bump line 443
  25. theorem OAI.SKFluctuations.Hierarchy.affineBump_continuous line 455
  26. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchy_affine_chord line 485
  27. theorem OAI.SKFluctuations.Hierarchy.PathKernelBound.congr_bounds line 543
  28. theorem OAI.SKFluctuations.Hierarchy.pathKernelCost_congr line 553
  29. theorem OAI.SKFluctuations.Hierarchy.pathKernelCost_continuous line 561
  30. def OAI.SKFluctuations.Hierarchy.affineInitialMass line 568
  31. theorem OAI.SKFluctuations.Hierarchy.affineInitialMass_pos line 573
  32. theorem OAI.SKFluctuations.Hierarchy.affineSteps_ordered_initial line 580
  33. theorem OAI.SKFluctuations.Hierarchy.rootedHierarchy_affine_chord line 595