OAI/Geometry/Riemannian/HarmonicCore/SmoothBootstrap.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.weak_forced_cutoff_all_orders line 16
  2. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.CompactSobolev.classical line 107
  3. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.CompactSobolev.smooth line 138
  4. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.metric_weak_smooth line 149
  5. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.metric_affine_weak_smooth line 180