OAI/Analysis/LipschitzHilbert/Packets/PacketDataAssignedTubeEnvelope.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The original assigned packet envelope on the entire phase tube. Its growth in the imaginary norm is linear, with the exact polynomial factor needed by the Gaussian vertex extension.

  1. theorem OAI.LipschitzHilbert.PacketLatticeData.eventually_assigned_original_tube_envelope line 16