OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralWeightedCoreWeak.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Compact observations of the weighted constrained inverse converge for weak inputs.

  1. theorem OAI.DefocusingNLS.spectralHarmonicObservation_weakSequence line 11
  2. theorem OAI.DefocusingNLS.spectralHarmonicFirstValue_weakSequence line 21
  3. theorem OAI.DefocusingNLS.spectralHarmonicCoreInverse_weak_input line 33