OAI/Analysis/LipschitzHilbert/Packets/PacketDataReferenceEnvelope.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Actual Schwartz packets are dominated by the envelope used in the selected-tree cross-term estimate, in its common reference direction.

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