StationaryCoefficients.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Identification of the outgoing stationary coefficients

The zeroth coefficient is evaluated on the chart amplitude. The outgoing Helmholtz recurrence uniquely determines the manuscript's polynomial coefficients. The identification for local quadratic jets is conditional on their satisfying this recurrence.

theorem OAI.Falconer.quadraticAmplitude_zero line 19
theorem OAI.Falconer.quadraticJetCoefficient_amplitude_zero line 23
def OAI.Falconer.sphereDirectOperator line 33
Source documentation
Evaluation of the exact direct polynomial at a linear angular operator.
```
noncomputable def sphereDirectOperator (D : Module.End ℂ V) (n j : ℕ) : Module.End ℂ V :=
…
```
theorem OAI.Falconer.sphereDirectOperator_zero line 36
theorem OAI.Falconer.sphereDirectOperator_recurrence line 40

theorem OAI.Falconer.sphereDirectOperator_unique line 53

Source documentation

Once the genuine outgoing coefficients satisfy the Helmholtz recurrence, their identification with L_j is forced; no arbitrary choice of higher coefficients remains.

theorem sphereDirectOperator_unique (D : Module.End ℂ V) (n : ℕ) (b : V)
    (a : ℕ → V) (hzero : a 0 = sphereStationaryConstant n • b)
    (hrec : ∀ j : ℕ, (2 * Complex.I * (j+1)) • a (j+1) =
      D (a j) + ((j : ℂ)*(j+1) - (n : ℂ)*((n : ℂ)-2)/4) • a j) :
    ∀ j, a j = sphereDirectOperator D n j b := by
…

Mentions: OAI.Falconer.sphereStationaryConstant, OAI.Falconer.sphereDirectOperator