Gaussian rationals, and matrices with entries in a subfield

The enumeration of lem:value-lower-approx ranges over strategies whose matrices and state have entries in the Gaussian rationals ℚ(i). This file provides

• GaussianRat, the subfield of ℂ of numbers with rational real and imaginary parts, closed under complex conjugation (GaussianRat.star_mem) and dense (GaussianRat.exists_norm_sub_le);
• EntriesIn K M, "all entries of M lie in the subfield K", with its closure under the ring operations, conjugate transposition, Kronecker products, determinants, adjugates, inverses and hence the Cayley transform (EntriesIn.cayley) — which is how the enumeration reaches exact unitaries;
• entrywise rounding to Gaussian rationals, for matrices (exists_entriesIn_norm_sub_le), vectors (exists_forall_mem_norm_sub_le) and, preserving skew-Hermiticity by re-symmetrizing the rounded matrix, for skew-Hermitian matrices (IsSkewHermitian.exists_entriesIn_norm_sub_le).

The Gaussian rationals

def MIPRE.ValueApprox.GaussianRat : Subfield ℂ

The Gaussian rationals ℚ(i), as a subfield of ℂ: the numbers whose real and imaginary parts are rational.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.ValueApprox.GaussianRat.mem_iff {z : ℂ} : z ∈ GaussianRat ↔ (∃ (a : ℚ), ↑a = z.re) ∧ ∃ (b : ℚ), ↑b = z.im

theorem MIPRE.ValueApprox.GaussianRat.ratCast_mem (q : ℚ) : ↑q ∈ GaussianRat

theorem MIPRE.ValueApprox.GaussianRat.I_mem : Complex.I ∈ GaussianRat

theorem MIPRE.ValueApprox.GaussianRat.star_mem {z : ℂ} (hz : z ∈ GaussianRat) : star z ∈ GaussianRat

theorem MIPRE.ValueApprox.GaussianRat.mem_iff_exists_eq {z : ℂ} : z ∈ GaussianRat ↔ ∃ (a : ℚ) (b : ℚ), z = ↑a + ↑b * Complex.I

theorem MIPRE.ValueApprox.GaussianRat.exists_norm_sub_le (z : ℂ) {η : ℝ} (hη : 0 < η) : ∃ w ∈ GaussianRat, ‖z - w‖ ≤ η

Every complex number is within η of a Gaussian rational.

Matrices with entries in a subfield

def MIPRE.ValueApprox.EntriesIn (K : Subfield ℂ) {m : Type u_1} {n : Type u_2} (M : Matrix m n ℂ) : Prop

All entries of M lie in the subfield K.

Equations

• MIPRE.ValueApprox.EntriesIn K M = ∀ (i : m) (j : n), M i j ∈ K

theorem MIPRE.ValueApprox.EntriesIn.zero {K : Subfield ℂ} {m : Type u_1} {n : Type u_2} : EntriesIn K 0

theorem MIPRE.ValueApprox.EntriesIn.add {K : Subfield ℂ} {m : Type u_1} {n : Type u_2} {M N : Matrix m n ℂ} (hM : EntriesIn K M) (hN : EntriesIn K N) : EntriesIn K (M + N)

theorem MIPRE.ValueApprox.EntriesIn.sub {K : Subfield ℂ} {m : Type u_1} {n : Type u_2} {M N : Matrix m n ℂ} (hM : EntriesIn K M) (hN : EntriesIn K N) : EntriesIn K (M - N)

theorem MIPRE.ValueApprox.EntriesIn.smul {K : Subfield ℂ} {m : Type u_1} {n : Type u_2} {M : Matrix m n ℂ} {c : ℂ} (hc : c ∈ K) (hM : EntriesIn K M) : EntriesIn K (c • M)

theorem MIPRE.ValueApprox.EntriesIn.sum {K : Subfield ℂ} {m : Type u_1} {n : Type u_2} {ι : Type u_4} (s : Finset ι) {f : ι → Matrix m n ℂ} (hf : ∀ i ∈ s, EntriesIn K (f i)) : EntriesIn K (∑ i ∈ s, f i)

