OAI/Analysis/LipschitzHilbert/Packets/PacketDataReferenceProperties.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The physical selector centers are invariant under recentering. Restricting to the reference cone can only decrease their local count.

  1. theorem OAI.LipschitzHilbert.PacketLatticeData.referenceFamily_physical_center line 20
  2. theorem OAI.LipschitzHilbert.PacketLatticeData.referenceFamily_localMultiplicity line 25
  3. theorem OAI.LipschitzHilbert.PacketLatticeData.referenceFamily_selector_support line 46
  4. theorem OAI.LipschitzHilbert.PacketLatticeData.referenceFamily_physicalMultiplierCoefficient line 57
  5. theorem OAI.LipschitzHilbert.PacketLatticeData.referenceFamily_alternate_physicalPacket line 65
  6. theorem OAI.LipschitzHilbert.PacketLatticeData.referenceFamily_spectrum line 74
  7. theorem OAI.LipschitzHilbert.PacketLatticeData.sum_referenceFamily_selected line 96

    Source documentation

    A selected set supported in the reference cone has the identical sum after the literal label restriction, including empty item fibers.

    theorem sum_referenceFamily_selected {E : Type*} [AddCommMonoid E]
    (S : Finset P.PacketIndex) (f : P.PacketIndex → E)
    (hS : ∀ u ∈ S, P.referenceCondition oldSlope newSlope R cone w u.1 u.2.1) :
    (∑ u ∈ (Finset.univ : Finset (Q).PacketIndex).filter
      (fun u => (⟨u.1,⟨orig u.1 u.2.1,u.2.2⟩⟩ : P.PacketIndex) ∈ S),
      f ⟨u.1,⟨orig u.1 u.2.1,u.2.2⟩⟩) = ∑ u ∈ S, f u := by
…

    Mentions: OAI.LipschitzHilbert.PacketLatticeData.PacketIndex