OAI/Geometry/Riemannian/HarmonicCore/TransferOperator.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicCounterexample.Main.sphereInClosedBall line 19
2. def OAI.HarmonicCounterexample.Main.SmoothMetric3.radiusDirichlet line 28
3. def OAI.HarmonicCounterexample.Main.SmoothMetric3.radiusDirichletL2 line 32
4. lemma OAI.HarmonicCounterexample.Main.polar_radiusDirichletL2_norm_le line 37
5. def OAI.HarmonicCounterexample.Main.wholeBallL2 line 55
6. lemma OAI.HarmonicCounterexample.Main.wholeBallL2_on_smooth line 63
7. theorem OAI.HarmonicCounterexample.Main.wholeBallL2_norm_le line 73
8. def OAI.HarmonicCounterexample.Main.angularOneL2 line 85
9. lemma OAI.HarmonicCounterexample.Main.angularOneL2_inner line 88
10. lemma OAI.HarmonicCounterexample.Main.continuous_toL2_mean line 96
11. theorem OAI.HarmonicCounterexample.Main.wholeBallL2_mean line 101
12. theorem OAI.HarmonicCounterexample.Main.wholeBallL2_one line 118
13. theorem OAI.HarmonicCounterexample.Main.wholeBallL2_restriction line 144