PhysicalPacketSpectrum.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The original physical packet spectrum supplies Fourier cutoffs for the actual three raw kernels on every affine reference line. The exact dyadic endpoint identity puts these cutoffs in the form required by the scaled annular-variation estimate.

theorem OAI.LipschitzHilbert.physicalPlanarJet_fourier_cutoffs line 32

Source documentation

No Fourier assumption on the derived raw kernels is needed: their low and high cutoffs follow from the original physical packet.

theorem physicalPlanarJet_fourier_cutoffs (i : Fin 3) :
    (∀ ξ, |ξ| < (cEta * cb - cStar) / (2 * Real.pi * ell) →
      𝓕 (modulatedPlanarJet f a (b - s * a) ell W (s - θ)
        frequency scale c hell.ne' i) ξ = 0) ∧
    (∀ ξ, (CEta * Cb + cStar) / (2 * Real.pi * ell) < |ξ| →
      𝓕 (modulatedPlanarJet f a (b - s * a) ell W (s - θ)
        frequency scale c hell.ne' i) ξ = 0) := by
…

Mentions: OAI.LipschitzHilbert.modulatedPlanarJet

theorem OAI.LipschitzHilbert.packet_annulus_dyadic_scale line 49
Source documentation
Exact rescaling of either annulus endpoint for a dyadic physical length. The same reference length R works for every index.
```
theorem packet_annulus_dyadic_scale (numerator R : ℝ) (j : ℕ) (hR : R ≠ 0) :
    numerator / (2 * Real.pi * (R / (2 : ℝ) ^ j)) =
      (numerator / (2 * Real.pi * R)) * (2 : ℝ) ^ j := by
…
```

theorem OAI.LipschitzHilbert.physicalPlanarJet_dyadic_fourier_cutoffs line 70

Source documentation

The concrete raw kernels have the dyadic cutoffs used in scalar and Hilbert annular variation, uniformly over all three covariant jets.

theorem physicalPlanarJet_dyadic_fourier_cutoffs
    (R : ℝ) (hR : 0 < R) (j : ℕ) (hlength : ell = R / (2 : ℝ) ^ j) (i : Fin 3) :
    (∀ ξ, |ξ| < ((cEta * cb - cStar) / (2 * Real.pi * R)) * (2 : ℝ) ^ j →
      𝓕 (modulatedPlanarJet f a (b - s * a) ell W (s - θ)
        frequency scale c hell.ne' i) ξ = 0) ∧
    (∀ ξ, ((CEta * Cb + cStar) / (2 * Real.pi * R)) * (2 : ℝ) ^ j < |ξ| →
      𝓕 (modulatedPlanarJet f a (b - s * a) ell W (s - θ)
        frequency scale c hell.ne' i) ξ = 0) := by
…

Mentions: OAI.LipschitzHilbert.modulatedPlanarJet