LaguerreOrthogonality.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Algebraic Laguerre orthogonality

The factorial moment functional realizes integration against exp (-t) on the positive ray. Integration by parts becomes a finite polynomial identity.

def OAI.DefocusingNLS.laguerreMoment line 15
theorem OAI.DefocusingNLS.laguerreMoment_monomial line 18
theorem OAI.DefocusingNLS.laguerreMoment_C line 22
theorem OAI.DefocusingNLS.laguerreMoment_C_mul line 25
theorem OAI.DefocusingNLS.laguerreMoment_derivative_sub line 30
Source documentation
The boundary term in integration by parts at zero.
```
theorem laguerreMoment_derivative_sub (p : ℂ[X]) :
    laguerreMoment (p.derivative - p) = -p.coeff 0 := by
…
```
Mentions: OAI.DefocusingNLS.laguerreMoment
def OAI.DefocusingNLS.laguerreOperator line 43
theorem OAI.DefocusingNLS.laguerreMoment_green line 47
Source documentation
The Laguerre operator is symmetric for the factorial moment functional.
```
theorem laguerreMoment_green (p q : ℂ[X]) :
    laguerreMoment (laguerreOperator p * q) =
      -laguerreMoment (X * p.derivative * q.derivative) := by
…
```
Mentions: OAI.DefocusingNLS.laguerreMoment, OAI.DefocusingNLS.laguerreOperator
theorem OAI.DefocusingNLS.laguerreOperator_laguerrePolynomial line 59
theorem OAI.DefocusingNLS.laguerreMoment_orthogonal line 65
theorem OAI.DefocusingNLS.laguerreMoment_derivative_self line 81
theorem OAI.DefocusingNLS.laguerreMoment_self line 90
Source documentation
This normalization gives squared norm one for every degree.
```
theorem laguerreMoment_self (n : ℕ) :
    laguerreMoment (laguerrePolynomial n * laguerrePolynomial n) = 1 := by
…
```
Mentions: OAI.DefocusingNLS.laguerreMoment, OAI.DefocusingNLS.laguerrePolynomial
theorem OAI.DefocusingNLS.laguerreMoment_orthonormal line 100