OAI/Geometry/Riemannian/HarmonicCore/ForcedDerivative.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HarmonicCounterexample.Main.SmoothMetric3.vectorizeL2 line 12
  2. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.vectorizeL2_coe line 15
  3. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.vectorizeL2_norm line 19
  4. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.vectorizeL2_translate line 24
  5. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.vectorizeL2_finiteDifference line 32
  6. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.vectorize_component_sum line 36
  7. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.forcing_finiteDifference_bound line 51
  8. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.weak_finiteDifference_forced line 68
  9. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.localized_differenceLimit line 91
  10. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.weak_forced_gradient_finiteDifference_bound line 131
  11. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.weak_forced_interior_derivative line 166