OAI/Analysis/LipschitzHilbert/Packets/PlanarPacketDerivative.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Horizontal derivatives of general modulated packets. Uniform bounds use precisely the dimensionless carrier and slope restrictions.

  1. def OAI.LipschitzHilbert.planarHorizontalDerivative line 11
  2. theorem OAI.LipschitzHilbert.planarHorizontalDerivative_apply line 14
  3. theorem OAI.LipschitzHilbert.modulatedPlanarSlice_horizontal_hasDerivAt line 17
  4. theorem OAI.LipschitzHilbert.modulatedPlanarSlice_derivative_bound line 43