OAI/Geometry/Riemannian/HarmonicCore/InteriorDerivative.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.value_eq_of_test_pairings line 11
  2. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.scalarValue_inner line 32
  3. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.scalarValue_test line 40
  4. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.componentL2_scalar line 53
  5. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.sobolev_component_weak line 64
  6. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.sobolev_norm_le_gradient line 80
  7. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.weak_interior_derivative_sobolev line 89