OAI/Geometry/Riemannian/HarmonicCore/ClassicalHarmonic.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.metric_energy_gradient_flux line 17
  2. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.metric_weak_classical_harmonic line 28
  3. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.metric_affine_classical_interior line 72
  4. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.laplacian_congr_nhds line 100
  5. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.glue_classical_inner_balls line 105
  6. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.metric_affine_classical_open_ball line 160