OAI/Analysis/LipschitzHilbert/Trees/SourceAssignedTopFamily.lean

GitHub source file

10 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.SourceLabeledLattice.AssignedTopItem line 17
  2. instance OAI.LipschitzHilbert.SourceLabeledLattice.assignedTopItemFintype line 22
  3. def OAI.LipschitzHilbert.SourceLabeledLattice.assignedTopFamily line 27
  4. theorem OAI.LipschitzHilbert.SourceLabeledLattice.assignedTopFamily_length line 55
  5. theorem OAI.LipschitzHilbert.SourceLabeledLattice.assignedTopFamily_constant line 59
  6. theorem OAI.LipschitzHilbert.SourceLabeledLattice.assignedTopFamily_label_count line 63
  7. def OAI.LipschitzHilbert.SourceLabeledLattice.assignedTopPacketEquiv line 69

    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.SourceLabeledLattice.PacketIndex

  8. theorem OAI.LipschitzHilbert.SourceLabeledLattice.assignedTopFamily_physicalPacket line 91
  9. theorem OAI.LipschitzHilbert.SourceLabeledLattice.assignedTopFamily_physicalMultiplierCoefficient line 99

    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.SourceLabeledLattice.physicalMultiplierCoefficient

  10. theorem OAI.LipschitzHilbert.SourceLabeledLattice.sum_assignedTopPackets line 109