OAI/Geometry/NodalSets/Elliptic/UniformSmoothBounds.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Yau.Jets.DerivativeBound line 11
  2. lemma OAI.Yau.Jets.DerivativeBound.mono line 14
  3. lemma OAI.Yau.Jets.DerivativeBound.add line 18
  4. lemma OAI.Yau.Jets.DerivativeBound.mul line 28
  5. lemma OAI.Yau.Jets.DerivativeBound.sum line 40
  6. lemma OAI.Yau.Jets.coordPartial_derivative_norm_le line 50
  7. lemma OAI.Yau.Jets.DerivativeBound.coordPartial line 72
  8. theorem OAI.Yau.Jets.compact_smooth_derivative_bound line 80