OAI/Probability/SKFluctuations/LineDerivativesSignEquivVolume.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

Line Derivatives Sign Equiv Volume.

  1. def OAI.SKFluctuations.Hierarchy.BddSmooth.lineDerivatives line 21
  2. theorem OAI.SKFluctuations.Hierarchy.variance_le_BddSmooth_block line 28
  3. structure OAI.SKFluctuations.Hierarchy.PinFrame line 55
  4. def OAI.SKFluctuations.Hierarchy.PinFrame.potential line 69
  5. def OAI.SKFluctuations.Hierarchy.PinFrame.observable line 70
  6. def OAI.SKFluctuations.Hierarchy.PinFrame.energy line 72
  7. def OAI.SKFluctuations.Hierarchy.PinFrame.gradient line 75
  8. def OAI.SKFluctuations.Hierarchy.PinFrame.hessian line 77
  9. def OAI.SKFluctuations.Hierarchy.PinFrame.cross line 79
  10. theorem OAI.SKFluctuations.Hierarchy.PinFrame.potential_lipschitz line 84
  11. def OAI.SKFluctuations.Hierarchy.PinFrame.derivatives line 89
  12. theorem OAI.SKFluctuations.Hierarchy.PinFrame.hessian_nonneg line 101
  13. theorem OAI.SKFluctuations.Hierarchy.PinFrame.observable_smooth line 104
  14. theorem OAI.SKFluctuations.Hierarchy.PinFrame.energy_smooth line 107
  15. theorem OAI.SKFluctuations.Hierarchy.PinFrame.cross_eq_lineDeriv line 110
  16. theorem OAI.SKFluctuations.Hierarchy.PinFrame.block_nonneg line 117
  17. theorem OAI.SKFluctuations.Hierarchy.pi_norm_sq_le_sum_sq line 133
  18. def OAI.SKFluctuations.Hierarchy.driverQuadratic line 143
  19. def OAI.SKFluctuations.Hierarchy.driverQuadratic_derivatives line 145
  20. theorem OAI.SKFluctuations.Hierarchy.gaussianDominated_quadratic_lipschitz line 168
  21. theorem OAI.SKFluctuations.Hierarchy.positive_integral_exp_neg line 188
  22. def OAI.SKFluctuations.Hierarchy.normalizedPotential line 195
  23. def OAI.SKFluctuations.Hierarchy.potentialLaw line 198
  24. theorem OAI.SKFluctuations.Hierarchy.exp_neg_normalizedPotential line 201
  25. theorem OAI.SKFluctuations.Hierarchy.gaussianDominated_normalizedPotential line 208
  26. theorem OAI.SKFluctuations.Hierarchy.potentialLaw_isProbability line 224
  27. def OAI.SKFluctuations.Hierarchy.pinnedPotential line 244
  28. def OAI.SKFluctuations.Hierarchy.pinnedObservable line 248
  29. def OAI.SKFluctuations.Hierarchy.pinnedEnergy line 251
  30. def OAI.SKFluctuations.Hierarchy.pinnedPotential_derivatives line 255
  31. theorem OAI.SKFluctuations.Hierarchy.pinnedPotential_gaussianDominated line 276
  32. theorem OAI.SKFluctuations.Hierarchy.pinnedObservable_smooth line 305
  33. theorem OAI.SKFluctuations.Hierarchy.pinnedEnergy_smooth line 309
  34. theorem OAI.SKFluctuations.Hierarchy.pinnedObservable_lineDeriv line 313
  35. theorem OAI.SKFluctuations.Hierarchy.pinnedPotential_strong line 324
  36. theorem OAI.SKFluctuations.Hierarchy.pinnedPotential_block line 330
  37. theorem OAI.SKFluctuations.Hierarchy.pinned_variance_le line 359
  38. def OAI.SKFluctuations.Hierarchy.zeroContinuation line 389
  39. theorem OAI.SKFluctuations.Hierarchy.ExponentialIncrement.integrable_norm line 393
  40. theorem OAI.SKFluctuations.Hierarchy.ExponentialIncrement.integrable_lipschitz line 401
  41. theorem OAI.SKFluctuations.Hierarchy.shiftedMean_zero line 415
  42. theorem OAI.SKFluctuations.Hierarchy.zeroContinuation_lipschitz line 420
  43. theorem OAI.SKFluctuations.Hierarchy.hasDerivAt_zeroContinuation line 433
  44. theorem OAI.SKFluctuations.Hierarchy.BddSmooth.zeroContinuation line 453
  45. theorem OAI.SKFluctuations.Hierarchy.PotentialRegularity.zeroContinuation line 466
  46. theorem OAI.SKFluctuations.Hierarchy.BddSmooth.integrable_zero_shift line 478
  47. def OAI.SKFluctuations.Hierarchy.SourceContinuation.root line 487
  48. theorem OAI.SKFluctuations.Hierarchy.shiftedContinuation_equiv line 541
  49. theorem OAI.SKFluctuations.Hierarchy.shiftedMean_equiv line 555
  50. theorem OAI.SKFluctuations.Hierarchy.spinPartition_equiv line 570
  51. theorem OAI.SKFluctuations.Hierarchy.spinWeight_equiv line 579
  52. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchy_equiv line 587
  53. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchyMean_equiv line 604
  54. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchyHessian_equiv line 628
  55. def OAI.SKFluctuations.Hierarchy.signEquiv line 659
  56. theorem OAI.SKFluctuations.Hierarchy.signEquiv_apply line 670
  57. theorem OAI.SKFluctuations.Hierarchy.signEquiv_gaussian line 673
  58. theorem OAI.SKFluctuations.Hierarchy.signEquiv_volume line 688