OAI/Analysis/LipschitzHilbert/Phase/ActualBandDiagonal.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Exact identification of the physical localized operator pairing with the finite diagonal form used by the high-disparity estimate.

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