OAI/Analysis/LipschitzHilbert/Phase/PacketAngularModel.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Build the three actual ordinary models from one angular assignment. The assignment is common to all carrier components. It only partitions the original packet indices; every physical wave and site is preserved.

  1. def OAI.LipschitzHilbert.PacketLatticeData.angularPackets line 16
  2. def OAI.LipschitzHilbert.PacketLatticeData.angularSelector line 20
  3. def OAI.LipschitzHilbert.PacketLatticeData.angularModelConfig line 25