OAI/Analysis/LipschitzHilbert/Fourier/BandProjectedHigh.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The improved high-diagonal estimate for the actual vertically projected input vectors. All projection size and energy hypotheses are discharged.

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