OAI/Analysis/LipschitzHilbert/Fourier/FiniteBandDerivative.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Vertical differentiation commutes with the actual finite band sums. The covariant derivative uses the same carrier in every band of a fixed coordinate, so no carrier-frequency factor is lost.

  1. def OAI.LipschitzHilbert.scalarBandPartial line 15
  2. theorem OAI.LipschitzHilbert.scalarBandPartial_hasDerivAt line 18
  3. theorem OAI.LipschitzHilbert.scalarBandPartial_covariant line 28
  4. def OAI.LipschitzHilbert.bandIntervalSignal line 39
  5. theorem OAI.LipschitzHilbert.bandIntervalSignal_covariant line 44
  6. theorem OAI.LipschitzHilbert.bandIntervalSignal_norm_le line 68