Operator-norm estimates for the enumeration of strategies

The analytic input of lem:value-lower-approx, in the L2 operator norm on matrices (Matrix.Norms.L2Operator), with vectors x : n → ℂ measured in ℂ^n as toLp 2 x:

• IsSkewHermitian.norm_inv_one_add_le: ‖(1 + S)⁻¹‖ ≤ 1 for skew-Hermitian S;
• norm_cayley_sub_cayley_le: the Cayley transform is 2-Lipschitz on skew-Hermitian matrices;
• l2_opNorm_le_card_mul_of_entry_le: an entrywise bound δ gives ‖E‖ ≤ n δ, which is what rounding a matrix entrywise costs;
• unitaries and projections have norm at most 1 (norm_le_one_of_mem_unitaryGroup, norm_le_one_of_isProj).

Vectors of ℂ^n

theorem MIPRE.ValueApprox.inner_toLp_toLp {n : Type u_1} [Fintype n] (x y : n → ℂ) : inner ℂ (WithLp.toLp 2 x) (WithLp.toLp 2 y) = star x ⬝ᵥ y

theorem MIPRE.ValueApprox.norm_sq_toLp {n : Type u_1} [Fintype n] (x : n → ℂ) : ‖WithLp.toLp 2 x‖ ^ 2 = (star x ⬝ᵥ x).re

theorem MIPRE.ValueApprox.dotProduct_star_self_eq_ofReal {n : Type u_1} [Fintype n] (x : n → ℂ) : star x ⬝ᵥ x = ↑(‖WithLp.toLp 2 x‖ ^ 2)

⟨x, x⟩ = ‖x‖², as a complex number.

theorem MIPRE.ValueApprox.norm_toLp_eq_one_of_dotProduct {n : Type u_1} [Fintype n] {x : n → ℂ} (h : star x ⬝ᵥ x = 1) : ‖WithLp.toLp 2 x‖ = 1

theorem MIPRE.ValueApprox.norm_toLp_mulVec_le {n : Type u_1} [Fintype n] [DecidableEq n] (A : Matrix n n ℂ) (x : n → ℂ) : ‖WithLp.toLp 2 (A.mulVec x)‖ ≤ ‖A‖ * ‖WithLp.toLp 2 x‖

theorem MIPRE.ValueApprox.norm_dotProduct_mulVec_le {n : Type u_1} [Fintype n] [DecidableEq n] (T : Matrix n n ℂ) (x y : n → ℂ) : ‖star x ⬝ᵥ T.mulVec y‖ ≤ ‖T‖ * ‖WithLp.toLp 2 x‖ * ‖WithLp.toLp 2 y‖

|⟨x, T y⟩| ≤ ‖T‖ ‖x‖ ‖y‖.

theorem MIPRE.ValueApprox.l2_opNorm_le_of_forall {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℂ} {c : ℝ} (hc : 0 ≤ c) (h : ∀ (x : n → ℂ), ‖WithLp.toLp 2 (A.mulVec x)‖ ≤ c * ‖WithLp.toLp 2 x‖) : ‖A‖ ≤ c

The operator norm is bounded by any uniform bound on vectors.

Skew-Hermitian matrices and the Cayley transform

theorem MIPRE.ValueApprox.IsSkewHermitian.norm_toLp_le_norm_toLp_one_add_mulVec {n : Type u_1} [Fintype n] [DecidableEq n] {S : Matrix n n ℂ} (hS : IsSkewHermitian S) (x : n → ℂ) : ‖WithLp.toLp 2 x‖ ≤ ‖WithLp.toLp 2 ((1 + S).mulVec x)‖

‖(1 + S) x‖ ≥ ‖x‖ for skew-Hermitian S: the cross term of ‖x + S x‖² vanishes.

theorem MIPRE.ValueApprox.IsSkewHermitian.norm_inv_one_add_le {n : Type u_1} [Fintype n] [DecidableEq n] {S : Matrix n n ℂ} (hS : IsSkewHermitian S) : ‖(1 + S)⁻¹‖ ≤ 1

‖(1 + S)⁻¹‖ ≤ 1 for skew-Hermitian S.

theorem MIPRE.ValueApprox.cayley_sub_cayley {n : Type u_1} [Fintype n] [DecidableEq n] {S T : Matrix n n ℂ} (hS : IsSkewHermitian S) (hT : IsSkewHermitian T) : cayley S - cayley T = 2 • ((1 + S)⁻¹ * (T - S) * (1 + T)⁻¹)

The resolvent identity for the Cayley transform.

theorem MIPRE.ValueApprox.norm_cayley_sub_cayley_le {n : Type u_1} [Fintype n] [DecidableEq n] {S T : Matrix n n ℂ} (hS : IsSkewHermitian S) (hT : IsSkewHermitian T) : ‖cayley S - cayley T‖ ≤ 2 * ‖S - T‖

The Cayley transform is 2-Lipschitz on skew-Hermitian matrices.

Entrywise bounds

theorem MIPRE.ValueApprox.l2_opNorm_le_card_mul_of_entry_le {n : Type u_1} [Fintype n] [DecidableEq n] {E : Matrix n n ℂ} {δ : ℝ} (hδ : 0 ≤ δ) (h : ∀ (i j : n), ‖E i j‖ ≤ δ) : ‖E‖ ≤ ↑(Fintype.card n) * δ

