OAI/Analysis/LipschitzHilbert/Fourier/LineSamplingStrongDerivative.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Strong L2 derivatives of the actual sampling paths.

  1. def OAI.LipschitzHilbert.PacketRepresentation.lineSchwartzDerivativeBound line 12
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.lineSchwartzDerivativeBound_nonneg line 15
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.lineSchwartz_lipschitz line 18
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.line_small_eventually line 25
  5. theorem OAI.LipschitzHilbert.PacketRepresentation.lineSamplingPath_L2_hasDerivAt line 33
  6. theorem OAI.LipschitzHilbert.PacketRepresentation.lineSamplingInversePath_L2_hasDerivAt line 60