OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralLiouvilleNormPositive.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Positivity of the actual Liouville Cauchy-state weight away from a turn.

  1. theorem OAI.DefocusingNLS.spectralLiouville_norm_weight_pos line 9