OAI/Probability/SKSupport/Foundations/VarianceHeatGradientBound.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ZeroTemperatureSK.Heat.varianceHeat_gradient_bound line 23
2. lemma OAI.ZeroTemperatureSK.Heat.deriv_varianceHeat_of_bounded line 29
3. lemma OAI.ZeroTemperatureSK.Heat.deriv_of_mild line 36
4. lemma OAI.ZeroTemperatureSK.Heat.uniform_gradient_bound_of_mild line 56
5. lemma OAI.ZeroTemperatureSK.Heat.iteratedDeriv_mild line 142
6. lemma OAI.ZeroTemperatureSK.Heat.burgers_source_derivative_bound line 160
7. lemma OAI.ZeroTemperatureSK.Heat.iteratedDeriv_finiteBurgersSource_bound line 191