OAI/Probability/SKSupport/Moments/ThirdFields.lean
13 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.ZeroTemperatureSK.thirdCurvatureFieldline 15 - lemma
OAI.ZeroTemperatureSK.thirdCurvatureField_eqline 22 - lemma
OAI.ZeroTemperatureSK.secondCurvatureField_generator_eqline 30 - lemma
OAI.ZeroTemperatureSK.hasDerivAt_of_right_on_Iooline 47 - def
OAI.ZeroTemperatureSK.stripSecondline 73 - def
OAI.ZeroTemperatureSK.stripThirdline 76 - lemma
OAI.ZeroTemperatureSK.stripSecond_continuousline 79 - lemma
OAI.ZeroTemperatureSK.stripThird_continuousline 82 - lemma
OAI.ZeroTemperatureSK.curvatureField_expectedline 85 - lemma
OAI.ZeroTemperatureSK.stripA_hasDerivWithinAt_rightline 94 - lemma
OAI.ZeroTemperatureSK.stripSecond_hasDerivWithinAt_rightline 107 - lemma
OAI.ZeroTemperatureSK.stripA_hasDerivAt_on_constantline 120 - lemma
OAI.ZeroTemperatureSK.stripSecond_hasDerivAt_on_constantline 131