Approximation of Quantum Gates using Lattices

Reference: arxiv/1506.05785 On the Approximation of Quantum Gates using Lattices by Alec Greene and Steven Damelin

def EuclideanSpace.«termℤ⁴» : Lean.ParserDescr

The integer lattice ℤ⁴ as the ℤ-span of the standard basis in 4-dimensional Euclidean space.

Equations

• EuclideanSpace.«termℤ⁴» = Lean.ParserDescr.node `EuclideanSpace.«termℤ⁴» 1024 (Lean.ParserDescr.symbol "ℤ⁴")

theorem Arxiv.«1506.05785».conjecture_3_4 : ∃ δ ∈ Set.Ioo 0 1, ∀ (a : EuclideanSpace ℝ (Fin 4)), ‖a‖ = 1 → ∃ (b : ↥(Submodule.span ℤ (Set.range ⇑(PiLp.basisFun 2 ℝ (Fin 4))))), ∃ k > 0, ‖b‖ = 5 ^ k ∧ 1 - 5 ^ (-↑k / (2 - δ)) ≤ inner a (‖b‖⁻¹ • ↑b)

Conjecture 3.4 There exists $0 < \delta < 1$ such that for any $a \in \mathbb{S}^3$, there exists $b \in \mathbb{Z}^4$ and $k \in \mathbb{Z}$ such that $\|b\| = 5^k$ and $\langle a, \frac{b}{\|b\|} \rangle \geq 1 - 5^{-\frac{k}{2 - \delta}}.$