QuantumComputinglib learn · inspect · formalize
Checked on this commit 4,524 public declarations commit 4e2c5b2c0be5 Build record

Quantum Information / Quantum Information Apps

Quantum Information Apps

Exercise PLAN-412

intermediate · proof · test_public

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

      Let d_sym = dim Sym^n(C^d) = binom(n + d - 1, n). Prove the integral formula Pi_sym = d_sym integral dphi |phi><phi|^{tensor n}, where Pi_sym is the orthogonal projector onto the symmetric subspace Sym^n(C^d) and dphi is the Haar-induced normalized measure on pure states of C^d. Structure the proof as: (i) the operator X = integral dphi |phi><phi|^{tensor n} is supported on Sym^n; (ii) X commutes with (and is in fact fixed by conjugation under) U^{tensor n} for all U; (iii) Schur's lemma forces X proportional to Pi_sym; (iv) the trace fixes the constant.

      Hint: mathematical route

      Averaging |phi><phi|^{tensor n} over Haar pure states gives, by irreducibility of U^{tensor n} on Sym^n and Schur's lemma, exactly (1/d_sym) Pi_sym, with the constant fixed by the trace.

      1. The product-power states span Sym^n, so X is supported there.
      2. Left-invariance of the Haar measure makes X invariant under U^{tensor n}.
      3. Schur's lemma plus the trace fix X = (1/d_sym) Pi_sym.
      Reference solution

      (i) Each |phi><phi|^{tensor n} = (|phi>^{tensor n})(<phi|^{tensor n}) is a rank-one operator whose range is spanned by the symmetric vector |phi>^{tensor n} in Sym^n(C^d); since such vectors |phi>^{tensor n} span Sym^n (every symmetric tensor is a combination of such product powers), every |phi><phi|^{tensor n} annihilates any vector orthogonal to Sym^n. Averaging preserves this, so X is fully supported on Sym^n (X = Pi_sym X Pi_sym). (ii) For any U in U_d, conjugating gives U^{tensor n} X (U^dagger)^{tensor n} = integral dphi (U|phi><phi|U^dagger)^{tensor n}. Parametrize the measure as |phi> = V|phi_0> with V Haar on U_d; then U|phi> = (UV)|phi_0>, and by the left-invariance of the Haar measure the integral over V equals the integral over UV, so U^{tensor n} X (U^dagger)^{tensor n} = X. Thus X is invariant under conjugation by U^{tensor n} for all U; equivalently X commutes with the representation U^{tensor n} restricted to its support Sym^n. (iii) By a theorem (proved earlier in the course) the representation U -> U^{tensor n} restricted to Sym^n(C^d) is irreducible. An operator on an irreducible representation that commutes with the whole representation is, by Schur's lemma, a scalar multiple of the identity on that irreducible space; since X is supported on Sym^n and commutes there with U^{tensor n}, we get X = c Pi_sym for some constant c >= 0 (nonnegative because X is positive). (iv) Take traces: tr X = integral dphi tr(|phi><phi|^{tensor n}) = integral dphi 1 = 1 by normalization of the measure, while tr(c Pi_sym) = c dim Sym^n = c d_sym. Hence c = 1/d_sym, i.e. X = (1/d_sym) Pi_sym, equivalently Pi_sym = d_sym integral dphi |phi><phi|^{tensor n}, as claimed.

      Assessment rubric
      1. Shows X = integral dphi |phi><phi|^{tensor n} is supported on Sym^n because the |phi>^{tensor n} span Sym^n (1 weight)
      2. Proves U^{tensor n}-invariance of X using the parametrization |phi> = V|phi_0> and left-invariance of the Haar measure (1 weight)
      3. Invokes irreducibility of U^{tensor n} on Sym^n and Schur's lemma to get X = c Pi_sym (1 weight)
      4. Fixes c = 1/d_sym by taking traces (tr X = 1, tr Pi_sym = d_sym), giving Pi_sym = d_sym integral dphi |phi><phi|^{tensor n} (1 weight)

      Graph-grounded prerequisites

      These are support/source anchors, not an automatically extracted theorem-dependency proof.

      • Operator and semigroup theory (frozen curriculum anchor; see graph registry)
      • Probability and sampling (frozen curriculum anchor; see graph registry)
      • Harmonic analysis (frozen curriculum anchor; see graph registry)
      • Tensor networks (frozen curriculum anchor; see graph registry)

      Download the shared core 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.

      Read the Lean track and existing diagnostic warmups

      Sources and provenance

      Contract: 74e100f2da1752b912928419b8cbd09087749e3243f8db78a724cb3b198123d9

      Item digest: b4183f8ccfaf78c2989b2a41175edfa0d6bd452671cb1a5d0c767b53fdac475d

      Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

      Authored support steps: 3. This is not measured graph distance or model difficulty.