OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/UnitTorusCoefficients.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Recovering the physical coefficients from the continuous Fourier series

  1. def OAI.DefocusingNLS.unitTorusCoefficient line 19
  2. theorem OAI.DefocusingNLS.unitTorusCoefficient_apply line 23
  3. theorem OAI.DefocusingNLS.unitTorusCoefficient_mFourier line 30
  4. def OAI.DefocusingNLS.expandingUnitTorusTerm line 35
  5. theorem OAI.DefocusingNLS.summable_expandingUnitTorusTerm line 39
  6. def OAI.DefocusingNLS.expandingUnitTorusFunction line 46
  7. theorem OAI.DefocusingNLS.expandingUnitTorusFunction_coefficient line 49
  8. theorem OAI.DefocusingNLS.expandingUnitTorusFunction_projection line 72
  9. theorem OAI.DefocusingNLS.expandingFourierCoefficient_eq_of_torus_eq line 91