OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralGaugeRobin.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Exact passage from the physical two-channel boundary condition to the profile gauge used by the coercive weak formulation.

  1. def OAI.DefocusingNLS.spectralGaugeColumns line 11
  2. def OAI.DefocusingNLS.spectralGaugeInverse line 14
  3. theorem OAI.DefocusingNLS.spectralGaugeColumns_det line 17
  4. theorem OAI.DefocusingNLS.spectralGaugeInverse_columns line 25
  5. theorem OAI.DefocusingNLS.spectralGaugeColumns_inverse line 29
  6. def OAI.DefocusingNLS.spectralGaugeRobin line 33
  7. theorem OAI.DefocusingNLS.spectralGaugeRobin_condition line 37
  8. theorem OAI.DefocusingNLS.spectralGaugeColumns_tendsto line 56
  9. theorem OAI.DefocusingNLS.spectralGaugeInverse_tendsto line 63
  10. theorem OAI.DefocusingNLS.spectralGaugeRobin_tendsto line 71