OAI/Analysis/LipschitzHilbert/Estimates/PlanarProfileBounds.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Uniform profile constants for the first three raw waves. Scaling a covariant derivative costs only the square of its dimensionless width.

  1. theorem OAI.LipschitzHilbert.planarVerticalDerivative_smul line 13
  2. theorem OAI.LipschitzHilbert.planarHorizontalDerivative_smul line 18
  3. def OAI.LipschitzHilbert.planarVerticalJet line 23
  4. theorem OAI.LipschitzHilbert.planarProfileJet_eq line 27
  5. def OAI.LipschitzHilbert.planarProfileConstant line 36
  6. theorem OAI.LipschitzHilbert.planarProfileConstant_pos line 41
  7. theorem OAI.LipschitzHilbert.planar_profile_base_envelope line 48
  8. theorem OAI.LipschitzHilbert.planar_profile_horizontal_base_envelope line 66
  9. theorem OAI.LipschitzHilbert.planar_profile_vertical_base_envelope line 84
  10. theorem OAI.LipschitzHilbert.planar_profile_envelope line 102
  11. theorem OAI.LipschitzHilbert.planar_profile_horizontal_envelope line 113
  12. theorem OAI.LipschitzHilbert.planar_profile_vertical_envelope line 125