OAI/Analysis/LipschitzHilbert/Packets/PlanarPacketDifferentiation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Exact vertical derivatives of packet syntheses. Coefficients stay fixed during differentiation, including when they are analyzing integrals.

  1. def OAI.LipschitzHilbert.planarPacketBand line 16
  2. theorem OAI.LipschitzHilbert.planarPacketBand_hasDerivAt line 21
  3. theorem OAI.LipschitzHilbert.planarPacketBand_covariant line 31
  4. def OAI.LipschitzHilbert.planarPacketInterval line 47
  5. theorem OAI.LipschitzHilbert.planarPacketInterval_smul line 52
  6. theorem OAI.LipschitzHilbert.planarPacketInterval_covariant line 75
  7. theorem OAI.LipschitzHilbert.planarPacketInterval_eq_partial_difference line 91
  8. theorem OAI.LipschitzHilbert.planarPacketInterval_norm_le line 105
  9. theorem OAI.LipschitzHilbert.planarPacketInterval_covariant_norm_le line 115
  10. theorem OAI.LipschitzHilbert.planarPacketInterval_scaled_covariant_norm_le line 128