OAI/MathematicalPhysics/DefocusingNLS/Certificates/LaguerreHilbert.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Hilbert-space decay of Laguerre coefficients

Multiplication by exp (-t/2) puts the weighted problem into the ordinary complex L² space on the positive ray. Bessel's inequality then proves decay of coefficients without presupposing completeness of the Laguerre family.

  1. def OAI.DefocusingNLS.halfWeighted line 19
  2. theorem OAI.DefocusingNLS.halfWeighted_norm_sq line 22
  3. theorem OAI.DefocusingNLS.halfWeighted_inner line 31
  4. theorem OAI.DefocusingNLS.memLp_halfWeighted_of_exp_bound line 44
  5. theorem OAI.DefocusingNLS.memLp_halfWeighted_laguerre line 72
  6. def OAI.DefocusingNLS.laguerreL2 line 78
  7. theorem OAI.DefocusingNLS.inner_laguerreL2_halfWeighted line 81
  8. theorem OAI.DefocusingNLS.orthonormal_laguerreL2 line 95
  9. theorem OAI.DefocusingNLS.laguerreCoefficientIntegral_tendsto_zero line 105