OAI/Analysis/LipschitzHilbert/Trees/SourceCoordinateSpectrum.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Coordinate Fourier support of actual planar packets. These lemmas project the original two-dimensional spectrum without a tensor assumption.

  1. def OAI.LipschitzHilbert.planarSwap line 13
  2. theorem OAI.LipschitzHilbert.planarSwap_apply line 16
  3. def OAI.LipschitzHilbert.planarVerticalSlice line 19
  4. theorem OAI.LipschitzHilbert.planarVerticalSlice_apply line 22
  5. theorem OAI.LipschitzHilbert.planarFourier_swap line 27
  6. theorem OAI.LipschitzHilbert.planarVerticalSlice_fourier_eq_zero line 35
  7. theorem OAI.LipschitzHilbert.planarHorizontalSlice_fourier_band line 42
  8. theorem OAI.LipschitzHilbert.planarVerticalSlice_fourier_band line 53
  9. theorem OAI.LipschitzHilbert.planarAngularFourier_coordinate_bands line 64

    Source documentation

    Angular and cycles-per-unit cutoffs differ by exactly 2π.

    theorem planarAngularFourier_coordinate_bands (f : SchwartzMap (ℝ×ℝ) ℂ) (Rx Ry : ℝ)
    (hf : ∀ ξ η, planarAngularFourier f (ξ,η)≠0 → |ξ|≤Rx ∧ |η|≤Ry) :
    ∀ ξ η, planarFourier f (ξ,η)≠0 →
      |ξ|≤Rx/(2*Real.pi) ∧ |η|≤Ry/(2*Real.pi) := by
…

    Mentions: OAI.LipschitzHilbert.planarAngularFourier, OAI.LipschitzHilbert.planarFourier

  10. theorem OAI.LipschitzHilbert.planarVerticalSlice_angular_band line 78
  11. theorem OAI.LipschitzHilbert.sourcePacket_coordinate_bands line 93

    Source documentation

    The manuscript's wedge and positive transverse band give both coordinate cutoffs on the reference plane. Only the upper selector separation is needed here.

    theorem sourcePacket_coordinate_bands (f : SchwartzMap (ℝ×ℝ) ℂ)
    (θ ell w cStar cEta CEta Cb : ℝ)
    (hell : 0<ell) (hw : 0<w) (hcEta : 0<cEta) (hCb : 0≤Cb)
    (hspectrum : ∀ ξ η, planarAngularFourier f (ξ,η)≠0 →
      |ξ+θ*η|≤cStar/ell ∧ cEta≤w*η ∧ w*η≤CEta)
    (hselector : |θ|≤Cb*w/ell) :
    (∀ y ξ, 𝓕 (planarSchwartzSlice f y 0) ξ≠0 →
      |ξ|≤(CEta*Cb+cStar)/(2*Real.pi*ell)) ∧
    (∀ x η, 𝓕 (planarVerticalSlice f x) η≠0 →
      |η|≤CEta/(2*Real.pi*w)) := by
…

    Mentions: OAI.LipschitzHilbert.planarAngularFourier, OAI.LipschitzHilbert.planarSchwartzSlice, OAI.LipschitzHilbert.planarVerticalSlice

  12. theorem OAI.LipschitzHilbert.vectorHorizontalSlice_coordinate line 120
  13. theorem OAI.LipschitzHilbert.vectorVerticalSlice_coordinate line 128
  14. theorem OAI.LipschitzHilbert.vector_coordinate_fourier_bands line 137

    Source documentation

    The same planar scalar-coordinate spectral rectangle controls the actual vector slices, with no loss depending on their dimension.

    theorem vector_coordinate_fourier_bands (f : SchwartzMap (ℝ×ℝ) (EuclideanSpace ℂ κ))
    (Rx Ry : ℝ)
    (hf : ∀ k ξ η, planarFourier (f.postcompCLM (vectorCoordinate k)) (ξ,η)≠0 →
      |ξ|≤Rx ∧ |η|≤Ry) :
    (∀ y ξ, 𝓕 (vectorHorizontalSlice f y) ξ≠0 → |ξ|≤Rx) ∧
    (∀ x η, 𝓕 (vectorVerticalSlice f x) η≠0 → |η|≤Ry) := by
…

    Mentions: OAI.LipschitzHilbert.planarFourier, OAI.LipschitzHilbert.vectorCoordinate, OAI.LipschitzHilbert.vectorHorizontalSlice, OAI.LipschitzHilbert.vectorVerticalSlice