OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousSpectralPower.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Geometric power decay from the spectral radius

This quantitative form of Gelfand's formula is used for the restricted time-step operator after its exceptional spectral subspace is removed.

  1. theorem OAI.DefocusingNLS.operator_powers_le_geometric line 20
  2. theorem OAI.DefocusingNLS.operator_powers_decay_of_spectralRadius_lt_one line 49