An entrywise bound gives an operator-norm bound with a factor of the dimension.

Vectors with small entries

theorem MIPRE.ValueApprox.norm_toLp_le_card_mul_of_forall_norm_le {n : Type u_1} [Fintype n] {v : n → ℂ} {δ : ℝ} (hδ : 0 ≤ δ) (h : ∀ (i : n), ‖v i‖ ≤ δ) : ‖WithLp.toLp 2 v‖ ≤ ↑(Fintype.card n) * δ

An entrywise bound on a vector gives a norm bound with a factor of the dimension.

theorem MIPRE.ValueApprox.norm_toLp_normalize_sub_le {n : Type u_1} [Fintype n] (u ψ : n → ℂ) (hψ : ‖WithLp.toLp 2 ψ‖ = 1) (hu : u ≠ 0) : ‖WithLp.toLp 2 ((↑‖WithLp.toLp 2 u‖)⁻¹ • u - ψ)‖ ≤ 2 * ‖WithLp.toLp 2 (u - ψ)‖

Normalizing a vector u near a unit vector ψ keeps it near ψ: ‖u / ‖u‖ - ψ‖ ≤ 2 ‖u - ψ‖.

Kronecker products

theorem MIPRE.ValueApprox.kronecker_one_mulVec {n : Type u_1} [Fintype n] [DecidableEq n] {m : Type u_2} [Fintype m] (X : Matrix m m ℂ) (v : m × n → ℂ) (i : m) (j : n) : (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) X 1).mulVec v (i, j) = X.mulVec (fun (k : m) => v (k, j)) i

theorem MIPRE.ValueApprox.one_kronecker_mulVec {n : Type u_1} [Fintype n] {m : Type u_2} [Fintype m] [DecidableEq m] (Y : Matrix n n ℂ) (v : m × n → ℂ) (i : m) (j : n) : (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 Y).mulVec v (i, j) = Y.mulVec (fun (l : n) => v (i, l)) j

theorem MIPRE.ValueApprox.norm_kronecker_one_le {n : Type u_1} [Fintype n] [DecidableEq n] {m : Type u_2} [Fintype m] [DecidableEq m] (X : Matrix m m ℂ) : ‖Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) X 1‖ ≤ ‖X‖

‖X ⊗ 1‖ ≤ ‖X‖: X ⊗ 1 acts as X on each column.

theorem MIPRE.ValueApprox.norm_one_kronecker_le {n : Type u_1} [Fintype n] [DecidableEq n] {m : Type u_2} [Fintype m] [DecidableEq m] (Y : Matrix n n ℂ) : ‖Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 Y‖ ≤ ‖Y‖

‖1 ⊗ Y‖ ≤ ‖Y‖: 1 ⊗ Y acts as Y on each row.

theorem MIPRE.ValueApprox.norm_kronecker_le {n : Type u_1} [Fintype n] [DecidableEq n] {m : Type u_2} [Fintype m] [DecidableEq m] (X : Matrix m m ℂ) (Y : Matrix n n ℂ) : ‖Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) X Y‖ ≤ ‖X‖ * ‖Y‖

The L2 operator norm is submultiplicative for Kronecker products.

Conjugation

theorem MIPRE.ValueApprox.norm_mul_mul_conjTranspose_sub_le {n : Type u_1} [Fintype n] [DecidableEq n] {V W P : Matrix n n ℂ} (hV : ‖V‖ ≤ 1) (hW : ‖W‖ ≤ 1) (hP : ‖P‖ ≤ 1) : ‖V * P * V.conjTranspose - W * P * W.conjTranspose‖ ≤ 2 * ‖V - W‖

V P Vᴴ is 2-Lipschitz in V when all matrices have norm at most 1.

Unitaries and projections

theorem MIPRE.ValueApprox.norm_toLp_mulVec_eq_of_mem_unitaryGroup {n : Type u_1} [Fintype n] [DecidableEq n] {U : Matrix n n ℂ} (hU : U ∈ Matrix.unitaryGroup n ℂ) (x : n → ℂ) : ‖WithLp.toLp 2 (U.mulVec x)‖ = ‖WithLp.toLp 2 x‖

theorem MIPRE.ValueApprox.norm_le_one_of_mem_unitaryGroup {n : Type u_1} [Fintype n] [DecidableEq n] {U : Matrix n n ℂ} (hU : U ∈ Matrix.unitaryGroup n ℂ) : ‖U‖ ≤ 1

theorem MIPRE.ValueApprox.norm_le_one_of_isProj {n : Type u_1} [Fintype n] [DecidableEq n] {P : Matrix n n ℂ} (hP : P.conjTranspose = P) (hPP : P * P = P) : ‖P‖ ≤ 1

A self-adjoint idempotent has norm at most 1.

theorem MIPRE.ValueApprox.IsPVM.norm_le_one {n : Type u_1} [Fintype n] [DecidableEq n] {A : Type u_2} [Fintype A] {M : A → Matrix n n ℂ} (hM : IsPVM M) (a : A) : ‖M a‖ ≤ 1