OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralRobinNormBounds.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Norm bounds and coercivity of the local diagonal Robin relation.

  1. theorem OAI.DefocusingNLS.SpectralScalarBoundarySystem.inner_slope_norm line 10
  2. theorem OAI.DefocusingNLS.spectralCoupled_robin_coercivity line 25