OAI/Analysis/LipschitzHilbert/Packets/PacketDataTrimInteractions.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Removing noninteracting short packets is an exact equality for the actual vector-valued far Gram sum.

  1. theorem OAI.LipschitzHilbert.PacketLatticeData.far_pairing_restrict_to_interacting line 17