OAI/Analysis/LipschitzHilbert/Packets/SourceSupportedLinearEnvelope.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The supported-scale node estimate with its explicit linear phase factor. No restriction is placed on the size of the imaginary phases; this is the bound used for the Gaussian tail in §11.

  1. theorem OAI.LipschitzHilbert.AngularGrid.source_supported_selector_linear_envelope line 14