OAI/Geometry/Riemannian/HarmonicCore/SphericalMean.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HarmonicCounterexample.Main.UnitSphere3 line 18
2. def OAI.HarmonicCounterexample.Main.angularMeasure line 22
3. instance OAI.HarmonicCounterexample.Main.angularMeasure_probability line 27
4. def OAI.HarmonicCounterexample.Main.sphericalMean line 40
5. def OAI.HarmonicCounterexample.Main.sphericalMeanDerivative line 45
6. lemma OAI.HarmonicCounterexample.Main.sphericalMean_continuous line 50
7. lemma OAI.HarmonicCounterexample.Main.sphericalMeanDerivative_continuous line 60
8. lemma OAI.HarmonicCounterexample.Main.sphericalMean_hasDerivAt line 72
9. lemma OAI.HarmonicCounterexample.Main.sphericalMean_zero line 106
10. lemma OAI.HarmonicCounterexample.Main.regular_origin_flux_zero line 111
11. theorem OAI.HarmonicCounterexample.Main.integral_polar_three line 121