OAI/Analysis/LipschitzHilbert/Packets/PacketDataParentReference.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The actual data at a selected reference uses only its local cone.

  1. abbrev OAI.LipschitzHilbert.PacketLatticeData.recenteredReferenceData line 24

    Source documentation

    Literal recentering of original physical reference data.

    abbrev recenteredReferenceData : PhysicalReferenceData N κ Label Item where
…

    Mentions: OAI.LipschitzHilbert.PhysicalReferenceData

  2. def OAI.LipschitzHilbert.PacketLatticeData.recenteredReferenceSelection line 36

    Source documentation

    Original packet indices are selected through the exact reference-label map.

    def recenteredReferenceSelection (S : Finset P.PacketIndex) :
    Finset (P.referenceFamily oldSlope newSlope R cone w F hw hcone hF hwide hfrequency).PacketIndex :=
…

    Mentions: OAI.LipschitzHilbert.PacketLatticeData.PacketIndex

  3. theorem OAI.LipschitzHilbert.PacketLatticeData.recenteredReferenceData_slope line 41
  4. theorem OAI.LipschitzHilbert.PacketLatticeData.recenteredReferenceData_angle line 45
  5. theorem OAI.LipschitzHilbert.PacketLatticeData.recenteredReferenceData_short line 49
  6. theorem OAI.LipschitzHilbert.PacketLatticeData.recenteredReferenceData_bad line 56