OAI/Geometry/Riemannian/HarmonicCore/ClassicalDerivative.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.sobolev_continuous_hasFDerivAt line 17
2. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.cutoffSobolev_continuous_representatives line 39
3. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.sobolev_local_continuous_hasFDerivAt line 69
4. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.metric_weak_classical_first line 87
5. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.metric_weak_C1 line 116
6. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.metric_affine_weak_C1 line 130