OAI/Analysis/LipschitzHilbert/Trees/SourceTreeSpectrum.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LipschitzHilbert.vector_horizontal_sum line 14
2. theorem OAI.LipschitzHilbert.vector_vertical_sum line 20
3. theorem OAI.LipschitzHilbert.vector_sum_bands line 26
4. def OAI.LipschitzHilbert.SourceLabeledLattice.physicalTreePartialSchwartz line 57
5. theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalTreePartialSchwartz_apply line 64
6. theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalTreePartialSchwartz_bands line 76

   Source documentation

   Uniform coordinate cutoffs for a genuine prefix of long packets. The cutoff is expressed at the cell scale rather than the smallest individual packet length.

   theorem physicalTreePartialSchwartz_bands
       (c : ∀ j (l : P.labels j), Item j l → EuclideanSpace ℂ κ)
       (n : ℕ) (r w cStar cEta CEta Cb : ℝ)
       (hr : 0<r) (hw : 0<w) (hcStar : 0≤cStar) (hcEta : 0<cEta)
       (hCEta : 0≤CEta) (hCb : 0≤Cb)
       (hlen : ∀ j : Fin N, j.val<n → r≤P.length j)
       (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.physicalTreePartialSchwartz 0 c n) y) ξ≠0 →
         |ξ|≤(CEta*Cb+cStar)/(2*Real.pi*r)) ∧
       (∀ x η, 𝓕 (vectorVerticalSlice (P.physicalTreePartialSchwartz 0 c n) x) η≠0 →
   …

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