OAI/Analysis/LipschitzHilbert/Packets/PacketDataCrossForm.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The physical distinct-profile sum is exactly the finite coefficient form used in the packet representation. Both sides keep the original spatial sites and analyzing coefficients.

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