SphereOffPole.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Decay away from the two stationary poles

The actual normalized cap partition reduces a full-sphere amplitude to the proved capwise integration-by-parts estimate. The only published input is the gnomonic surface formula. Constants depend on the fixed distance from the poles, dimension, and differentiation order.

theorem OAI.Falconer.offPole_center_gap line 19

theorem OAI.Falconer.sphere_offPole_decay line 41

Source documentation

Uniform full-sphere integration by parts for an amplitude separated from both poles. Its hypotheses are ordinary chart derivative bounds on the original amplitude, before cap localization.

theorem sphere_offPole_decay (hpublished : PublishedGnomonicSurface)
    (n m : ℕ) (hn : 1 ≤ n) {ε : ℝ} (hε : 0 < ε) :
    ∃ K : ℝ, 0 ≤ K ∧ ∀ (v : Space (n+2)) (b : Sphere (n+2) → ℂ),
      ‖v‖ = 1 → Measurable b →
      (∀ w, b w ≠ 0 → ε ≤ ‖perpendicularPart (w : Space (n+2)) v‖) →
      (∀ e : Space (n+2) ≃ₗᵢ[ℝ] Space (n+2), ∀ y : Space n, ‖y‖ ≤ 1 →
        ContDiff ℝ ∞ (rotatedChartAmplitude e b y)) →
      ∀ (M C D Λ : ℝ), 0 ≤ C → 1 ≤ D → 0 < Λ →
      (∀ w, ‖b w‖ ≤ M) →
      (∀ e : Space (n+2) ≃ₗᵢ[ℝ] Space (n+2), ∀ y : Space n, ‖y‖ ≤ 1 →
        ∀ k ≤ m, ∀ u ∈ Icc (-1 : ℝ) 1,
          ‖iteratedDeriv k (rotatedChartAmplitude e b y) u‖ ≤ C*D^k) →
…

Mentions: OAI.Falconer.PublishedGnomonicSurface, OAI.Falconer.Space, OAI.Falconer.Sphere, OAI.Falconer.perpendicularPart, OAI.Falconer.rotatedChartAmplitude