Almost Mathieu operator

AbbreviationThe sequence space \(\ell^2(\mathbb{Z})\)#✓fully proved

We write \(\ell^2(\mathbb{Z})\) for the Hilbert space of square-summable sequences \((u_n)_{n \in \mathbb{Z}}\) of complex numbers.

abbrev EllTwo : Type := lp (fun _ : ℤ => ℂ) 2

Used by 2

Used byAlmost Mathieu operator · Ten Martini theorem (Avila–Jitomirskaya)

DefinitionAlmost Mathieu operator#✓fully proved

Let \(\alpha\), \(\lambda\) and \(\theta\) be real numbers. A bounded complex-linear operator \(H\) on \(\ell^2(\mathbb{Z})\) is an almost Mathieu operator with frequency \(\alpha\), coupling \(\lambda\) and phase \(\theta\) when, for every \(u \in \ell^2(\mathbb{Z})\) and every \(n \in \mathbb{Z}\),

\[(Hu)(n) = u(n+1) + u(n-1) + 2\lambda \cos(2\pi(\theta + n\alpha))\, u(n).\]

def IsAlmostMathieuOperator (α coupling θ : ℝ) (H : EllTwo →L[ℂ] EllTwo) : Prop :=
  ∀ (u : EllTwo) (n : ℤ),
    H u n =
      u (n + 1) + u (n - 1) +
        ((2 * coupling * Real.cos (2 * Real.pi * (θ + (n : ℝ) * α) : ℝ) : ℂ) * u n)

Uses 1 · Used by 1

Statement usesThe sequence space \(\ell^2(\mathbb{Z})\)

Used byTen Martini theorem (Avila–Jitomirskaya)

TheoremTen Martini theorem (Avila–Jitomirskaya)#●ready to prove

Let \(\alpha\), \(\lambda\) and \(\theta\) be real numbers with \(\alpha\) irrational and \(\lambda \neq 0\). Then there is an almost Mathieu operator \(H\) on \(\ell^2(\mathbb{Z})\) with frequency \(\alpha\), coupling \(\lambda\) and phase \(\theta\), and the spectrum of \(H\) is nonempty, compact, perfect and totally disconnected, that is, a Cantor set.

public theorem_wanted ten_martini_problem (α coupling θ : ℝ)
    (hα : Irrational α) (hcoupling : coupling ≠ 0) :
    ∃ H : EllTwo →L[ℂ] EllTwo,
      IsAlmostMathieuOperator α coupling θ H ∧
        (spectrum ℂ H).Nonempty ∧
        IsCompact (spectrum ℂ H) ∧
        Perfect (spectrum ℂ H) ∧
        IsTotallyDisconnected (spectrum ℂ H)

Sources

• 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. Problem ten_martini_problem of the lean-eval benchmark.

Uses 2

Statement usesThe sequence space \(\ell^2(\mathbb{Z})\) · Almost Mathieu operator

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.