OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralChainCorePower.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The differentiated weak solution is still a regular harmonic function in its second core component: the new source is the vanishing first core component of the leading kernel vector.

  1. theorem OAI.DefocusingNLS.spectralSecondChain_core_power line 14