OAI/Analysis/LipschitzHilbert/Estimates/ActualBinReconstruction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The exact bin diagonalization of the actual localized time operator. The error is the same projected commutator sum whose energy is estimated.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.actualBin_reconstruction line 14