OAI/Geometry/Riemannian/HarmonicCore/CutoffBounds.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.continuous_compact_bound line 11
2. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.weak_cutoff_H2 line 21
3. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.sobolev_gradient_norm_le line 58
4. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.cutoff_gradient_bound line 61
5. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.component_gradientField line 71
6. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.weak_cutoff_H2_bound line 83