OAI/MathematicalPhysics/DefocusingNLS/Certificates/LaguerrePolynomial.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The Laguerre polynomials used in the slow-solution projection

The normalization is Lₙ(0) = 1, with weight exp (-t) on the positive ray. The differential and derivative identities hold as polynomial identities.

  1. def OAI.DefocusingNLS.laguerreCoefficient line 18
  2. def OAI.DefocusingNLS.laguerrePolynomial line 21
  3. theorem OAI.DefocusingNLS.laguerreCoefficient_eq_zero line 24
  4. theorem OAI.DefocusingNLS.coeff_laguerrePolynomial line 28
  5. theorem OAI.DefocusingNLS.laguerreCoefficient_zero line 37
  6. theorem OAI.DefocusingNLS.laguerrePolynomial_eval_zero line 40
  7. theorem OAI.DefocusingNLS.laguerrePolynomial_zero line 44
  8. theorem OAI.DefocusingNLS.laguerreCoefficient_recurrence line 48
  9. theorem OAI.DefocusingNLS.laguerrePolynomial_differential_equation line 67

    Source documentation

    t Lₙ'' + (1-t)Lₙ' + n Lₙ = 0, as a polynomial identity.

    theorem laguerrePolynomial_differential_equation (n : ℕ) :
    X * (laguerrePolynomial n).derivative.derivative +
      (1 - X) * (laguerrePolynomial n).derivative +
      C (n : ℂ) * laguerrePolynomial n = 0 := by
…

    Mentions: OAI.DefocusingNLS.laguerrePolynomial

  10. theorem OAI.DefocusingNLS.laguerreCoefficient_derivative_step line 84
  11. theorem OAI.DefocusingNLS.laguerrePolynomial_derivative_step line 98
  12. theorem OAI.DefocusingNLS.laguerrePolynomial_derivative line 107

    Source documentation

    The derivative has the finite triangular expansion used in projection.

    theorem laguerrePolynomial_derivative (n : ℕ) :
    (laguerrePolynomial n).derivative =
      -∑ j ∈ Finset.range n, laguerrePolynomial j := by
…

    Mentions: OAI.DefocusingNLS.laguerrePolynomial