OAI/Analysis/LipschitzHilbert/Phase/DiagonalAmplitudeReconstruction.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exact reconstruction of the actual finite diagonal form from its measurable amplitude slices.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.amplitudeApprox_coordinate line 18
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.amplitudePiece_coordinate_integrable line 26
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.finiteDiagonalBand_amplitude_reconstruction line 33