OAI/Probability/SKSupport/Foundations/BoundedSmooth.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.ZeroTemperatureSK.Heat.BoundedSmooth line 18
2. lemma OAI.ZeroTemperatureSK.Heat.BoundedSmooth.bound line 22
3. lemma OAI.ZeroTemperatureSK.Heat.BoundedSmooth.deriv line 25
4. lemma OAI.ZeroTemperatureSK.Heat.BoundedSmooth.const line 31
5. lemma OAI.ZeroTemperatureSK.Heat.BoundedSmooth.add line 38
6. lemma OAI.ZeroTemperatureSK.Heat.BoundedSmooth.mul line 50
7. lemma OAI.ZeroTemperatureSK.Heat.BoundedSmooth.const_mul line 70
8. structure OAI.ZeroTemperatureSK.Heat.RegularDatum line 73
9. lemma OAI.ZeroTemperatureSK.Heat.weighted_derivative_boundedSmooth line 77
10. lemma OAI.ZeroTemperatureSK.Heat.weighted_derivative_formula line 82
11. lemma OAI.ZeroTemperatureSK.Heat.contDiff_nat_semigroup_weight_exp line 93
12. lemma OAI.ZeroTemperatureSK.Heat.contDiff_semigroup_weight_exp line 119