OAI/Probability/SKSupport/Foundations/DerivVarianceHeatCurve.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ZeroTemperatureSK.Heat.hasDerivAt_varianceHeat_curve line 18
2. lemma OAI.ZeroTemperatureSK.Heat.hasDerivAt_varianceLogHeat_curve line 44
3. def OAI.ZeroTemperatureSK.Heat.kernelConstant line 103
4. lemma OAI.ZeroTemperatureSK.Heat.kernelConstant_nonneg line 105
5. lemma OAI.ZeroTemperatureSK.Heat.integrable_standardGaussian_abs line 107
6. lemma OAI.ZeroTemperatureSK.Heat.scaled_gradient_stein line 110
7. lemma OAI.ZeroTemperatureSK.Heat.scaled_gradient_bound line 129
8. lemma OAI.ZeroTemperatureSK.Heat.semigroup_gradient_bound line 152