OAI/Geometry/Riemannian/HarmonicCore/HigherDerivative.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.coefficientCLM_coe line 12
  2. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.coefficient_component_vectorize line 17
  3. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.matrix_component_support line 31
  4. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.coefficient_H1_component line 38
  5. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.weak_forced_cutoff_H2 line 70
  6. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.weak_direction_H2 line 110