SourcePacketSpectrum.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The packet spectrum and selector separation in the manuscript, §2, equations red:packet-spectra and red:selector-assumptions, give the actual reference-line annuli used in §5, conc:main-annuli.

The only spectral premise is the original planar packet's tilted wedge and positive vertical band. The same premise suffices for the first two scaled covariant derivatives. Angular frequencies and mathlib's cycles-per-unit convention are related explicitly.

theorem OAI.LipschitzHilbert.source_frequency_annulus line 20
theorem OAI.LipschitzHilbert.sourcePacket_angular_annulus line 74
Source documentation
Exact angular-frequency annulus for an actual affine-line slice.
```
theorem sourcePacket_angular_annulus {ω : ℝ}
    (hω : angularFourier (planarSchwartzSlice f b s) ω ≠ 0) :
    (cEta * cb - cStar) / ell ≤ |ω| ∧
      |ω| ≤ (CEta * Cb + cStar) / ell := by
…
```
Mentions: OAI.LipschitzHilbert.angularFourier, OAI.LipschitzHilbert.planarSchwartzSlice
theorem OAI.LipschitzHilbert.sourcePacket_fourier_annulus line 92
Source documentation
The same annulus, with endpoints converted to mathlib's Fourier transform convention by division by 2π.
```
theorem sourcePacket_fourier_annulus {ξ : ℝ}
    (hξ : 𝓕 (planarSchwartzSlice f b s) ξ ≠ 0) :
    (cEta * cb - cStar) / (2 * Real.pi * ell) ≤ |ξ| ∧
      |ξ| ≤ (CEta * Cb + cStar) / (2 * Real.pi * ell) := by
…
```
Mentions: OAI.LipschitzHilbert.planarSchwartzSlice
theorem OAI.LipschitzHilbert.sourcePacket_jet_spectrum line 113

theorem OAI.LipschitzHilbert.sourcePacket_jet_fourier_annulus line 125

Source documentation

All three covariant jets lie in the same actual line annulus; there is no separate spectral assumption on either derivative.

theorem sourcePacket_jet_fourier_annulus (frequency scale : ℝ) (i : Fin 3) {ξ : ℝ}
    (hξ : 𝓕 (planarSchwartzSlice (planarCovariantJet f frequency scale i) b s) ξ ≠ 0) :
    (cEta * cb - cStar) / (2 * Real.pi * ell) ≤ |ξ| ∧
      |ξ| ≤ (CEta * Cb + cStar) / (2 * Real.pi * ell) :=
…

Mentions: OAI.LipschitzHilbert.planarSchwartzSlice, OAI.LipschitzHilbert.planarCovariantJet

theorem OAI.LipschitzHilbert.sourcePacket_jet_fourier_cutoffs line 135
theorem OAI.LipschitzHilbert.sourcePacket_annulus_inner_pos line 156
Source documentation
The prescribed small bandwidth makes the lower annulus endpoint strictly positive, as required by the annular-variation theorem.
```
theorem sourcePacket_annulus_inner_pos {ell cStar cEta cb : ℝ}
    (hell : 0 < ell) (hgap : cStar < cEta * cb) :
    0 < (cEta * cb - cStar) / (2 * Real.pi * ell) :=
…
```
theorem OAI.LipschitzHilbert.sourcePacket_annulus_outer_nonneg line 161