OAI/Probability/SKSupport/Regularity/RightRegularity.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ZeroTemperatureSK.SpatialRightContinuous line 13
2. lemma OAI.ZeroTemperatureSK.SpatialRightContinuous.deriv line 16
3. lemma OAI.ZeroTemperatureSK.SpatialRightContinuous.add line 21
4. lemma OAI.ZeroTemperatureSK.SpatialRightContinuous.const_mul line 34
5. lemma OAI.ZeroTemperatureSK.SpatialRightContinuous.mul line 42
6. lemma OAI.ZeroTemperatureSK.SpatialRightContinuous.timeConst line 56
7. lemma OAI.ZeroTemperatureSK.compactCoeff_rightContinuous line 65
8. lemma OAI.ZeroTemperatureSK.compactGradient_rightSmooth line 83
9. lemma OAI.ZeroTemperatureSK.compactValueRate_rightSmooth line 101
10. theorem OAI.ZeroTemperatureSK.value_derivative_hasDerivWithinAt_right line 121