OAI/Geometry/Riemannian/HarmonicCore/BoundaryContinuity.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.sobolevValue_supported line 17
  2. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.metricFlux_compact line 43
  3. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.laplacian_green_sobolev line 51
  4. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.smooth_energy_nonneg_of_superharmonic line 97
  5. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.gradient_sub_smooth line 114
  6. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.gradient_eqOn_closedBall line 121
  7. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.clipped_energy_representation line 133
  8. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.clipped_affine_energy_eq line 145
  9. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.affine_weak_le_superharmonic line 175
  10. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.classical_weak_le_superharmonic line 221
  11. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.barrier_boundary_domination line 244
  12. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.exists_boundary_majorant line 293
  13. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.gradient_neg_smooth line 331
  14. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.affine_weak_neg line 338
  15. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.classical_weak_boundary_continuity line 356
  16. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.metric_classical_dirichlet line 435