PoleStationarySupport.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Actual support conditions for the pole expansion

Geometric support in a radius-1/4 cap implies all support conditions in the quadratic stationary theorem. The ambient pole bump is invisible to the actual coefficient jets at its center.

theorem OAI.Falconer.gnomonic_small_cap_coordinates line 18
theorem OAI.Falconer.fixed_cap_mem_north line 44
theorem OAI.Falconer.rotated_cap_quadratic_support line 59
def OAI.Falconer.poleLocalizedAmbient line 94
theorem OAI.Falconer.poleLocalizedAmbient_contDiff line 97
theorem OAI.Falconer.poleLocalizedAmbient_cap line 102
theorem OAI.Falconer.poleLocalizedAmbient_coefficient line 109
theorem OAI.Falconer.poleCutoff_opposite_neg line 119
theorem OAI.Falconer.poleLocalized_opposite_oscillation line 128
Source documentation
The incoming pole uses the same smooth direction patch as the outgoing pole, applied to the conjugated antipodal amplitude.
```
theorem poleLocalized_opposite_oscillation {d : ℕ} (Λ : ℝ) (e : Sphere d)
    (B : Space d → ℂ) :
    sphereOscillation Λ e (fun w => poleLocalizedAmbient (oppositePole e) B w) =
      star (sphereOscillation Λ e
        (fun w => poleLocalizedAmbient e (fun x => star (B (-x))) w)) := by
…
```
Mentions: OAI.Falconer.Sphere, OAI.Falconer.Space, OAI.Falconer.sphereOscillation, OAI.Falconer.poleLocalizedAmbient, OAI.Falconer.oppositePole
theorem OAI.Falconer.poleLocalized_quadratic_contDiff line 154

theorem OAI.Falconer.poleLocalized_stationary_remainder line 179

Source documentation

The local expansion has the original-amplitude coefficients. All support and smoothness requirements are discharged by the fixed bump. The remaining derivative bound is the explicit Euclidean jet budget.

theorem poleLocalized_stationary_remainder
    (hgnomonic : PublishedGnomonicSurface) (hquadratic : PublishedQuadraticStationary)
    (m J : ℕ) (hJ : 1 ≤ J) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ (e : Sphere (m+3)) (B : Space (m+3) → ℂ),
      ContDiff ℝ ∞ B → ∀ E : ℝ, 0 ≤ E →
      (∀ k ≤ 2*J+(m+2)+1, ∀ u,
        ‖iteratedFDeriv ℝ k (quadraticAmplitude m
          (fun w => poleLocalizedAmbient e B (sphereMap (stationaryPoleRotation e) w))) u‖ ≤ E) →
      ∀ Λ : ℝ, 1 ≤ Λ →
      ‖((Λ ^ (((m+2 : ℕ) : ℝ)/2) : ℝ) : ℂ) * Complex.exp (-(Complex.I*(Λ : ℂ))) *
          sphereOscillation Λ e (fun w => poleLocalizedAmbient e B w) -
        ∑ j ∈ Finset.range J, ((Λ ^ (-(j : ℝ)) : ℝ) : ℂ) *
…

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