OAI/Geometry/Riemannian/HarmonicCore/Multipliers.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.field_memLp line 16
  2. def OAI.HarmonicCounterexample.Main.SmoothMetric3.fieldLinear line 25
  3. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.fieldLinear_norm line 44
  4. def OAI.HarmonicCounterexample.Main.SmoothMetric3.fieldCLM line 54
  5. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.fieldCLM_coe line 59
  6. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.gradient_mul_smooth line 66
  7. def OAI.HarmonicCounterexample.Main.SmoothMetric3.scalarFieldCLM line 72
  8. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.scalarFieldCLM_coe line 81
  9. def OAI.HarmonicCounterexample.Main.SmoothMetric3.gradientFieldCLM line 87
  10. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.gradientFieldCLM_coe line 98
  11. def OAI.HarmonicCounterexample.Main.SmoothMetric3.localizePair line 103
  12. def OAI.HarmonicCounterexample.Main.SmoothMetric3.DirichletTest.localize line 111
  13. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.localizePair_test line 116
  14. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.localizePair_preserves line 151
  15. def OAI.HarmonicCounterexample.Main.SmoothMetric3.localizeSobolev line 163
  16. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.localizeSobolev_value line 168
  17. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.localizeSobolev_derivative line 174
  18. def OAI.HarmonicCounterexample.Main.SmoothMetric3.DirichletTest.cutoff line 181
  19. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.localizePair_cutoff line 187
  20. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.localizePair_mem_smaller line 196
  21. def OAI.HarmonicCounterexample.Main.SmoothMetric3.cutoffSobolev line 209
  22. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.scalarField_inner line 215
  23. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.scalarField_coefficient_commute line 224
  24. lemma OAI.HarmonicCounterexample.Main.SmoothMetric3.gradientField_scalar_commute line 241