Avila-Jitomirskaya Ten Martini Problem

ten_martini_problem

Submitter: Kim Morrison.

Notes: The theorem constructs the almost Mathieu operator as an actual Mathlib continuous linear endomorphism of `lp (fun _ : Int => Complex) 2`; `IsAlmostMathieuOperator` fixes it by the standard coordinate formula, rather than hiding it in trusted spectral scaffolding. For irrational frequency `alpha`, nonzero coupling `lambda`, and arbitrary phase `theta`, its complex spectrum is asserted to be nonempty, compact, perfect, and totally disconnected, i.e. a Cantor set. Including operator existence in the conclusion prevents vacuity through an uninhabited formula predicate.

Source: A. Avila and S. Jitomirskaya, 'The Ten Martini Problem', Ann. of Math. 170 (2009), 303-342, https://doi.org/10.4007/annals.2009.170.303.

Informal solution: Aubry duality relates the almost Mathieu operators at couplings `lambda` and `1/lambda`, so the proof can combine localization information in one regime with reducibility information in the dual regime. Avila and Jitomirskaya establish nonperturbative localization estimates and analyze the associated quasiperiodic `SL(2,R)` cocycles. For every irrational frequency and nonzero coupling, these estimates rule out intervals in the spectrum and also rule out isolated spectral points. Standard self-adjoint spectral theory supplies nonemptiness and compactness. Thus the spectrum is compact and perfect with no nontrivial connected subsets, which is precisely the Cantor-set conclusion stated in Lean.

theorem declaration uses `sorry`ten_martini_problem (α coupling θ : ℝ)
    (hα : Irrational α) (hcoupling : coupling ≠ 0) :
    ∃ H : LeanEval.Analysis.TenMartini.EllTwo →L[ℂ] LeanEval.Analysis.TenMartini.EllTwo,
      LeanEval.Analysis.TenMartini.IsAlmostMathieuOperator α coupling θ H ∧
        (spectrum ℂ H).Nonempty ∧
        IsCompact (spectrum ℂ H) ∧
        Perfect (spectrum ℂ H) ∧
        IsTotallyDisconnected (spectrum ℂ H) := byα:ℝcoupling:ℝθ:ℝhα:Irrational αhcoupling:coupling ≠ 0⊢ ∃ H,
  IsAlmostMathieuOperator α coupling θ H ∧
    (spectrum ℂ H).Nonempty ∧ IsCompact (spectrum ℂ H) ∧ Perfect (spectrum ℂ H) ∧ IsTotallyDisconnected (spectrum ℂ H)
  sorryAll goals completed! 🐙

Solved by

Not yet solved.