PacketDataReferenceConditions.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Frozen main coefficients vanish outside the fixed selector cone. Restricting the main reference family to that cone is an exact identity; its carrier bound therefore does not inherit the wide error cone.

def OAI.LipschitzHilbert.PacketLatticeData.referenceCondition line 17
def OAI.LipschitzHilbert.PacketLatticeData.referenceLabelsEquiv line 22

theorem OAI.LipschitzHilbert.PacketLatticeData.sum_referenceLabels_of_zero line 35

Source documentation

A finite source sum supported on the reference labels equals the sum in the literal restricted family.

theorem sum_referenceLabels_of_zero {E : Type*} [AddCommMonoid E]
    (oldSlope newSlope referenceLength cone w : ℝ) (j : Fin N)
    (f : ∀ l : P.labels j, Item j l → E)
    (hzero : ∀ l, ¬P.referenceCondition oldSlope newSlope referenceLength cone w j l →
      ∀ u, f l u = 0) :
    (∑ l : P.referenceLabels oldSlope newSlope referenceLength cone w j,
      ∑ u : Item j l, f (P.referenceOriginalLabel oldSlope newSlope referenceLength cone w j l) u) =
      ∑ l : P.labels j, ∑ u : Item j l, f l u := by
…

theorem OAI.LipschitzHilbert.PacketLatticeData.sum_reference_frozen line 60

Source documentation

Nonzero frozen selector values force both shortness and narrow angular membership. Any term annihilated by a zero frozen selector can therefore be restricted exactly, including positive norm envelopes.

theorem sum_reference_frozen {E : Type*} [AddCommMonoid E]
    (oldSlope newSlope referenceLength cone w : ℝ) (j : Fin N)
    (c : ∀ l : P.labels j, Item j l → κ → ℂ)
    (f : ∀ l : P.labels j, Item j l → E)
    (hshort : ∀ l u k, c l u k ≠ 0 → P.length j ≤ referenceLength)
    (hsupport : ∀ l u k, c l u k ≠ 0 →
      |oldSlope+P.rowSlope j l-newSlope| ≤ cone*w/P.length j)
    (hvanish : ∀ l u, (∀ k, c l u k = 0) → f l u = 0) :
    (∑ l : P.referenceLabels oldSlope newSlope referenceLength cone w j,
      ∑ u : Item j l, f (P.referenceOriginalLabel oldSlope newSlope referenceLength cone w j l) u) =
      ∑ l : P.labels j, ∑ u : Item j l, f l u := by
…