OAI/Geometry/NodalSets/Elliptic/RealL2DifferenceQuotient.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Yau.RealEuclideanL2 line 10
  2. def OAI.Yau.realL2Translate line 12
  3. theorem OAI.Yau.realL2Translate_ae line 15
  4. theorem OAI.Yau.realL2Translate_norm line 19
  5. def OAI.Yau.realDifferenceQuotient line 22
  6. def OAI.Yau.realL2DifferenceQuotient line 25
  7. theorem OAI.Yau.realL2DifferenceQuotient_ae line 28
  8. theorem OAI.Yau.realDifferenceQuotient_memLp line 41
  9. theorem OAI.Yau.realL2DifferenceQuotient_norm line 49
  10. theorem OAI.Yau.real_integral_translate_pairing line 58
  11. theorem OAI.Yau.real_differenceQuotient_pairing line 64