OAI/Probability/SKSupport/Regularity/GaussianFlowRegularity.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ZeroTemperatureSK.Heat.BoundedSmoothFamily.continuousOn_iteratedDeriv line 12
2. lemma OAI.ZeroTemperatureSK.Heat.varianceGradient_family line 25
3. lemma OAI.ZeroTemperatureSK.Heat.varianceGradient_continuousOn line 38
4. def OAI.ZeroTemperatureSK.Heat.gaussianRate line 47
5. lemma OAI.ZeroTemperatureSK.Heat.gaussianRate_family line 51
6. lemma OAI.ZeroTemperatureSK.Heat.gaussianRate_continuousOn line 59
7. lemma OAI.ZeroTemperatureSK.Heat.varianceLogHeat_integral_rate line 69
8. lemma OAI.ZeroTemperatureSK.Heat.gaussianRate_integral_derivative line 82
9. lemma OAI.ZeroTemperatureSK.Heat.hasDerivAt_varianceLogHeat_derivative line 98