OAI/Analysis/LipschitzHilbert/Estimates/HilbertTimeDecomposition.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Assembly of the actual short, middle and long time pieces. The middle term is the finite annular operator already estimated by the packet argument; all other terms have explicit restricted bounds.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.kernelPairing_projection_normalize line 16
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.hilbertProjected_middle_error line 27
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.hilbertProjected_short_error line 63
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.hilbertTimeDecomposition_bound line 80