OAI/Analysis/LipschitzHilbert/Packets/SourcePackedPacketPairing.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.SourceLabeledLattice.packed_short_packet_pairing_sq line 16