OAI/Analysis/LipschitzHilbert/Trees/SourceAssignedLinearEnvelope.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The arbitrary-phase linear envelope for the original assigned packet amplitudes. Recentring, masks and original analyzing coefficients are retained exactly.

  1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.assigned_original_linear_envelope line 15