OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialComplexConvergence.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform convergence of the actual complex amplitude-phase jets.

  1. theorem OAI.DefocusingNLS.radial_uniform_complex_product line 12
  2. theorem OAI.DefocusingNLS.radial_uniform_ofReal line 20
  3. theorem OAI.DefocusingNLS.radial_uniform_phase_exp line 25
  4. theorem OAI.DefocusingNLS.radial_polar_jet_uniform line 38