OAI/Analysis/LipschitzHilbert/Phase/BandDiagonalHighL1.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The improved diagonal estimate with all auxiliary geometry removed. A fixed multiple of the band width specifies the retained low endpoint.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.band_diagonal_high_l1 line 13