OAI/Analysis/LipschitzHilbert/Trees/SourceScaleRestrictionSums.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Dropping an initial scale segment is an exact reindexing of finite packet sums. Original coefficients and physical packets are retained.

  1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.dropIndex_injective line 16
  2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.dropIndex_surjective_tail line 23
  3. theorem OAI.LipschitzHilbert.SourceLabeledLattice.sum_dropIndex line 30
  4. theorem OAI.LipschitzHilbert.SourceLabeledLattice.sum_dropScales line 44
  5. theorem OAI.LipschitzHilbert.SourceLabeledLattice.dropScales_selector_value line 53

    Source documentation

    The full selector sum is unchanged when all omitted coefficients are zero.

    theorem dropScales_selector_value (first : Fin N) (t : ℝ)
    (c : ∀ j (l : P.labels j), Item j l → EuclideanSpace ℂ κ)
    (hz : ∀ j, j.val<first.val → ∀ l u, c j l u=0)
    (selector : ∀ j, P.labels j → κ → ℂ) (z : ℝ×ℝ) :
    (P.dropScales first).physicalTreeSelectorValue t
      (fun j l u => c (dropIndex first j) l u)
      (fun j l k => selector (dropIndex first j) l k) z=
      P.physicalTreeSelectorValue t c selector z := by
…

    Mentions: OAI.LipschitzHilbert.SourceLabeledLattice.physicalTreeSelectorValue, OAI.LipschitzHilbert.SourceLabeledLattice.dropIndex