OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralForcedEdgeBoundary.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

When the source is continuous at the constrained core, the flux extends to that core as well as to the outer boundary.

  1. theorem OAI.DefocusingNLS.spectralForced_closedBoundary_at_edge line 12