OAI/Analysis/IrrationalRotation/PrescribedAngleConditional.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The spectral-radius hypothesis and its consequences for prescribed irrational angles.

  1. structure OAI.Invariant233.PublishedRotationSpectralInput line 17
  2. theorem OAI.Invariant233.PublishedRotationSpectralInput.normQuasinilpotent line 21
  3. theorem OAI.Invariant233.Results.prescribed_irrational_counterexample_of_published_spectral_input line 34