OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousHarmonicTransport.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Angular averaging of radial transport and multiplication

These identities use the actual physical realization. They complement the radial Laplacian identity with the other terms of the linearized generator.

  1. theorem OAI.DefocusingNLS.continuous_harmonicSphere line 18
  2. theorem OAI.DefocusingNLS.memLp_star_harmonicSphere line 30
  3. theorem OAI.DefocusingNLS.homogeneous_harmonic_projection line 37
  4. theorem OAI.DefocusingNLS.homogeneous_harmonic_contDiff line 46
  5. theorem OAI.DefocusingNLS.homogeneous_harmonic_smul line 55
  6. theorem OAI.DefocusingNLS.homogeneous_harmonic_deriv line 66
  7. theorem OAI.DefocusingNLS.homogeneous_harmonic_euler line 79
  8. theorem OAI.DefocusingNLS.harmonicAngularCoefficient_radial_mul line 92
  9. theorem OAI.DefocusingNLS.integrable_harmonicSphere_product line 103
  10. theorem OAI.DefocusingNLS.harmonicAngularCoefficient_four line 110