OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralRadialPoincare.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A fixed-ball radial Poincare estimate with its boundary trace follows from the Hardy identity at constant weight.

  1. theorem OAI.DefocusingNLS.spectralComplex_radialHardy line 13
  2. theorem OAI.DefocusingNLS.spectralRadial_weightedPoincare line 31