OAI/Geometry/Riemannian/HarmonicCore/CoefficientDifference.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HarmonicCounterexample.Main.SmoothMetric3.shiftedCoefficient line 11
  2. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.shiftedCoefficient_continuous line 14
  3. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.shiftedCoefficient_bound line 17
  4. def OAI.HarmonicCounterexample.Main.SmoothMetric3.shiftedCoefficientCLM line 20
  5. def OAI.HarmonicCounterexample.Main.SmoothMetric3.differenceCoefficient line 25
  6. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.differenceCoefficient_continuous line 28
  7. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.differenceCoefficient_bound line 35
  8. def OAI.HarmonicCounterexample.Main.SmoothMetric3.differenceCoefficientCLM line 51
  9. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.differenceCoefficientCLM_norm line 57
  10. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.finiteDifference_coefficient_product line 64
  11. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.weak_finiteDifference_equation line 92
  12. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.scalarFieldCLM_norm line 111
  13. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.gradientFieldCLM_norm line 121
  14. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.weak_gradient_finiteDifference_bound line 133