OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralRemoteInverseJets.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Fixed-order bounds for inversion of the remote changes of variables. The same constant works for every path whose jets obey the stated bounds.

  1. def OAI.DefocusingNLS.spectralRemoteInverseMap line 16
  2. theorem OAI.DefocusingNLS.spectralRemoteInverseMap_smooth line 19
  3. theorem OAI.DefocusingNLS.spectralRemote_inverse_jet_bound line 32