OAI/Analysis/LipschitzHilbert/Packets/PacketDataAssignedLinearEnvelope.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.PacketLatticeData.assigned_original_linear_envelope line 15