OAI/Analysis/LipschitzHilbert/Trees/SourceLongPrefixes.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The long packets form a literal prefix in scale. Every truncated interval of that prefix has the proved coordinate cutoffs and is bounded pointwise by the original tree maximum.

  1. def OAI.LipschitzHilbert.SourceLabeledLattice.longPrefix line 18
  2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.longPrefix_le line 21
  3. theorem OAI.LipschitzHilbert.SourceLabeledLattice.longPrefix_spec line 26
  4. def OAI.LipschitzHilbert.SourceLabeledLattice.physicalLongIntervalSchwartz line 37
  5. theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalLongIntervalSchwartz_norm line 43
  6. theorem OAI.LipschitzHilbert.SourceLabeledLattice.horizontal_sub line 57
  7. theorem OAI.LipschitzHilbert.SourceLabeledLattice.vertical_sub line 62
  8. theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalLongIntervalSchwartz_bands line 68

    Source documentation

    The cutoff scale is the actual horizontal cell length.

    theorem physicalLongIntervalSchwartz_bands
    (c : ∀ j (l : P.labels j), Item j l → EuclideanSpace ℂ κ)
    (lo hi : ℕ) (r w cStar cEta CEta Cb : ℝ)
    (hr : 0<r) (hw : 0<w) (hcStar : 0≤cStar) (hcEta : 0<cEta)
    (hCEta : 0≤CEta) (hCb : 0≤Cb)
    (hspectrum : ∀ j l u k ξ η, planarAngularFourier (P.physicalPacket 0 j l u k) (ξ,η)≠0 →
      |ξ+P.rowSlope j l*η|≤cStar/P.length j ∧ cEta≤w*η ∧ w*η≤CEta)
    (hselector : ∀ j l, |P.rowSlope j l|≤Cb*w/P.length j) :
    (∀ y ξ, 𝓕 (vectorHorizontalSlice (P.physicalLongIntervalSchwartz 0 r c lo hi) y) ξ≠0 →
      |ξ|≤(CEta*Cb+cStar)/(2*Real.pi*r)) ∧
    (∀ x η, 𝓕 (vectorVerticalSlice (P.physicalLongIntervalSchwartz 0 r c lo hi) x) η≠0 →
      |η|≤CEta/(2*Real.pi*w)) := by
…

    Mentions: OAI.LipschitzHilbert.planarAngularFourier, OAI.LipschitzHilbert.vectorHorizontalSlice, OAI.LipschitzHilbert.vectorVerticalSlice