OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralGaugeObservationLine.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exterior physical values and regular core continuation determine the entire compact observation, including its boundary traces.

  1. theorem OAI.DefocusingNLS.spectralHarmonicRepresentative_sub_smul line 11
  2. theorem OAI.DefocusingNLS.spectralHarmonicObservation_zero_of_core_exterior line 19
  3. theorem OAI.DefocusingNLS.spectralHarmonicObservation_eq_of_gauge_values line 54