OAI/Geometry/Riemannian/HarmonicCore/Regularization.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HarmonicCounterexample.Analytic.E3 line 16
2. lemma OAI.HarmonicCounterexample.Analytic.weak_continuous_convolution_derivative line 18
3. def OAI.HarmonicCounterexample.Analytic.regularizingBump line 63
4. lemma OAI.HarmonicCounterexample.Analytic.regularizingBump_tendsto line 69
5. theorem OAI.HarmonicCounterexample.Analytic.continuous_weak_hasFDerivAt line 74