OAI/Geometry/TamingCompatibility/Currents/BoundedDistribution.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.EuclideanSobolev.boundedDistribution line 13
2. lemma OAI.TamingCompatibility.EuclideanSobolev.boundedDistribution_apply line 16
3. lemma OAI.TamingCompatibility.EuclideanSobolev.integral_fourierInv_smul line 23
4. lemma OAI.TamingCompatibility.EuclideanSobolev.inverseFourier_boundedDistribution line 35
5. theorem OAI.TamingCompatibility.EuclideanSobolev.exists_boundedContinuous_representative line 42
6. theorem OAI.TamingCompatibility.EuclideanSobolev.H3_representative line 49
7. def OAI.TamingCompatibility.EuclideanSobolev.fourierMeasure line 55
8. lemma OAI.TamingCompatibility.EuclideanSobolev.fourierMeasure_apply line 61
9. lemma OAI.TamingCompatibility.EuclideanSobolev.fourier_measure_distribution line 72
10. lemma OAI.TamingCompatibility.EuclideanSobolev.memLp_besselWeight line 87
11. theorem OAI.TamingCompatibility.EuclideanSobolev.finite_measure_memSobolev line 107
12. theorem OAI.TamingCompatibility.EuclideanSobolev.finite_measure_memHneg3 line 117