OAI/Analysis/LipschitzHilbert/Packets/BoxPacketVariation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Short-scale Hilbert packet variation from the explicit coefficient budget and packet envelopes, retaining the horizontal and transverse decay of one center box.

  1. theorem OAI.LipschitzHilbert.box_packet_variation line 16