OAI/Analysis/LipschitzHilbert/Packets/PacketDataAssignedTopFamily.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Assigned top restrictions with common label and item types. The top is part of the label, so each top family contains exactly its own packets and the family-valued concentration and path estimates apply literally.

  1. def OAI.LipschitzHilbert.PacketLatticeData.AssignedTopItem line 18
  2. instance OAI.LipschitzHilbert.PacketLatticeData.assignedTopItemFintype line 23
  3. def OAI.LipschitzHilbert.PacketLatticeData.assignedTopFamily line 28
  4. theorem OAI.LipschitzHilbert.PacketLatticeData.assignedTopFamily_length line 52
  5. theorem OAI.LipschitzHilbert.PacketLatticeData.assignedTopFamily_label_count line 56
  6. def OAI.LipschitzHilbert.PacketLatticeData.assignedTopPacketEquiv line 62

    Source documentation

    No packet is copied to a second top, and no empty fiber adds a packet.

    def assignedTopPacketEquiv (packets : Finset P.PacketIndex) (assigned : P.PacketIndex → τ)
    (top : τ) : (P.assignedTopFamily packets assigned top).PacketIndex ≃
      packets.filter (fun q => assigned q = top) where
…

    Mentions: OAI.LipschitzHilbert.PacketLatticeData.PacketIndex

  7. theorem OAI.LipschitzHilbert.PacketLatticeData.assignedTopFamily_physicalPacket line 84
  8. theorem OAI.LipschitzHilbert.PacketLatticeData.assignedTopFamily_physicalMultiplierCoefficient line 92

    Source documentation

    Repartitioning retains the original analyzing integral exactly.

    theorem assignedTopFamily_physicalMultiplierCoefficient (packets : Finset P.PacketIndex)
    (assigned : P.PacketIndex → τ) (top : τ) (t : ℝ)
    (b : ∀ j, P.labels j → κ → ℝ → ℂ) (v : ℝ×ℝ → ℝ)
    (f : ℝ×ℝ → EuclideanSpace ℂ κ) (j : Fin N)
    (l : (P.assignedTopFamily packets assigned top).labels j)
    (u : P.AssignedTopItem packets assigned j l) :
    (P.assignedTopFamily packets assigned top).physicalMultiplierCoefficient t
      (fun j l => b j l.val.2) v f j l u =
      P.physicalMultiplierCoefficient t b v f j l.val.2 u.val := rfl

    Mentions: OAI.LipschitzHilbert.PacketLatticeData.physicalMultiplierCoefficient

  9. theorem OAI.LipschitzHilbert.PacketLatticeData.sum_assignedTopPackets line 102