OAI/Analysis/LipschitzHilbert/Estimates/SharpTimeSplit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exact splitting of sharp time truncations; the two boundary points are removed only by a null-set argument.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.sharpTimeKernel_split_ae line 12
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.kernelPairing_sharp_split line 36