OAI/Geometry/Riemannian/HarmonicCore/Distributions.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HarmonicCounterexample.Main.SmoothMetric3.complexifyL2 line 14
  2. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.complexifyL2_coe line 17
  3. def OAI.HarmonicCounterexample.Main.SmoothMetric3.realDistribution line 21
  4. def OAI.HarmonicCounterexample.Main.SmoothMetric3.DirichletTest.schwartz line 24
  5. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.complexify_test line 28
  6. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.realDistribution_test line 37
  7. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.complexify_test_derivative line 42
  8. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.realDistribution_test_derivative line 60
  9. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.sobolev_distribution_derivative line 68
  10. theorem OAI.HarmonicCounterexample.Main.SmoothMetric3.graph_laplacian line 85