OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousHarmonicDecomposition.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Algebraic harmonic decomposition

A homogeneous polynomial is a homogeneous harmonic polynomial plus the squared radius times a polynomial of two lower degrees. The preimage is constructed by induction, using the positive radius-power coefficient.

  1. theorem OAI.DefocusingNLS.physicalPolynomialLaplacian_radius_preimage line 17
  2. theorem OAI.DefocusingNLS.physicalPolynomial_harmonic_decomposition line 57