Research proof index

Let $H$ be a subgroup of $G \times G'$. Then there exists a subgroup $H_0$ of $G$, a subgroup $H_1$ of $G'$, and a homomorphism $\phi: G \to G'$ such that $H := \{ (x, \phi(x) + y): x \in H_0, y \in H_1 \}.$ In particular, $|H| = |H_0| |H_1|$.

Sub-lemma for Step 1b: the conj of H_hat by σ^{−γ} simplifies to (ρ.M.conj (σ^γ).mat)^{α−1}. This uses σ^{−γ} · σ^γ = identity (on support) to cancel the outer σ^γ factors.

If A ≥ 0 and A ≤ 1, then each eigenvalue of A is in [0, 1].

Hermitian trace Hölder inequality: for PSD A, B and conjugate exponents p, q > 1, ⟪A, B⟫ ≤ Tr[A^p]^(1/p) * Tr[B^q]^(1/q).

The operator norm of the conjugate transpose is equal to the operator norm. -/ theorem Matrix.opNorm_conjTranspose_eq_opNorm {m n : Type*} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] (A : Matrix m n 𝕜) : Matrix.opNorm Aᴴ = Matrix.opNorm A := by unfold Matrix.opNorm rw [← ContinuousLinearMap.adjoint.norm_map (toEuclideanLin A).toContinuousLine...

If for all i, ker(σs i) ≤ ker(ρs i), then ker(∑ w i • σs i) ≤ ker(∑ w i • ρs i), provided all weights are nonneg and all matrices are PSD.