OAI/Geometry/Riemannian/HarmonicCore/BoundaryTrace.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HarmonicCounterexample.Main.SmoothMetric3.compactTrace line 19
  2. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.compactTrace_unit line 27
  3. def OAI.HarmonicCounterexample.Main.SmoothMetric3.smoothTraceAlgebra line 34
  4. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.smoothTrace_separates line 54
  5. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.compactTrace_dense line 73
  6. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.compactTrace_L2_dense line 83
  7. theorem OAI.HarmonicCounterexample.Main.smooth_source_boundary_dense line 93
  8. def OAI.HarmonicCounterexample.Main.SmoothMetric3.radiusTrace line 102
  9. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.radiusTrace_dense line 110
  10. def OAI.HarmonicCounterexample.Main.SmoothMetric3.radiusTraceL2 line 123
  11. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.radiusTraceL2_dense line 128
  12. lemma OAI.HarmonicCounterexample.Main.continuous_toL2_norm_sq line 136
  13. lemma OAI.HarmonicCounterexample.Main.radiusTraceL2_norm_sq line 145