- Boxes
- definitions
- Ellipses
- theorems and lemmas
- Blue border
- the statement of this result is ready to be formalized; all prerequisites are done
- Orange border
- the statement of this result is not ready to be formalized; the blueprint needs more work
- Blue background
- the proof of this result is ready to be formalized; all prerequisites are done
- Green border
- the statement of this result is formalized
- Green background
- the proof of this result is formalized
- Dark green background
- the proof of this result and all its ancestors are formalized
- Dark green border
- this is in Mathlib
Let \(S\) be a finite set. For each \(s\in S\), let \(\Omega _s\) be a measurable space and let \(I_s\) and \(L_s\) be two index sets. Given complex functions \(c_s(a,b;\cdot )\) on \(\Omega _s\), define the coefficient associated with multiindices \(i\in \prod _s I_s\) and \(l\in \prod _s L_s\) by
where \(\omega \in \prod _s\Omega _s\). The ket and bra index sets may have different cardinalities. This is the coefficient product in [ Ope26a , Equation (5.11) ] .
Let \(T\) be a finite set of source positions, with \(N=|T|\). For every real \(a\),
For \(k{\gt}0\), the summand \(Q^{|U|}k^{-|U|/2}\) equals \((Q/\sqrt{k})^{|U|}\), so its sum is \((1+Q/\sqrt{k})^N-1\). The sum is zero when \(T\) is empty. If \(a\geq 0\), then \((1+a)^N-1\leq e^{Na}-1\). For \(0\leq \epsilon \leq 1\), one also has \(e^{\epsilon /8}-1\leq \epsilon /4\). These are the scalar estimates in [ Ope26a , Equation (5.19) and the following paragraph ] .
- CompressionSampling.sum_nonempty_subsets_pow
- CompressionSampling.sum_nonempty_subsets_weight
- CompressionSampling.inverse_half_power
- CompressionSampling.sum_nonempty_subsets_rpow
- CompressionSampling.zero_slots_error
- CompressionSampling.binomial_error_le_exp
- CompressionSampling.exp_eighth_sub_one_le_quarter
Let \(T\) be finite and let \(F_U\) be integrable functions with values in a normed additive group, indexed by the nonempty subsets of \(T\). If \(\int \lVert F_U\rVert \, d\mu \leq a^{|U|}\) for each such \(U\), then
More generally, the same bound holds for an integrable real error \(e\) whenever \(e\leq \sum _U e_U\) pointwise and the integrable real correction estimates satisfy \(\int e_U\, d\mu \leq a^{|U|}\). In particular, for \(k{\gt}0\), per-subset bounds \(\int \lVert F_U\rVert \, d\mu \leq Q^{|U|}k^{-|U|/2}\) give the right side \((1+Q/\sqrt{k})^{|T|}-1\). This is the summation implication in [ Ope26a , Equation (5.19) ] .
Let \(Z\) be an arbitrary rectangular matrix. Let \(K\) and \(\widetilde K\) be contractions from its respective output and input spaces into a common physical space tensored with a discard space. Then
The same norm bound holds for left and right contractions alone, and partial trace alone cannot increase the trace norm. This is [ Ope26a , Equation (5.13) ] .
Let \(S\) be finite. At each slot \(s\), let \(A_s,C_s\) be finite endpoint supports with nonnegative weights \(\lambda _s,\mu _s\). Take independent standard circular complex Gaussian coordinates \(g^{(j,s)}_{ac}\), with \(\mathbb E|g^{(j,s)}_{ac}|^2=1\), and independent Gaussian factors across slots. For \(k{\gt}0\), define
The product law is a probability measure, and both \(z_{il}\) and every conjugate pair product are integrable. Set \(p_i=\prod _s\lambda _s(i_s^1)\lambda _s(i_s^2)\) and \(\widetilde p_l=\prod _s\mu _s(l_s^1)\mu _s(l_s^2)\). Their covariance is (5). If each endpoint weight list sums to one, both product weight lists also sum to one. For nonempty \(S\), \(\mathbb E z_{il}=0\). These are the actual independent coefficients in [ Ope26a , Equations (5.7), (5.8), and (5.11) ] .
- QICLean.ComplexGaussian.pairedProductProbability
- QICLean.ComplexGaussian.pairedProductProbability_nonneg
- QICLean.ComplexGaussian.sum_pairedProductProbability_eq_one
- QICLean.ComplexGaussian.independentDensityLaw
- QICLean.ComplexGaussian.independentDensityLawIsProbabilityMeasure
- QICLean.ComplexGaussian.independentDensityCoefficient
- QICLean.ComplexGaussian.integrable_independentDensityCoefficient
- QICLean.ComplexGaussian.integrable_independentDensityCoefficient_mul_conj
- QICLean.ComplexGaussian.integral_independentDensityCoefficient_mul_conj
- QICLean.ComplexGaussian.integral_independentDensityCoefficient_eq_zero
Let \(J\) be finite, let \(\mu \) be a measure, and let \(z_j\) be complex functions with every product \(z_i\overline{z_j}\) integrable. Suppose \(\int z_i\overline{z_j}\, d\mu =\delta _{ij}v_i\), where \(v_i\in \mathbb {R}\). For complex numbers \(a_j\) and arbitrary rectangular matrices \(A_j\),
Both squared integrands are integrable. If \(\mu \) is a probability measure, then
These are the moment calculation and expectation estimate used in [ Ope26a , Equations (5.16) and (5.18) ] .
Let each \(\mu _s\) be a \(\sigma \)-finite measure on \(\Omega _s\), and set \(\mu =\bigotimes _{s\in S}\mu _s\). For complex functions \(f_s,g_s\),
If each \(f_s\overline{g_s}\) is integrable, the product integrand is integrable. In particular, pair-product integrability of the slot coefficients implies pair-product integrability of \(z_{il}\).
For nonnegative diagonal probability matrices \(\tau ,\widetilde\tau \) and an arbitrary rectangular matrix \(W\) of compatible size,
More generally, let \(R,\widetilde R\) be arbitrary positive semidefinite trace-one matrices and let \(O\) be a rectangular contraction between their spaces. Then
Zero eigenvalues and different input dimensions are allowed. These are the comparisons in [ Ope26a , Equations (5.15) and (5.17) ] .
Let \(\mu \) be a probability measure, let \(Q\geq 0\) and \(0{\lt}\epsilon \leq 1\), and choose \(k\) by (15). Suppose \(e\) is integrable and \(\mathbb E e\leq (1+Q/\sqrt{k})^N-1\). If a condition \(V\) holds almost surely, there exists \(\omega \) satisfying \(V(\omega )\) and \(e(\omega )\leq \epsilon /2\). In particular, this conclusion applies with \(e=\lVert \sum _{\varnothing \neq U\subseteq T}F_U\rVert \) and \(N=|T|\), provided each \(F_U\) is integrable and \(\mathbb E\lVert F_U\rVert \leq Q^{|U|}k^{-|U|/2}\). This is the realization step after [ Ope26a , Equation (5.19) ] .
For \(N\in \mathbb {N}\) and real \(Q,\epsilon \), put
Then \(k{\gt}0\) and \((8NQ/\epsilon )^2\leq k\leq (8NQ/\epsilon )^2+2\). If \(Q\geq 0\) and \(0{\lt}\epsilon \leq 1\), every positive integer \(k\) satisfying \((8NQ/\epsilon )^2\leq k\) obeys
For \(N{\gt}0\), the sample-count hypothesis gives \(Q/\sqrt{k}\leq \epsilon /(8N)\). This is an explicit integer choice for the sample count in [ Ope26a , Theorem 5.2, paragraph following Equation (5.19) ] .
On the product of \(\sigma \)-finite measures, suppose the individual slot moments satisfy
Then the full multiindices have diagonal moments:
In particular, on probability spaces, let \(k\) be a positive integer and let \(p_s,q_s\) be nonnegative weights. Put \(p_i=\prod _s p_s(i_s)\) and \(\widetilde p_l=\prod _s q_s(l_s)\). If \(\nu _s(a,b)=k^{-1}\sqrt{p_s(a)q_s(b)}\), then
For finite \(I_s\), the equalities \(\sum _a p_s(a)=1\) imply \(\sum _i\prod _s p_s(i_s)=1\); this normalization identity requires no sign condition on the individual weights. The weighted moment formula is [ Ope26a , Equation (5.11) ] .
For a complex rectangular matrix \(A\), let \(\lVert A\rVert _1\) be the sum of its singular values. Equivalently, \(\lVert A\rVert _1=\sum _j\sqrt{\lambda _j(A^\dagger A)}\); for square matrices this is the trace norm. Every rectangular contraction \(U\) of the same size satisfies \(|\operatorname{tr}(A^\dagger U)|\leq \lVert A\rVert _1\), and some such \(U\) satisfies \(\operatorname{tr}(A^\dagger U)=\lVert A\rVert _1\). This is the trace-norm duality used in [ Ope26a , Equation (5.13) ] .
For complex matrices \(A\) of size \(m\times p\) and \(B\) of size \(n\times p\), \(\lVert AB^T\rVert _1\leq \lVert A\rVert _2\lVert B\rVert _2\). No dimension enters. This is the bound used in the proof of [ Ope26a , Lemma 6.2 ] .
Let \(M\) be a complex rectangular matrix and \(k\geq 0\). There is an orthonormal family \(f_1,\dots ,f_r\) with \(r\leq k\) whose orthogonal projector \(P=\sum _i f_if_i^\dagger \) satisfies \((k+1)\lVert M-MP\rVert _2^2\leq \lVert M\rVert _1^2\). If the domain of \(M\) has dimension at most \(k\), then \(M=MP\). No dimension enters the estimate. This is the singular-value tail estimate in the proof of [ Ope26a , Lemma 6.2 ] .