OAI/Probability/SKSupport/Moments/SquareEquation.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ZeroTemperatureSK.compactValueRate_eq line 15
  2. lemma OAI.ZeroTemperatureSK.compactGradient_hasDerivWithinAt_right line 19
  3. lemma OAI.ZeroTemperatureSK.deriv_compactValueRate line 30
  4. def OAI.ZeroTemperatureSK.compactSquare line 47
  5. def OAI.ZeroTemperatureSK.compactSquareRate line 50
  6. lemma OAI.ZeroTemperatureSK.compactSquare_family line 53
  7. lemma OAI.ZeroTemperatureSK.compactSquareRate_family line 57
  8. lemma OAI.ZeroTemperatureSK.compactSquareRate_right line 62
  9. lemma OAI.ZeroTemperatureSK.compactSquare_integral_rate line 70
  10. lemma OAI.ZeroTemperatureSK.compactSquare_generator line 86
  11. lemma OAI.ZeroTemperatureSK.compactGradient_derivative_continuous line 120
  12. lemma OAI.ZeroTemperatureSK.BoundedLipschitzDrift.expected_continuous line 134
  13. lemma OAI.ZeroTemperatureSK.stripDrift_pathDrift_right line 150
  14. lemma OAI.ZeroTemperatureSK.compactSquare_continuous line 166
  15. lemma OAI.ZeroTemperatureSK.compactCurvatureSquare_continuous line 171