OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralPolynomialMixedDerivative.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Mixed derivatives of the finite outgoing expansion commute by the finite coefficient formula, before adding the weighted correction.

  1. theorem OAI.DefocusingNLS.circularPolynomialJet_time_hasDerivAt line 11
  2. theorem OAI.DefocusingNLS.circularPolynomialJet_mixed_hasDerivAt line 19