OAI/Analysis/LipschitzHilbert/Phase/ScalarBandDiagonal.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The scalar basic and reverse-disparity diagonal bounds, without projecting the test or imposing a spectrum on amplitude slices.

  1. def OAI.LipschitzHilbert.PacketRepresentation.scalarVector line 13
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.scalarVector_apply line 16
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.scalarVector_norm line 21
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.scalarVector_measurable line 24
  5. def OAI.LipschitzHilbert.PacketRepresentation.scalarBandForm line 33
  6. theorem OAI.LipschitzHilbert.PacketRepresentation.scalarBandForm_eq line 38
  7. theorem OAI.LipschitzHilbert.PacketRepresentation.scalar_band_basic line 45
  8. theorem OAI.LipschitzHilbert.PacketRepresentation.scalar_band_reverse line 72