Quantum Information Apps
Exercise PLAN-419
primary source nl only. Current content-bound mathematical second pass accepted. No new Lean verification is claimed for this NL view.
Assumptions and conventions
Question
In the de Finetti proof one meets the average squared fidelity integral dphi p(phi) F(tilde-phi, phi^{tensor k})^2 = R, where R = [ (m+d-1)!/m! ] / [ (k+m+d-1)!/(k+m)! ] simplifies to the ratio of two products of (d-1) consecutive integers, R = [(m+1)(m+2)...(m+d-1)] / [(k+m+1)(k+m+2)...(k+m+d-1)]. Prove the chain of lower bounds R >= ((m+1)/(k+m+1))^{d-1} = (1 - k/(k+m+1))^{d-1} >= 1 - k(d-1)/(k+m+1) >= 1 - kd/m. State the elementary inequalities used and where each applies.
Hint: mathematical route
The de Finetti fidelity ratio factorizes into d-1 increasing terms, so replacing them by the smallest, applying Bernoulli, and a crude comparison yields the clean lower bound 1 - kd/m.
- R is a product of d-1 factors, minimized termwise by the j=1 factor.
- Bernoulli's inequality lowers the power to a linear bound.
- A crude denominator/numerator comparison gives R >= 1 - kd/m.
Reference solution
Write R as a product of d-1 factors, pairing the j-th numerator term (m+j) with the j-th denominator term (k+m+j) for j = 1, ..., d-1: R = prod_{j=1}^{d-1} (m+j)/(k+m+j). Each factor (m+j)/(k+m+j) is an increasing function of j (as j grows the ratio (m+j)/(k+m+j) increases toward 1), so the smallest factor is the one at j = 1, namely (m+1)/(k+m+1). Replacing every factor by this smallest one gives the first bound R >= ((m+1)/(k+m+1))^{d-1}; this uses only that each factor is at least the j=1 factor. Rewrite (m+1)/(k+m+1) = 1 - k/(k+m+1), which is a number in [0,1] since 0 <= k/(k+m+1) <= 1. Apply Bernoulli's inequality (1 - a)^p >= 1 - p a for a in [0,1] and p = d-1 >= 0: ((1 - k/(k+m+1))^{d-1} >= 1 - (d-1) k/(k+m+1). That is the second bound. Finally, since k+m+1 >= m and d-1 <= d, we have (d-1) k/(k+m+1) <= d k/m (replacing the denominator by the smaller m only increases the fraction, and d-1 by d only increases the numerator factor), hence 1 - (d-1)k/(k+m+1) >= 1 - kd/m. Chaining the three steps gives R >= 1 - kd/m. The elementary inequalities used are: (1) monotonicity of each factor in j to replace by the minimal factor; (2) Bernoulli's inequality (1-a)^p >= 1 - pa; (3) the crude comparison (d-1)/(k+m+1) <= d/m. This is exactly the fidelity lower bound 1 - kd/m that feeds, via Fuchs-van de Graaf and Jensen, into the de Finetti trace-distance bound sqrt(kd/(n-k)) with m = n - k.
Assessment rubric
- Factorizes R = prod_{j=1}^{d-1} (m+j)/(k+m+j) and replaces each factor by the minimal j=1 factor to get R >= ((m+1)/(k+m+1))^{d-1} (1 weight)
- Rewrites (m+1)/(k+m+1) = 1 - k/(k+m+1) in [0,1] (1 weight)
- Applies Bernoulli (1-a)^{d-1} >= 1 - (d-1)a to get 1 - (d-1)k/(k+m+1) (1 weight)
- Uses (d-1)/(k+m+1) <= d/m to reach R >= 1 - kd/m and ties it to the de Finetti bound with m = n - k (1 weight)
Graph-grounded prerequisites
These are support/source anchors, not an automatically extracted theorem-dependency proof.
- Matrix analysis (frozen curriculum anchor; see graph registry)
- Probability and sampling (frozen curriculum anchor; see graph registry)
Lean view and evidence boundary
No aligned Lean view has been admitted for this native core in this textbook checkpoint. This is not a claim that the underlying mathematics lacks a formal proof. Contributions must preserve this exact target contract and split.
Sources and provenance
- website/research/sources.json
leditzky-2025-repth-qit
Source SHA-256:9f85f45f20ed5a46931ad0dec3b94ee09748bc56e39fae29b0aefe910440b0ae· MIT metadata only - Primary source
Contract: cf3b3e8068b77f61f195406c0239bd3a4c62a221a769e3241a1fd3ff437e30ea
Item digest: 59c6bcb17e48756c7d9d42d22d2a2834b87745b5f7064cefc99fb1b53aa8b270
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 3. This is not measured graph distance or model difficulty.