OAI/Analysis/LipschitzHilbert/Phase/PacketAngularBasicPairing.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The basic pairing estimate for a whole packet collection, after constructing and recombining its three ordinary angular models. No model configuration is assumed. All constants precede the finite packet data.

  1. theorem OAI.LipschitzHilbert.PacketLatticeData.exists_angular_basic_pairing line 15