OAI/Analysis/LipschitzHilbert/Trees/SourceLengthRestriction.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Restricting to an interval of original packet lengths preserves all interval concentration bounds. The resulting coefficients are explicit zero extensions of the original analyzing coefficients.

  1. def OAI.LipschitzHilbert.SourceLabeledLattice.restrictCoefficient line 17
  2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.rawBand_restrictCoefficient line 22
  3. theorem OAI.LipschitzHilbert.SourceLabeledLattice.restricted_rawInterval_eq line 34
  4. theorem OAI.LipschitzHilbert.SourceLabeledLattice.restricted_rawInterval_bound line 60

    Source documentation

    Every restricted source interval is an original interval, including when the two length ranges are disjoint.

    theorem restricted_rawInterval_bound (P : SourceLabeledLattice N κ Label Item)
    (coeff : ∀ j (l : P.labels j), Item j l → EuclideanSpace ℂ κ)
    (lengthLower lengthUpper : ℕ) (jet : Fin 3) (x y B : ℝ)
    (hbound : ∀ lower upper, lower ≤ upper → upper ≤ N →
      ‖P.rawInterval coeff jet lower upper x y‖ ≤ B) :
    ∀ lower upper, lower ≤ upper → upper ≤ N →
      ‖P.rawInterval (P.restrictCoefficient coeff lengthLower lengthUpper)
        jet lower upper x y‖ ≤ B := by
…

    Mentions: OAI.LipschitzHilbert.SourceLabeledLattice