OAI/Analysis/LipschitzHilbert/Phase/PacketAngularReversePairing.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Construct and recombine the three angular models for the reverse estimate. The fixed cost is independent of all finite packet data.

  1. theorem OAI.LipschitzHilbert.PacketLatticeData.exists_angular_reverse_pairing line 14