OAI/Geometry/Riemannian/HarmonicCore/GradientContinuity.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HarmonicCounterexample.Main.SmoothMetric3.testSobolev line 14
  2. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.affineSobolev_value line 17
  3. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.affineSobolev_derivative line 23
  4. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.compact_test_extension line 29
  5. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.metric_affine_weak_continuous line 35
  6. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.graph_H2_continuous line 64
  7. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.weak_interior_gradient_continuous line 79
  8. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.identity_perturbation_derivatives line 133
  9. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.smooth_energy_extension_higher line 152
  10. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.metric_weak_gradient_continuous line 181