OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralRadialEnergySpace.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The completed radial H¹ energy space on the fixed twelve-dimensional ball.

The two ambient coordinates are the radial value and its weak derivative. Taking the closure of smooth jets keeps their compatibility in the completion.

  1. abbrev OAI.DefocusingNLS.SpectralRadialL2 line 18
  2. abbrev OAI.DefocusingNLS.SpectralRadialJetSpace line 20
  3. def OAI.DefocusingNLS.spectralRadialSmoothValue line 23
  4. def OAI.DefocusingNLS.spectralRadialSmoothJet line 28
  5. def OAI.DefocusingNLS.spectralRadialEnergySubspace line 34
  6. abbrev OAI.DefocusingNLS.SpectralRadialEnergy line 38
  7. instance OAI.DefocusingNLS.spectralRadialEnergy_complete line 40
  8. def OAI.DefocusingNLS.spectralRadialValue line 43
  9. def OAI.DefocusingNLS.spectralRadialDerivative line 48
  10. theorem OAI.DefocusingNLS.spectralRadialEnergy_norm_sq line 53
  11. def OAI.DefocusingNLS.spectralRadialSmoothEmbedding line 59
  12. theorem OAI.DefocusingNLS.spectralRadialSmoothEmbedding_dense line 64
  13. theorem OAI.DefocusingNLS.spectralRadialSmoothEmbedding_value line 73
  14. theorem OAI.DefocusingNLS.spectralRadialSmoothEmbedding_derivative line 76