OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousSpectralGrowthEquation.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Applying polynomial derivative growth to the actual circular equation

  1. def OAI.DefocusingNLS.homogeneousSpectralState line 14
  2. theorem OAI.DefocusingNLS.homogeneousSpectralState_zero line 18
  3. theorem OAI.DefocusingNLS.homogeneousSpectralState_one line 20
  4. theorem OAI.DefocusingNLS.homogeneousSpectralState_two line 22
  5. theorem OAI.DefocusingNLS.homogeneousSpectralState_three line 24
  6. theorem OAI.DefocusingNLS.homogeneousSpectralState_four line 26
  7. theorem OAI.DefocusingNLS.homogeneousSpectralState_five line 28
  8. def OAI.DefocusingNLS.homogeneousSpectralDifferential line 31
  9. theorem OAI.DefocusingNLS.homogeneousSpectralDifferential_eval line 57
  10. theorem OAI.DefocusingNLS.homogeneousSpectralState_hasDerivAt line 79
  11. theorem OAI.DefocusingNLS.homogeneousSpectralState_bound line 100
  12. theorem OAI.DefocusingNLS.homogeneousSpectral_derivatives_exponential_bound line 111
  13. def OAI.DefocusingNLS.homogeneousCoupledSpectralField line 128
  14. theorem OAI.DefocusingNLS.homogeneousCoupledSpectralField_contDiff line 133
  15. theorem OAI.DefocusingNLS.homogeneousSpectral_solution_contDiffOn line 146