OAI/Analysis/LipschitzHilbert/Packets/PacketDataKernelForm.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Exact passage from a physical coefficient form to the finite sum of convolution packet products, retaining the inverse-area factor.

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