OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralLiouvilleGreenData.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual forbidden scalar equation has a Dirichlet/outgoing Green kernel with a uniform bound. The arbitrary outgoing normalization cancels.

  1. theorem OAI.DefocusingNLS.spectralLiouville_forbidden_green_data line 12