OAI/Probability/SKSupport/Regularity/FamilyDifferentiation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ZeroTemperatureSK.Heat.BoundedSmoothFamily.add line 13
2. lemma OAI.ZeroTemperatureSK.Heat.BoundedSmoothFamily.const_mul line 26
3. lemma OAI.ZeroTemperatureSK.Heat.BoundedSmoothFamily.intervalIntegrable line 30
4. lemma OAI.ZeroTemperatureSK.Heat.BoundedSmoothFamily.hasDerivAt_integral line 38
5. lemma OAI.ZeroTemperatureSK.Heat.BoundedSmoothFamily.iteratedDeriv_integral line 55
6. lemma OAI.ZeroTemperatureSK.Heat.tendstoUniformlyOn_deriv_family line 77
7. lemma OAI.ZeroTemperatureSK.Heat.continuousOn_deriv_family line 120