StationaryInverse.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

The finite inverse for the higher-dimensional stationary expansion

The polynomials are those of osc:L-operators and osc:B-operators in Section 6 of the manuscript. Their variable represents the sphere Laplacian. The finite inverse identity is algebraic and independent of a sphere stationary-phase expansion.

def OAI.Falconer.sphereStationaryConstant line 23
theorem OAI.Falconer.sphereStationaryConstant_ne_zero line 27
def OAI.Falconer.sphereDirectPolynomial line 36
Source documentation
The direct stationary coefficient, as a polynomial in the sphere Laplacian. Here n is the sphere dimension, so the ambient dimension is n+1.
```
noncomputable def sphereDirectPolynomial (n j : ℕ) : Polynomial ℂ :=
…
```
theorem OAI.Falconer.sphereDirectPolynomial_zero line 41
theorem OAI.Falconer.sphereDirectPolynomial_degree line 45
theorem OAI.Falconer.constant_polynomial_product line 54
theorem OAI.Falconer.polynomial_product_reorder line 59
theorem OAI.Falconer.sphereDirectPolynomial_succ line 64
Source documentation
The coefficient recurrence obtained by substituting the outgoing series in the Helmholtz equation, with the manuscript's Laplacian sign convention.
```
theorem sphereDirectPolynomial_succ (n j : ℕ) :
    C (2 * Complex.I * (j+1)) * sphereDirectPolynomial n (j+1) =
      (X + C ((j : ℂ)*(j+1) - (n : ℂ)*((n : ℂ)-2)/4)) *
        sphereDirectPolynomial n j := by
…
```
Mentions: OAI.Falconer.sphereDirectPolynomial

def OAI.Falconer.sphereInversePolynomial line 91

Source documentation

The finite inverse coefficients from osc:B-operators.

noncomputable def sphereInversePolynomial (n : ℕ) : ℕ → Polynomial ℂ
  | 0 => C ((sphereStationaryConstant n)⁻¹)
  | j+1 => C (-(sphereStationaryConstant n)⁻¹) *
      ∑ h ∈ Finset.range (j+1),
        sphereDirectPolynomial n (h+1) * sphereInversePolynomial n (j-h)
termination_by j => j
decreasing_by omega

Mentions: OAI.Falconer.sphereStationaryConstant, OAI.Falconer.sphereDirectPolynomial

theorem OAI.Falconer.sphereInversePolynomial_zero line 99
theorem OAI.Falconer.sphereInversePolynomial_degree line 103
theorem OAI.Falconer.sphereInversePolynomial_cancellation line 119
theorem OAI.Falconer.sphereInversePolynomial_cancellation_reverse line 135
theorem OAI.Falconer.sphereInversePolynomial_triangle line 149
Source documentation
Exact cancellation in the triangular truncation used for the inverse stationary expansion, before estimating any analytic remainder.
```
theorem sphereInversePolynomial_triangle (n J : ℕ) (t : ℂ) :
    (∑ j ∈ Finset.range (J+1), ∑ h ∈ Finset.range (J+1-j),
      C (t^(j+h)) * sphereDirectPolynomial n h * sphereInversePolynomial n j) = 1 := by
…
```
Mentions: OAI.Falconer.sphereDirectPolynomial, OAI.Falconer.sphereInversePolynomial
theorem OAI.Falconer.sphereInversePolynomial_triangle_linear line 168
Source documentation
Applying the triangular identity to a Laplacian jet evaluated at a point. The relevant linear map is p ↦ (p(Δ)b)(e).
```
theorem sphereInversePolynomial_triangle_linear (n J : ℕ) (t : ℂ)
    (F : Polynomial ℂ →ₗ[ℂ] ℂ) :
    (∑ j ∈ Finset.range (J+1), t^j *
      ∑ h ∈ Finset.range (J+1-j),
        t^h * F (sphereDirectPolynomial n h * sphereInversePolynomial n j)) = F 1 := by
…
```
Mentions: OAI.Falconer.sphereDirectPolynomial, OAI.Falconer.sphereInversePolynomial

theorem OAI.Falconer.sphereInversePolynomial_error_identity line 187

Source documentation

The exact error identity for inversion. Each I j is a normalized stationary integral of B_j b, expanded through order J-j.

theorem sphereInversePolynomial_error_identity (n J : ℕ) (t z : ℂ)
    (F : Polynomial ℂ →ₗ[ℂ] ℂ) (I : ℕ → ℂ) :
    (∑ j ∈ Finset.range (J+1), t^j * I j) - z * F 1 =
      ∑ j ∈ Finset.range (J+1), t^j *
        (I j - z * ∑ h ∈ Finset.range (J+1-j),
          t^h * F (sphereDirectPolynomial n h * sphereInversePolynomial n j)) := by
…

Mentions: OAI.Falconer.sphereDirectPolynomial, OAI.Falconer.sphereInversePolynomial

theorem OAI.Falconer.sphereInversePolynomial_remainder line 202

Source documentation

No uniformity or analyticity is hidden in finite inversion: it costs exactly the sum of the weighted direct remainder bounds.

theorem sphereInversePolynomial_remainder (n J : ℕ) (t z : ℂ)
    (F : Polynomial ℂ →ₗ[ℂ] ℂ) (I : ℕ → ℂ) (E : ℕ → ℝ)
    (hE : ∀ j ∈ Finset.range (J+1),
      ‖I j - z * ∑ h ∈ Finset.range (J+1-j),
        t^h * F (sphereDirectPolynomial n h * sphereInversePolynomial n j)‖ ≤ E j) :
    ‖(∑ j ∈ Finset.range (J+1), t^j * I j) - z * F 1‖ ≤
      ∑ j ∈ Finset.range (J+1), ‖t‖^j * E j := by
…

Mentions: OAI.Falconer.sphereDirectPolynomial, OAI.Falconer.sphereInversePolynomial