OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralFreeRobinPropagation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Propagation of the outer outgoing Robin plane through the free radial equation.

  1. theorem OAI.DefocusingNLS.spectralFreePhysicalPairField_smul line 12
  2. theorem OAI.DefocusingNLS.spectralFreePhysicalPairField_add line 28
  3. theorem OAI.DefocusingNLS.spectralFreeCombination_hasDerivAt line 34
  4. theorem OAI.DefocusingNLS.spectralFreeRobin_propagation_general line 47
  5. theorem OAI.DefocusingNLS.spectralFreeRobin_propagation line 68
  6. theorem OAI.DefocusingNLS.spectralFreeCoreBoundary_linear line 85
  7. theorem OAI.DefocusingNLS.matchingColumn_coefficients_zero line 92