OAI/Analysis/LipschitzHilbert/Fourier/LineConjugationDerivative.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual strong L2 conjugation derivative.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.lineSampling_conjugation_tangent line 16
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.lineConjugation_L2_hasDerivAt line 38