OAI/Analysis/LipschitzHilbert/Packets/PacketDataPackedPairing.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The packed short packets can be paired with a weighted long-tree maximum. This is the analytic estimate for the distant-scale Gram sum.

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