QuadraticBudget.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The derivative budget of the actual quadratic amplitude

The fixed pole cutoff and fixed quadratic geometry cost constants depending only on the dimension and derivative order. The original symbol supplies the entire scale power.

theorem OAI.Falconer.mixed_product_uniform_bound_at line 18
theorem OAI.Falconer.poleLocalizedAmbient_uniform_budget line 40
theorem OAI.Falconer.quadraticAmplitude_tsupport_half line 77
theorem OAI.Falconer.quadratic_chart_composition_uniform_budget line 97

theorem OAI.Falconer.pole_quadratic_amplitude_budget line 135

Source documentation

Uniform global bounds for the actual zero-extended quadratic amplitude. The scale appears with exactly the highest requested derivative order K.

theorem pole_quadratic_amplitude_budget (m K : ℕ) :
    ∃ L : ℝ, 0 ≤ L ∧ ∀ (e : Sphere (m+3)) (B : Space (m+3) → ℂ),
      ContDiff ℝ ∞ B → ∀ C D : ℝ, 0 ≤ C → 1 ≤ D →
      (∀ j ≤ K, ∀ w : Sphere (m+3), ‖iteratedFDeriv ℝ j B w‖ ≤ C*D^j) →
      ∀ j ≤ K, ∀ u,
        ‖iteratedFDeriv ℝ j (quadraticAmplitude m
          (fun w => poleLocalizedAmbient e B (sphereMap (stationaryPoleRotation e) w))) u‖ ≤
          L*C*D^K := by
…

Mentions: OAI.Falconer.Sphere, OAI.Falconer.Space, OAI.Falconer.quadraticAmplitude, OAI.Falconer.poleLocalizedAmbient, OAI.Falconer.sphereMap, OAI.Falconer.stationaryPoleRotation

theorem OAI.Falconer.pole_stationary_remainder_of_ambient_bounds line 192

Source documentation

Quantitative outgoing stationary phase for the actual ambient symbol. The Euclidean derivative budget is derived, not assumed.

theorem pole_stationary_remainder_of_ambient_bounds
    (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) : ℝ) : ℂ) * Complex.exp (-(Complex.I*(Λ : ℂ))) *
          sphereOscillation Λ e (fun w => poleLocalizedAmbient e B w) -
        ∑ j ∈ Finset.range J, ((Λ ^ (-(j : ℝ)) : ℝ) : ℂ) *
          actualStationaryCoefficient m j B e‖ ≤
…

Mentions: OAI.Falconer.PublishedGnomonicSurface, OAI.Falconer.PublishedQuadraticStationary, OAI.Falconer.Sphere, OAI.Falconer.Space, OAI.Falconer.sphereOscillation, OAI.Falconer.poleLocalizedAmbient, OAI.Falconer.actualStationaryCoefficient