OAI/Geometry/SurfaceImmersion/Atlas/SupportedWeightedSeminorm.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The weighted derivative bounds as actual seminorms on smooth fields with fixed compact support, for finite derivative-loss parametrix iteration.

  1. abbrev OAI.ClosedSurfaceR4.JetPolynomial.SupportedField line 17
  2. def OAI.ClosedSurfaceR4.JetPolynomial.supportedWeightedSeminorm line 19
  3. lemma OAI.ClosedSurfaceR4.JetPolynomial.supportedWeightedSeminorm_component line 24
  4. lemma OAI.ClosedSurfaceR4.JetPolynomial.weightedBound_of_supportedSeminorm line 35
  5. lemma OAI.ClosedSurfaceR4.JetPolynomial.supportedSeminorm_le_of_weightedBound line 47
  6. theorem OAI.ClosedSurfaceR4.JetPolynomial.supportedSeminorm_le_iff line 62