OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousPolynomialLaplacian.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

The algebraic Laplacian on twelve-dimensional polynomials

The radius-multiplication identity is the algebraic ingredient for reducing sphere polynomial moments to homogeneous harmonic moments.

  1. abbrev OAI.DefocusingNLS.PhysicalRealPolynomial line 17
  2. def OAI.DefocusingNLS.physicalPolynomialLaplacian line 19
  3. def OAI.DefocusingNLS.physicalRadiusPolynomial line 23
  4. theorem OAI.DefocusingNLS.physicalPolynomialLaplacian_apply line 26
  5. theorem OAI.DefocusingNLS.pderiv_physicalRadiusPolynomial line 30
  6. theorem OAI.DefocusingNLS.physicalPolynomialLaplacian_radius line 35
  7. theorem OAI.DefocusingNLS.physicalRadiusPolynomial_homogeneous line 43
  8. theorem OAI.DefocusingNLS.physicalPolynomialLaplacian_mul line 48
  9. theorem OAI.DefocusingNLS.physicalPolynomialLaplacian_radius_mul line 60
  10. theorem OAI.DefocusingNLS.physicalPolynomialLaplacian_homogeneous line 73
  11. theorem OAI.DefocusingNLS.physicalPolynomialLaplacian_radius_pow_mul line 81
  12. theorem OAI.DefocusingNLS.physicalPolynomialLaplacian_constant line 111
  13. theorem OAI.DefocusingNLS.physicalPolynomialLaplacian_low_degree line 119
  14. theorem OAI.DefocusingNLS.physicalPolynomialLaplacian_iterate_homogeneous line 132
  15. theorem OAI.DefocusingNLS.physicalPolynomialLaplacian_iterate_zero line 142