auto-task(quantumCapacity): minimize imports of QuantumInfo/Capacity/Capacity.lean

[jstoobysmith]

Summary

Trims the import list of QuantumInfo/Capacity/Capacity.lean down to what the file
actually needs. Only import lines were touched — no code, docstrings, or
declarations were changed.

This file is a leaf module (no other file imports
QuantumInfo.Capacity.Capacity), so there is no downstream breakage and no
imports needed to be added anywhere.

Imports removed (9)

public import QuantumInfo.Entropy.SSA
public import QuantumInfo.Entropy.Relative
public import QuantumInfo.Entropy.DPI
public import QuantumInfo.Channels.Bundled
public import QuantumInfo.Channels.CPTP
public import QuantumInfo.Channels.Dual
public import QuantumInfo.Channels.MatrixMap
public import QuantumInfo.Channels.Unbundled
public import QuantumInfo.States.Mixed.TraceDistance

Why these are safe to remove

• Channels.Bundled, Channels.CPTP, Channels.Dual, Channels.MatrixMap,
  Channels.Unbundled — the CPTPMap operations used here (compose,
  compose_assoc, id, piProd, piProd_id, piProd_comp, ofEquiv, …) are
  still in scope because both retained imports, QuantumInfo.Entropy.VonNeumann
  and QuantumInfo.States.Mixed.Fidelity, transitively import all five Channels
  modules.
• Entropy.SSA, Entropy.Relative, Entropy.DPI — the file references nothing
  specific to strong subadditivity, relative entropy, or the data-processing
  inequality. These modules were only acting as carriers for
  QuantumInfo.Entropy.VonNeumann (which defines coherentInfo, the one entropy
  symbol the file uses); VonNeumann is now imported directly.
• States.Mixed.TraceDistance — unused; the approximation definitions in this
  file are stated in terms of fidelity, not trace distance.

Imports kept (4)

Each directly provides a symbol the file uses to state or prove its declarations:

• Mathlib.Analysis.SpecialFunctions.Log.Base — Real.logb
• QuantumInfo.Entropy.VonNeumann — coherentInfo
• QuantumInfo.States.Mixed.Fidelity — fidelity, fidelity_self_eq_one
• Physlib.Meta.Sorry — the @[sorryful] attribute

Verification

lake build completes successfully (9107 jobs, no errors). The only warnings on the
file are the three pre-existing declaration uses 'sorry' warnings from the
@[sorryful] theorems that were already present — no new sorry, no new axioms, and
no new errors or warnings were introduced.

[github-actions]

Thank you for this PR, which will now be reviewed. If submitting to ./Physlib or ./QuantumInfo, please see our review guidelines if you are not familiar with the process. You should expect a back and forth with a reviewer before your PR is merged. See also that link for how to add appropriate labels to your PR. The PR will also go through a number of automated checks. You can learn more about these here, including how to run them locally.

If you are submitting to ./PhyslibAlpha there will be a lighter review process, though your PR must still pass the automated checks.

If you want to bring attention to this PR, please write a message on this thread of the Lean Zulip.

Important: If a reviewer adds an awaiting-author label to your PR, once you have addressed the review comments, please remove that label by adding a comment with -awaiting-author. This helps us keep track of reviews.