OAI/Geometry/Riemannian/HarmonicCore/WeakDerivative.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.smooth_memLp line 10
  2. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.smooth_gradient_memLp line 14
  3. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.smooth_direction_memLp line 18
  4. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.smooth_smul_memLp line 23
  5. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.test_integration_by_parts line 29
  6. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.sobolev_integration_by_parts line 64
  7. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.sobolev_weak_derivative line 78
  8. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.sobolevDerivative_eq_zero_of_value_eq_zero line 94
  9. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.sobolevValue_injective line 117
  10. def OAI.HarmonicCounterexample.Main.SmoothMetric3.exteriorOperator line 127
  11. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.exteriorOperator_measurable line 131
  12. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.exteriorOperator_bound line 137
  13. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.sobolevDerivative_supported line 143
  14. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.clippedEnergy_integral_eq line 183
  15. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.metric_affine_weak_dirichlet line 194