OAI/Analysis/LipschitzHilbert/Packets/PacketDataAssignedReference.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Each assigned top receives its exact local bounded reference family.

  1. def OAI.LipschitzHilbert.PacketLatticeData.assignedReferenceFamily line 20

    Source documentation

    The selected reference family has derived shear and carrier bounds.

    def assignedReferenceFamily (top : τ) :
    SourceLabeledLattice N κ (fun j => τ×P.labels j) (P.AssignedTopItem packets assigned) :=
…

    Mentions: OAI.LipschitzHilbert.SourceLabeledLattice

  2. def OAI.LipschitzHilbert.PacketLatticeData.assignedReferenceOriginalLabel line 28
  3. def OAI.LipschitzHilbert.PacketLatticeData.assignedReferenceAlternate line 38
  4. theorem OAI.LipschitzHilbert.PacketLatticeData.assignedReferenceAlternate_bound line 46
  5. def OAI.LipschitzHilbert.PacketLatticeData.assignedReferenceSelector line 57