OAI/Geometry/Riemannian/HarmonicCore/DirichletOperator.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HarmonicCounterexample.Main.SmoothMetric3.compactSmoothData line 17
  2. abbrev OAI.HarmonicCounterexample.Main.SmoothMetric3.CompactSmoothData line 23
  3. def OAI.HarmonicCounterexample.Main.SmoothMetric3.classicalExtension line 25
  4. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.classicalExtension_spec line 29
  5. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.classicalExtension_C2 line 36
  6. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.classicalExtension_congr_boundary line 41
  7. def OAI.HarmonicCounterexample.Main.SmoothMetric3.ballDirichlet line 52
  8. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.ballDirichlet_boundary line 85
  9. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.ballDirichlet_positive line 90
  10. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.ballDirichlet_constant line 101
  11. def OAI.HarmonicCounterexample.Main.SmoothMetric3.boundaryUnit line 113
  12. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.boundaryUnit_eq line 117
  13. def OAI.HarmonicCounterexample.Main.SmoothMetric3.squareData line 122
  14. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.ballDirichlet_square line 129
  15. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.ballDirichlet_abs_le line 148
  16. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.compact_smooth_restriction line 173
  17. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.exact_dirichlet_restriction line 196
  18. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.metric_classical_dirichlet_smooth line 217