OAI/Analysis/HenonEmden/SphereMean.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HenonLaneEmden.SphereCalculus.slice_continuous line 26
2. lemma OAI.HenonLaneEmden.SphereCalculus.hasDerivAt_integral_compact line 32
3. abbrev OAI.HenonLaneEmden.SphereCalculus.UnitSphere line 67
4. def OAI.HenonLaneEmden.SphereCalculus.mean line 69
5. def OAI.HenonLaneEmden.SphereCalculus.meanD line 71
6. def OAI.HenonLaneEmden.SphereCalculus.meanDD line 73
7. lemma OAI.HenonLaneEmden.SphereCalculus.sphere_ne_zero line 79
8. lemma OAI.HenonLaneEmden.SphereCalculus.smul_sphere_ne_zero line 84
9. lemma OAI.HenonLaneEmden.SphereCalculus.continuous_mean_integrand line 88
10. lemma OAI.HenonLaneEmden.SphereCalculus.continuous_meanD_integrand line 96
11. lemma OAI.HenonLaneEmden.SphereCalculus.continuous_meanDD_integrand line 106
12. lemma OAI.HenonLaneEmden.SphereCalculus.continuousOn_mean line 117
13. lemma OAI.HenonLaneEmden.SphereCalculus.continuousOn_meanD line 123
14. lemma OAI.HenonLaneEmden.SphereCalculus.continuousOn_meanDD line 129
15. lemma OAI.HenonLaneEmden.SphereCalculus.continuous_mean line 135
16. lemma OAI.HenonLaneEmden.SphereCalculus.mean_zero line 142
17. lemma OAI.HenonLaneEmden.SphereCalculus.hasDerivAt_mean line 146
18. lemma OAI.HenonLaneEmden.SphereCalculus.hasDerivAt_meanD line 157
19. lemma OAI.HenonLaneEmden.SphereCalculus.mean_pos line 172