OAI/Geometry/Riemannian/HarmonicCore/FiniteDifference.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.zeroSobolevSpace_mono line 12
  2. def OAI.HarmonicCounterexample.Main.SmoothMetric3.includeSobolev line 20
  3. def OAI.HarmonicCounterexample.Main.SmoothMetric3.finiteDifferenceL2 line 23
  4. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.finiteDifferenceL2_apply line 27
  5. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.finiteDifferenceL2_coe line 31
  6. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.finiteDifferenceL2_inner line 39
  7. def OAI.HarmonicCounterexample.Main.SmoothMetric3.finiteDifferencePair line 46
  8. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.finiteDifferencePair_mem line 49
  9. def OAI.HarmonicCounterexample.Main.SmoothMetric3.finiteDifferenceSobolev line 56
  10. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.finiteDifferenceSobolev_value line 59
  11. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.finiteDifferenceSobolev_derivative line 62
  12. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.sobolev_finiteDifference_bound line 65
  13. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.weak_caccioppoli_forcing line 75