OAI/Analysis/LipschitzHilbert/Fourier/LineSamplingInverseDerivative.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Differentiation in time of the actual inverse sampling map.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.lineSampling_deriv_ne_zero line 11
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.lineSamplingInverse_space_hasDerivAt line 21
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.lineSamplingInverse_time_continuousAt line 32
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.lineSamplingInverse_time_hasDerivAt line 44