theorem MIPRE.ValueApprox.EntriesIn.conjTranspose {K : Subfield ℂ} {m : Type u_1} {n : Type u_2} {M : Matrix m n ℂ} (hK : ∀ z ∈ K, star z ∈ K) (hM : EntriesIn K M) : EntriesIn K M.conjTranspose

theorem MIPRE.ValueApprox.EntriesIn.mul {K : Subfield ℂ} {m : Type u_1} {n : Type u_2} {p : Type u_3} {M : Matrix m n ℂ} [Fintype n] {N : Matrix n p ℂ} (hM : EntriesIn K M) (hN : EntriesIn K N) : EntriesIn K (M * N)

theorem MIPRE.ValueApprox.EntriesIn.one {K : Subfield ℂ} {n : Type u_2} [DecidableEq n] : EntriesIn K 1

theorem MIPRE.ValueApprox.EntriesIn.patternProj {K : Subfield ℂ} {n : Type u_2} {A : Type u_4} [DecidableEq n] [DecidableEq A] (r : n → A) (a : A) : EntriesIn K (ValueApprox.patternProj r a)

theorem MIPRE.ValueApprox.EntriesIn.det_mem {K : Subfield ℂ} {n : Type u_2} [Fintype n] [DecidableEq n] {M : Matrix n n ℂ} (hM : EntriesIn K M) : M.det ∈ K

theorem MIPRE.ValueApprox.EntriesIn.adjugate {K : Subfield ℂ} {n : Type u_2} [Fintype n] [DecidableEq n] {M : Matrix n n ℂ} (hM : EntriesIn K M) : EntriesIn K M.adjugate

theorem MIPRE.ValueApprox.EntriesIn.inv {K : Subfield ℂ} {n : Type u_2} [Fintype n] [DecidableEq n] {M : Matrix n n ℂ} (hM : EntriesIn K M) : EntriesIn K M⁻¹

theorem MIPRE.ValueApprox.EntriesIn.cayley {K : Subfield ℂ} {n : Type u_2} [Fintype n] [DecidableEq n] {M : Matrix n n ℂ} (hM : EntriesIn K M) : EntriesIn K (ValueApprox.cayley M)

The Cayley transform of a matrix with entries in K has entries in K.

Rounding to Gaussian rationals

theorem MIPRE.ValueApprox.exists_entriesIn_norm_sub_le {m : Type u_1} {n : Type u_2} (M : Matrix m n ℂ) {η : ℝ} (hη : 0 < η) : ∃ (R : Matrix m n ℂ), EntriesIn GaussianRat R ∧ ∀ (i : m) (j : n), ‖M i j - R i j‖ ≤ η

Entrywise rounding of a matrix to Gaussian rationals.

theorem MIPRE.ValueApprox.exists_forall_mem_norm_sub_le {n : Type u_1} (v : n → ℂ) {η : ℝ} (hη : 0 < η) : ∃ (w : n → ℂ), (∀ (i : n), w i ∈ GaussianRat) ∧ ∀ (i : n), ‖v i - w i‖ ≤ η

Entrywise rounding of a vector to Gaussian rationals.

theorem MIPRE.ValueApprox.IsSkewHermitian.exists_entriesIn_norm_sub_le {n : Type u_1} {S : Matrix n n ℂ} (hS : IsSkewHermitian S) {η : ℝ} (hη : 0 < η) : ∃ (T : Matrix n n ℂ), IsSkewHermitian T ∧ EntriesIn GaussianRat T ∧ ∀ (i j : n), ‖S i j - T i j‖ ≤ η

Rounding a skew-Hermitian matrix S entrywise to R, then re-symmetrizing to (R - Rᴴ) / 2, gives a skew-Hermitian Gaussian-rational matrix within the same entrywise distance of S.