QuadraticStationary.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Applying the quadratic expansion to the actual sphere integral

The amplitude is the explicitly computed surface density times the spherical amplitude, extended by zero from the fixed unit chart. Smoothness and its quantitative derivative bounds are retained as local obligations. The only published inputs are the gnomonic measure formula and the fixed Euclidean quadratic stationary-phase theorem.

def OAI.Falconer.quadraticAmplitude line 21
theorem OAI.Falconer.quadraticAmplitude_tsupport line 26
theorem OAI.Falconer.quadraticAmplitude_hasCompactSupport line 31

theorem OAI.Falconer.quadraticAmplitude_contDiff line 38

Source documentation

A mask that vanishes in the outer half of the fixed chart removes the boundary issue in extending its chart amplitude by zero.

theorem quadraticAmplitude_contDiff (m : ℕ) (b : Sphere (m+3) → ℂ)
    (hb : ContDiffOn ℝ ∞
      (fun u : Space (m+2) => b (gnomonicChart (quadraticToGnomonic u)))
      (Metric.ball (0 : Space (m+2)) 1))
    (hmask : ∀ u : Space (m+2), (1:ℝ)/2 ≤ ‖u‖ → ‖u‖ < 1 →
      b (gnomonicChart (quadraticToGnomonic u)) = 0) :
    ContDiff ℝ ∞ (quadraticAmplitude m b) := by
…

Mentions: OAI.Falconer.Sphere, OAI.Falconer.Space, OAI.Falconer.gnomonicChart, OAI.Falconer.quadraticToGnomonic, OAI.Falconer.quadraticAmplitude

theorem OAI.Falconer.quadraticAmplitude_derivatives_bounded line 71
def OAI.Falconer.quadraticSphereOscillation line 77
theorem OAI.Falconer.quadraticSphereOscillation_eq line 84

theorem OAI.Falconer.quadraticSphereOscillation_remainder line 111

Source documentation

The published Euclidean estimate bounds the spherical oscillation. No spherical coefficient formula is presupposed: the jets on the right are the actual iterated Euclidean Laplacians of the chart amplitude.

theorem quadraticSphereOscillation_remainder
    (hgnomonic : PublishedGnomonicSurface) (hquadratic : PublishedQuadraticStationary)
    (m J : ℕ) (hJ : 1 ≤ J) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ (b : Sphere (m+3) → ℂ), Measurable b →
      (∀ w, w ∉ northHemisphere (m+2) → b w = 0) →
      (∀ x : Space (m+2),
        x ∉ quadraticToGnomonic '' Metric.ball (0 : Space (m+2)) 1 →
          b (gnomonicChart x) = 0) →
      ContDiff ℝ ∞ (quadraticAmplitude m b) →
      ∀ B : ℝ, 0 ≤ B →
        (∀ k ≤ 2*J+(m+2)+1, ∀ x,
          ‖iteratedFDeriv ℝ k (quadraticAmplitude m b) x‖ ≤ B) →
…

Mentions: OAI.Falconer.PublishedGnomonicSurface, OAI.Falconer.PublishedQuadraticStationary, OAI.Falconer.Sphere, OAI.Falconer.northHemisphere, OAI.Falconer.Space, OAI.Falconer.quadraticToGnomonic, OAI.Falconer.gnomonicChart, OAI.Falconer.quadraticAmplitude