OAI/Analysis/LipschitzHilbert/Trees/SourceReferenceMainRestriction.lean

GitHub source file

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.

  1. def OAI.LipschitzHilbert.SourceLabeledLattice.referenceCondition line 18
  2. def OAI.LipschitzHilbert.SourceLabeledLattice.referenceLabelsEquiv line 23
  3. theorem OAI.LipschitzHilbert.SourceLabeledLattice.sum_referenceLabels_of_zero line 36

    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
…
  4. theorem OAI.LipschitzHilbert.SourceLabeledLattice.sum_reference_frozen line 61

    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
…