OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralLowerOrderOperator.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The lower-order weak operator from volume and boundary observations. The two real multipliers are the mass and weighted radial flux. The boundary operator contains the outgoing Robin matrix and its transport correction.

  1. def OAI.DefocusingNLS.spectralPairSkew line 15
  2. def OAI.DefocusingNLS.spectralPairRiesz line 19
  3. theorem OAI.DefocusingNLS.spectralPairRiesz_inner line 28
  4. def OAI.DefocusingNLS.spectralHarmonicPairValues line 39
  5. def OAI.DefocusingNLS.spectralHarmonicPairDerivatives line 43
  6. def OAI.DefocusingNLS.spectralHarmonicPairTraces line 51
  7. def OAI.DefocusingNLS.spectralWeakOperator line 55
  8. def OAI.DefocusingNLS.spectralWeakPairing line 69
  9. theorem OAI.DefocusingNLS.spectralWeakOperator_inner line 80
  10. def OAI.DefocusingNLS.spectralLowerOrderOperator line 96
  11. theorem OAI.DefocusingNLS.spectralLowerOrderOperator_inner line 104