OAI/Geometry/NodalSets/Elliptic/SmoothDefectBounds.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Yau.Jets.UniformSmoothBounded line 11
  2. lemma OAI.Yau.Jets.uniformSmoothBounded_of_continuous_derivatives line 15
  3. lemma OAI.Yau.Jets.ContinuousPolyFamily.derivative_continuous line 21
  4. lemma OAI.Yau.Jets.ContinuousPolyFamily.uniformSmoothBounded line 37
  5. lemma OAI.Yau.Jets.UniformSmoothBounded.const line 45
  6. lemma OAI.Yau.Jets.UniformSmoothBounded.add line 53
  7. lemma OAI.Yau.Jets.UniformSmoothBounded.mul line 63
  8. lemma OAI.Yau.Jets.UniformSmoothBounded.sum line 73
  9. lemma OAI.Yau.Jets.UniformSmoothBounded.coordPartial line 83
  10. lemma OAI.Yau.Jets.uniformSmoothBounded_secondOrder line 91
  11. lemma OAI.Yau.Jets.uniformSmoothBounded_eikonal line 103
  12. lemma OAI.Yau.Jets.uniformSmoothBounded_beamVector line 113
  13. lemma OAI.Yau.Jets.uniformSmoothBounded_beamScalar line 121
  14. lemma OAI.Yau.Jets.uniformSmoothBounded_transport_defect line 130