OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingSobolevNonlinearity.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The fixed-weight identification preserves the actual nonlinearity

Both models represent the same Fourier coefficients. Consequently the change of norm intertwines multiplication, conjugation and the Schrödinger generator.

  1. theorem OAI.DefocusingNLS.coefficient_injective line 17

    Distinct definitions of this name: OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingNonlinearityTransport.lean:17 (different declaration text). Qualify references as OAI.DefocusingNLS.coefficient_injective@path.

  2. theorem OAI.DefocusingNLS.expandingToSobolev_product line 27
  3. theorem OAI.DefocusingNLS.expandingToSobolev_conjugate line 41
  4. theorem OAI.DefocusingNLS.expandingToSobolev_oddPower line 50
  5. theorem OAI.DefocusingNLS.expandingToSobolev_lowerInclusion line 60
  6. theorem OAI.DefocusingNLS.expandingToSobolev_lowerGenerator line 68
  7. theorem OAI.DefocusingNLS.sobolevTorusFunction_expandingToSobolev line 76