OAI/Analysis/LipschitzHilbert/Packets/SourceLabeledPacketRestriction.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Any fixed residual packet subset is itself a lattice family, with unchanged geometry, analyzing integrals and alternate synthesis waves. Restricting the item fibers preserves the lattice constants exactly.

  1. def OAI.LipschitzHilbert.SourceLabeledLattice.RestrictedPacketItem line 19
  2. instance OAI.LipschitzHilbert.SourceLabeledLattice.restrictedPacketItemFintype line 22
  3. def OAI.LipschitzHilbert.SourceLabeledLattice.restrictPackets line 27
  4. theorem OAI.LipschitzHilbert.SourceLabeledLattice.restrictPackets_absoluteConstant line 35
  5. theorem OAI.LipschitzHilbert.SourceLabeledLattice.restrictPackets_constant line 38
  6. def OAI.LipschitzHilbert.SourceLabeledLattice.restrictedPacketEquiv line 42

    Source documentation

    The restricted packet type is precisely the selected finite set.

    def restrictedPacketEquiv (Q : Finset P.PacketIndex) :
    (P.restrictPackets Q).PacketIndex ≃ Q where
…

    Mentions: OAI.LipschitzHilbert.SourceLabeledLattice.PacketIndex

  7. theorem OAI.LipschitzHilbert.SourceLabeledLattice.restrictPackets_physicalPacket line 51
  8. theorem OAI.LipschitzHilbert.SourceLabeledLattice.restrictPackets_physicalMultiplierCoefficient line 55
  9. theorem OAI.LipschitzHilbert.SourceLabeledLattice.sum_restrictPackets line 63

    Source documentation

    Exact scalar/vector sums over the selected packet family.

    theorem sum_restrictPackets {E : Type*} [AddCommMonoid E] (Q : Finset P.PacketIndex)
    (f : P.PacketIndex → E) :
    (∑ q : (P.restrictPackets Q).PacketIndex, f ⟨q.1,⟨q.2.1,q.2.2.val⟩⟩) =
      ∑ q ∈ Q, f q := by
…

    Mentions: OAI.LipschitzHilbert.SourceLabeledLattice.PacketIndex

  10. theorem OAI.LipschitzHilbert.SourceLabeledLattice.sum_restrictPackets_filter line 70
  11. def OAI.LipschitzHilbert.SourceLabeledLattice.restrictedAlternate line 82

    Source documentation

    Alternate synthesis profiles are restricted along the same item map.

    def restrictedAlternate (Q : Finset P.PacketIndex) (j : Fin N)
    (l : (P.restrictPackets Q).labels j) (u : P.RestrictedPacketItem Q j l) (k : κ) :
    SchwartzMap (ℝ×ℝ) ℂ := alt j l u.val k
…
  12. theorem OAI.LipschitzHilbert.SourceLabeledLattice.restrictedAlternate_bound line 87
  13. theorem OAI.LipschitzHilbert.SourceLabeledLattice.restrictPackets_physicalMaskedValue line 93
  14. theorem OAI.LipschitzHilbert.SourceLabeledLattice.restrictPackets_physicalMaskedBand line 104

    Source documentation

    Every fixed selected length-band is the corresponding band of the literal restricted family, with the original analyzing coefficient.

    theorem restrictPackets_physicalMaskedBand (Q : Finset P.PacketIndex)
    (t : ℝ) (b : ∀ j, P.labels j → κ → ℝ → ℂ) (v : ℝ×ℝ → ℝ)
    (g : ℝ×ℝ → EuclideanSpace ℂ κ)
    (T : ∀ j (l : P.labels j), Item j l → SlopeBox) (L A y x : ℝ) (j : Fin N) :
    (P.restrictPackets Q).physicalMaskedBand (P.restrictedAlternate alt Q)
      (P.restrictedAlternate_bound alt hAlt Q) t b v g (fun j l u => T j l u.val) L A y j x =
      ∑ q ∈ Q.filter (fun q => q.1 = j),
        P.physicalMaskedValue alt hAlt t b v g T L A (x,y+t*x) q := by
…

    Mentions: OAI.LipschitzHilbert.SlopeBox, OAI.LipschitzHilbert.SourceLabeledLattice.physicalMaskedBand