SourceDemodulatedFourier.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Exact translation of the angular Fourier transform when the vertical bin carrier is removed.

theorem OAI.LipschitzHilbert.planarAngularFourier_vertical_demodulation line 15
theorem OAI.LipschitzHilbert.planarAngularFourier_verticalDemodulation line 26

theorem OAI.LipschitzHilbert.demodulated_packet_bands line 35

Source documentation

A bin of width proportional to 1/W becomes a low vertical-frequency band; the horizontal bound still uses w and cancels its slope factor.

theorem demodulated_packet_bands
    (f : ℝ×ℝ → ℂ) (nu theta ell W w cStar CEta Cb Cv : ℝ)
    (hell : 0<ell) (hw : 0<w) (hCb : 0≤Cb)
    (hslope : |theta|≤Cb*w/ell)
    (hspectrum : ∀ xi eta, planarAngularFourier f (xi,eta)≠0 →
      |xi+theta*eta|≤cStar/ell ∧ |eta|≤CEta/w)
    (hbin : ∀ xi eta, planarAngularFourier f (xi,eta)≠0 → |eta-nu|≤Cv/W) :
    ∀ xi eta, planarAngularFourier (fun z => verticalCarrier (-nu) z*f z) (xi,eta)≠0 →
      |xi|≤(cStar+Cb*CEta)/ell ∧ |eta|≤Cv/W := by
…

Mentions: OAI.LipschitzHilbert.planarAngularFourier, OAI.LipschitzHilbert.verticalCarrier

theorem OAI.LipschitzHilbert.verticalDemodulation_coordinate_bands line 59

Source documentation

Componentwise bin support gives the coordinate slice bounds for the whole demodulated vector, without a factor for its dimension.

theorem verticalDemodulation_coordinate_bands (nu : κ → ℝ)
    (f : SchwartzMap (ℝ×ℝ) (EuclideanSpace ℂ κ)) (Rx Ry : ℝ)
    (hf : ∀ k xi eta, planarAngularFourier (fun z => f z k) (xi,eta)≠0 →
      |xi|≤Rx ∧ |eta-nu k|≤Ry) :
    (∀ y xi, 𝓕 (vectorHorizontalSlice (verticalDemodulation nu f) y) xi≠0 →
      |xi|≤Rx/(2*Real.pi)) ∧
    (∀ x eta, 𝓕 (vectorVerticalSlice (verticalDemodulation nu f) x) eta≠0 →
      |eta|≤Ry/(2*Real.pi)) := by
…

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