OAI/Probability/SKSupport/Moments/PerturbationLimits.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ZeroTemperatureSK.perturbationGradientErrors line 16
  2. def OAI.ZeroTemperatureSK.perturbationGradientError line 19
  3. lemma OAI.ZeroTemperatureSK.perturbationGradientErrors_bddAbove line 22
  4. lemma OAI.ZeroTemperatureSK.perturbationGradientError_nonneg line 30
  5. lemma OAI.ZeroTemperatureSK.perturbationGradientError_bound line 34
  6. lemma OAI.ZeroTemperatureSK.perturbationGradientError_limit line 38
  7. def OAI.ZeroTemperatureSK.perturbationPathError line 59
  8. lemma OAI.ZeroTemperatureSK.perturbationPathError_limit line 63
  9. lemma OAI.ZeroTemperatureSK.perturbationPathError_bound line 71
  10. lemma OAI.ZeroTemperatureSK.perturbationPath_limit line 78
  11. lemma OAI.ZeroTemperatureSK.mixedQ_perturbation_limit line 87
  12. lemma OAI.ZeroTemperatureSK.squareMoment_bounds line 125
  13. lemma OAI.ZeroTemperatureSK.squareMoment_continuousOn line 137
  14. lemma OAI.ZeroTemperatureSK.curvatureMoment_continuousOn_unit line 142
  15. lemma OAI.ZeroTemperatureSK.squareMoment_hasDerivAt line 154
  16. lemma OAI.ZeroTemperatureSK.squareMoment_weighted_integrable line 159