OAI/Analysis/LipschitzHilbert/Packets/PacketDataAssignedTopBands.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Assigned top bands retain the actual top mask and physical packet.

  1. theorem OAI.LipschitzHilbert.PacketLatticeData.assignedTopFamily_physicalMaskedValue line 18
  2. theorem OAI.LipschitzHilbert.PacketLatticeData.assignedTopFamily_physicalMaskedBand line 30
  3. theorem OAI.LipschitzHilbert.PacketLatticeData.assignedTopFamily_single_mask line 82

    Source documentation

    The mask on an assigned family is its single assigned top mask.

    theorem assignedTopFamily_single_mask (top : τ) (T : τ → SlopeBox) :
    (fun j (l : (P.assignedTopFamily packets assigned top).labels j)
      (u : P.AssignedTopItem packets assigned j l) =>
        T (assigned ⟨j,⟨l.val.2,u.val⟩⟩)) = fun _ _ _ => T top := by
…

    Mentions: OAI.LipschitzHilbert.SlopeBox

  4. theorem OAI.LipschitzHilbert.PacketLatticeData.assignedTopFamily_topMaskBand line 90