SeparatorPolynomials.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Polynomial meaning of the integer separator calculation

Interpreting the coefficient lists as polynomials identifies their recurrence with the backward matrix product and its coefficientwise imaginary part.

def OAI.DefocusingNLS.SeparatorArithmetic.toPolynomial line 19
Source documentation
Ascending coefficient lists interpreted as polynomials.
```
noncomputable def toPolynomial : List GaussianInt → Polynomial GaussianInt
  | [] => 0
  | a :: as => C a + X * toPolynomial as
```
theorem OAI.DefocusingNLS.SeparatorArithmetic.toPolynomial_add line 23
theorem OAI.DefocusingNLS.SeparatorArithmetic.toPolynomial_scale line 34
theorem OAI.DefocusingNLS.SeparatorArithmetic.toPolynomial_mulLinear line 43
theorem OAI.DefocusingNLS.SeparatorArithmetic.coeff_toPolynomial line 50
theorem OAI.DefocusingNLS.SeparatorArithmetic.toPolynomial_backwardStep_fst line 61
Source documentation
The list update for the first matching coordinate is the polynomial matrix update specified in the appendix.
```
theorem toPolynomial_backwardStep_fst (ℓ n : ℕ)
    (xy : List GaussianInt × List GaussianInt) :
    toPolynomial (backwardStep ℓ n xy).1 =
      (C (⟨scale * n + 50000000 * ℓ - 3125000, -centerB⟩ : GaussianInt) +
        C (scale : GaussianInt) * X - C (⟨scale * (ℓ + 5), centerZ⟩ : GaussianInt)) *
        toPolynomial xy.1 - C (⟨0, centerZ⟩ : GaussianInt) * toPolynomial xy.2 := by
…
```
Mentions: OAI.DefocusingNLS.SeparatorArithmetic.toPolynomial, OAI.DefocusingNLS.SeparatorArithmetic.backwardStep, OAI.DefocusingNLS.SeparatorArithmetic.scale, OAI.DefocusingNLS.SeparatorArithmetic.centerB, OAI.DefocusingNLS.SeparatorArithmetic.centerZ
theorem OAI.DefocusingNLS.SeparatorArithmetic.toPolynomial_backwardStep_snd line 73
def OAI.DefocusingNLS.SeparatorArithmetic.imaginaryPart line 81
Source documentation
Imaginary part as an additive homomorphism, for coefficient sums.
```
def imaginaryPart : GaussianInt →+ ℤ where
…
```
theorem OAI.DefocusingNLS.SeparatorArithmetic.imaginaryPart_apply line 86
theorem OAI.DefocusingNLS.SeparatorArithmetic.coefficients_product_im line 88
theorem OAI.DefocusingNLS.SeparatorArithmetic.windingCoefficient_eq line 102
Source documentation
The exact integer pⱼ is the imaginary part of the product coefficient [X^j] x(X) conj(y)(X); no numeric translation is assumed.
```
theorem windingCoefficient_eq (ℓ j : ℕ) :
    windingCoefficient ℓ j =
      ((toPolynomial (backwardCoefficients ℓ).1 *
        (toPolynomial (backwardCoefficients ℓ).2).map (starRingEnd GaussianInt)).coeff j).im := by
…
```
Mentions: OAI.DefocusingNLS.SeparatorArithmetic.windingCoefficient, OAI.DefocusingNLS.SeparatorArithmetic.toPolynomial, OAI.DefocusingNLS.SeparatorArithmetic.backwardCoefficients