OAI/Analysis/LipschitzHilbert/Fourier/DemodulatedVertical.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Remove the vertical carrier before applying the interval Sobolev estimate. The derivative norm is exactly the covariant derivative norm, independently of the carrier frequencies and Hilbert dimension.

  1. theorem OAI.LipschitzHilbert.character_hasDerivAt line 19
  2. def OAI.LipschitzHilbert.demodulatedSignal line 29
  3. def OAI.LipschitzHilbert.covariantSignal line 33
  4. theorem OAI.LipschitzHilbert.demodulatedSignal_norm line 37
  5. theorem OAI.LipschitzHilbert.demodulatedSignal_hasDerivAt line 42
  6. theorem OAI.LipschitzHilbert.demodulatedSignal_deriv_norm line 58
  7. theorem OAI.LipschitzHilbert.demodulated_deriv_memLp line 64
  8. theorem OAI.LipschitzHilbert.covariant_interval_energy line 73