OAI/Analysis/LipschitzHilbert/Packets/PacketLatticeRestriction.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Exact label restriction and finite tag partitions for the unrestricted packet family. Neither operation changes a packet or a lattice site.

  1. def OAI.LipschitzHilbert.PacketLatticeData.restrictedLabels line 16
  2. def OAI.LipschitzHilbert.PacketLatticeData.restrictedOriginalLabel line 19
  3. theorem OAI.LipschitzHilbert.PacketLatticeData.restrictedLabel_kept line 23
  4. def OAI.LipschitzHilbert.PacketLatticeData.restrictedLabelEquiv line 28
  5. def OAI.LipschitzHilbert.PacketLatticeData.restrictLabels line 35
  6. theorem OAI.LipschitzHilbert.PacketLatticeData.restrictLabels_physicalPacket line 46
  7. theorem OAI.LipschitzHilbert.PacketLatticeData.restrictLabels_length line 51
  8. theorem OAI.LipschitzHilbert.PacketLatticeData.restrictedLabels_card_le line 54
  9. def OAI.LipschitzHilbert.PacketLatticeData.tagLabelEquiv line 60
  10. theorem OAI.LipschitzHilbert.PacketLatticeData.tagLabelEquiv_apply line 66
  11. theorem OAI.LipschitzHilbert.PacketLatticeData.sum_tag_restrictions line 73

    Source documentation

    The partition has exactly one copy of each original term, including arbitrary empty label fibers and empty spatial item types.

    theorem sum_tag_restrictions {E : Type*} [AddCommMonoid E] (j : Fin N)
    (f : ∀ l : P.labels j, Item j l → E) :
    (∑ g : Tag, ∑ l : (P.restrictLabels (fun i a => tag i a=g)).labels j,
      ∑ u : Item j l, f (P.restrictedOriginalLabel (fun i a => tag i a=g) j l) u) =
      ∑ l : P.labels j, ∑ u : Item j l, f l u := by
…
  12. def OAI.LipschitzHilbert.PacketLatticeData.withProfile line 86

    Source documentation

    Replacing the analyzing profile keeps all physical geometry.

    def withProfile (alt : ∀ j (l : P.labels j), Item j l → κ → SchwartzMap (ℝ×ℝ) ℂ)
    (hAlt : ∀ j l u k, planarProfileConstant (alt j l u k) (2*P.order) ≤ P.profileBound) :
    PacketLatticeData N κ Label Item :=
…

    Mentions: OAI.LipschitzHilbert.planarProfileConstant, OAI.LipschitzHilbert.PacketLatticeData