SphereStationary.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Full-sphere stationary phase for the actual amplitude

The two pole expansions are combined with the proved off-pole estimate. The only inputs are the recorded gnomonic surface formula and the precise quadratic stationary-phase specialization. No spherical estimate is an assumption.

def OAI.Falconer.directStationarySum line 17

theorem OAI.Falconer.sphere_stationary_expansion line 23

Source documentation

Full outgoing/incoming expansion, with the original symbol and original sphere measure. The derivative budget is 2*J+d.

theorem sphere_stationary_expansion
    (hgnomonic : PublishedGnomonicSurface) (hquadratic : PublishedQuadraticStationary)
    (m J : ℕ) (hJ : 1 ≤ J) :
    ∃ A : ℝ, 0 ≤ A ∧ ∀ (e : Sphere (m+3)) (B : Space (m+3) → ℂ),
      ContDiff ℝ ∞ B → ∀ C D : ℝ, 0 ≤ C → 1 ≤ D →
      (∀ j ≤ 2*J+(m+2)+1, ∀ w : Sphere (m+3),
        ‖iteratedFDeriv ℝ j B w‖ ≤ C*D^j) →
      ∀ Λ : ℝ, 1 ≤ Λ →
      ‖((Λ^(((m+2 : ℕ) : ℝ)/2) : ℝ) : ℂ)*sphereOscillation Λ e (fun w => B w) -
        (Complex.exp (Complex.I*(Λ : ℂ))*directStationarySum m J Λ B e +
          star (Complex.exp (Complex.I*(Λ : ℂ))*
            directStationarySum m J Λ (antipodalConjugate B) e))‖ ≤
…

Mentions: OAI.Falconer.PublishedGnomonicSurface, OAI.Falconer.PublishedQuadraticStationary, OAI.Falconer.Sphere, OAI.Falconer.Space, OAI.Falconer.sphereOscillation, OAI.Falconer.directStationarySum, OAI.Falconer.antipodalConjugate