OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousHarmonicBounded.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniformly bounded radial channels from the actual Cā‚€ realization

A smooth angular test is bounded on the unit sphere. Thus the radial channel of a Cā‚€ physical function is uniformly bounded at every radius.

  1. theorem OAI.DefocusingNLS.harmonicAngularCoefficient_bounded line 19
  2. theorem OAI.DefocusingNLS.homogeneous_harmonic_channel_bounded line 41