OAI/Geometry/Riemannian/HarmonicCore/Fourier.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicCounterexample.Analytic.boundedDistribution line 16
2. lemma OAI.HarmonicCounterexample.Analytic.boundedDistribution_apply line 19
3. lemma OAI.HarmonicCounterexample.Analytic.integral_inverseFourier_mul line 26
4. lemma OAI.HarmonicCounterexample.Analytic.inverseFourier_boundedDistribution line 35
5. theorem OAI.HarmonicCounterexample.Analytic.sobolev_exists_continuous line 43
6. lemma OAI.HarmonicCounterexample.Analytic.besselPotential_two line 51
7. theorem OAI.HarmonicCounterexample.Analytic.laplacianL2_exists_continuous line 74
8. lemma OAI.HarmonicCounterexample.Analytic.boundedDistribution_eq_L2_ae line 85
9. lemma OAI.HarmonicCounterexample.Analytic.sobolevWeight_memLp line 113
10. theorem OAI.HarmonicCounterexample.Analytic.sobolev_continuous_bound line 133
11. theorem OAI.HarmonicCounterexample.Analytic.laplacianL2_continuous_estimate line 173