PublishedQuadraticStationary.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The fixed negative-quadratic stationary-phase input

Maciej Zworski, Semiclassical Analysis, AMS Graduate Studies in Mathematics 138 (2012), Theorem 3.13, equation (3.5.3), and the remainder estimate in its proof (printed pp. 54–55): https://math.jhu.edu/~lindblad/633/Zworski_final.pdf

This is only the specialization Q = -I, h = 1 / Λ, in dimension n = d - 1 ≥ 2, for amplitudes supported in the fixed closed unit ball. The Fourier convention in the cited formula is exp (-i ⟨x, ξ⟩), with D = (1/i) ∂. Consequently ⟨Q⁻¹ D, D⟩ is the ordinary Laplacian ∑ ∂ᵢ², and the coefficient is Δʲ / ((2i)ʲ j!). The Gaussian factor is (2π)^(n/2) exp (-iπn/4), already defined as sphereStationaryConstant.

The source controls the remainder by derivatives through order 2J+n+1. An operator-norm bound for the iterated Fréchet derivatives bounds each coordinate derivative; its dimensional constants are absorbed into C. No spherical stationary-phase statement is assumed here.

def OAI.Falconer.quadraticJetCoefficient line 34
Source documentation
Actual Euclidean iterated Laplacian, with the ordinary positive-second- derivative sign convention.
```
noncomputable def quadraticJetCoefficient {n : ℕ} (j : ℕ) (a : Space n → ℂ) : ℂ :=
…
```
Mentions: OAI.Falconer.Space
theorem OAI.Falconer.quadraticJetCoefficient_zero line 38
def OAI.Falconer.PublishedQuadraticStationary line 44
Source documentation
The fixed-quadratic stationary-phase hypothesis, uniform over amplitudes and frequencies.
```
def PublishedQuadraticStationary : Prop :=
…
```
theorem OAI.Falconer.quadratic_stationary_remainder line 58