Skip to content

auto-task(Capacity): clear QuantumInfo/Capacity/Capacity.lean from the linter exemption list #1370

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
jstoobysmith merged 2 commits into from
Jul 6, 2026
+198 −35
Merged

auto-task(Capacity): clear QuantumInfo/Capacity/Capacity.lean from the linter exemption list #1370

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
a0eda30
auto-task(Capacity): clear QuantumInfo/Capacity/Capacity.lean from th…
doxtor6 Jul 5, 2026
26b92b3
Remove 'HasTimeDimension' definition from API-map
jstoobysmith Jul 6, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
84 changes: 84 additions & 0 deletions Physlib/SpaceAndTime/Time/API-map.yaml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,84 @@
version: v0.1

Title: Time

Overview: |
The key data structure is `Time`, a structure with a single field `val : ℝ`
representing time with a given (but arbitrary) choice of units, origin and
orientation — the version of time most often used in non-relativistic physics,
forming a 1d real inner-product space. The API also contains the time
derivative `∂ₜ` of functions on `Time`, and the related types `TimeMan`,
`TimeTransMan` and `TimeUnit`, versions of time with fewer choices made,
related to `Time` via a choice of units or origin.

ParentAPIs:
- "Space (Physlib/SpaceAndTime/Space)"
- "Lorentz vectors (Physlib/Relativity/Tensors/RealTensor/Vector)"

References: []

Requirements:

- description: "The key data structure `Time` (a structure with a single field `val : ℝ`, representing time with an arbitrary but fixed choice of units and origin) is defined."
done: true
location: "Physlib/SpaceAndTime/Time/Basic.lean (Time)"

- description: "The API contains an instance of a vector space (module) on `Time`, with an orthonormal basis and continuous linear/isometric equivalences to `ℝ`."
done: true
location: "Physlib/SpaceAndTime/Time/Basic.lean (AddCommGroup Time, Module ℝ Time, basis : OrthonormalBasis (Fin 1) ℝ Time, toRealCLM, toRealCLE, toRealLIE)"

- description: "The API contains an ordering on `Time`."
done: true
location: "Physlib/SpaceAndTime/Time/Basic.lean (LE Time, PartialOrder Time)"

- description: "The API contains a norm on `Time`, and an inner product making it a 1d real inner-product space."
done: true
location: "Physlib/SpaceAndTime/Time/Basic.lean (Norm Time, NormedAddCommGroup Time, NormedSpace ℝ Time, InnerProductSpace ℝ Time)"

- description: "The API contains a measure-theoretic structure on `Time` (a Borel measurable space, with the volume measure equal to the Haar measure associated with the basis)."
done: true
location: "Physlib/SpaceAndTime/Time/Basic.lean (MeasurableSpace Time, BorelSpace Time, volume_eq_basis_addHaar, val_measurePreserving)"

- description: "The API contains the derivatives of functions from `Time` to normed spaces, with linearity, constant-function, quotient and smoothness lemmas, and compatibility with Euclidean and Lorentz-vector components."
done: true
location: "Physlib/SpaceAndTime/Time/Derivatives.lean (Time.deriv, notation ∂ₜ, deriv_smul, deriv_div, deriv_const, deriv_contDiff_of_contDiff, deriv_euclid, deriv_lorentzVector)"

- description: "The API contains the derivatives of functions from `Time` to manifolds."
done: true
location: "Physlib/SpaceAndTime/Time/Derivatives.lean (Time.manifoldDeriv, deriv_eq_manifoldDeriv)"

- description: "The API contains the product rule and commutation with transpose for the time derivative of square-matrix-valued functions of time."
done: true
location: "Physlib/SpaceAndTime/Time/MatrixDerivatives.lean (Time.deriv_matrix_mul, Time.deriv_matrix_transpose)"

- description: "The API contains the time manifold `TimeMan` (time with no structure except an orientation), with topology, charted-space and manifold instances and the diffeomorphism to `ℝ`."
done: true
location: "Physlib/SpaceAndTime/Time/TimeMan.lean (TimeMan, ChartedSpace ℝ TimeMan, IsManifold 𝓘(ℝ, ℝ) ω TimeMan, valDiffeomorphism)"

- description: "The API contains the type `TimeUnit` of choices of time unit (equivalent to the positive reals), with ratios of units, scaling, and concrete units (seconds through weeks) and their relations."
done: true
location: "Physlib/SpaceAndTime/Time/TimeUnit.lean (TimeUnit, HDiv TimeUnit TimeUnit ℝ≥0, scale, seconds, hours_div_seconds)"

- description: "The API contains the time manifold `TimeTransMan` with a transitive action of `ℝ`, an orientation, unit-dependent differences and translations (`diff`, `addTime`, `neg`), and the homeomorphism `toTime` to `Time` given a choice of origin and unit."
done: true
location: "Physlib/SpaceAndTime/Time/TimeTransMan.lean (TimeTransMan, AddAction ℝ TimeTransMan, diff, addTime, neg, toTime)"

- description: "The API shall contain an action of the translation group on `Time`."
done: false
location: N/A

- description: "The API shall contain derivatives of distributions from `Time` to normed spaces."
done: false
location: N/A

- description: "The API shall contain derivatives of distributions from `Time` to manifolds."
done: false
location: N/A

- description: "The API shall show that the homeomorphism `toTime` from `TimeTransMan` to `Time` is a diffeomorphism."
done: false
location: N/A

- description: "The API shall show that translationally-invariant metrics on `TimeTransMan` are in one-to-one correspondence with the positive reals (choices of `TimeUnit`)."
done: false
location: N/A
148 changes: 114 additions & 34 deletions QuantumInfo/Capacity/Capacity.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,39 +20,60 @@ public import QuantumInfo.States.Mixed.Fidelity
public import QuantumInfo.States.Mixed.TraceDistance
public import Physlib.Meta.Sorry

/-! # Quantum Capacity
/-!
# Quantum Capacity

This focuses on defining and proving theorems about the quantum capacity, the maximum asymptotic rate at which quantum information can be coherently transmitted. The precise definition is not consistent in the literature, see [Capacity_doc](./QuantumInfo/Finite/Capacity_doc.html) for a note on what has been used and how that was used to arrive at the following definition:
## i. Overview

This file focuses on defining and proving theorems about the quantum capacity, the maximum
asymptotic rate at which quantum information can be coherently transmitted through a quantum
channel. The precise definition is not consistent in the literature, see
`QuantumInfo/Capacity/Capacity_doc.lean` for a note on what has been used and how that was used
to arrive at the following definition:

1. A channel A `Emulates` another channel B if there are D and E such that D∘A∘E = B.
2. A channel A `εApproximates` channel B (of the same dimensions) if the for every state ρ, the fidelity F(A(ρ), B(ρ)) is at least 1-ε.
3. A channel A `AchievesRate` R:ℝ if for every ε>0, n copies of A emulates some channel B such that log2(dimout(B))/n ≥ R, and that B is εApproximately the identity.
4. The `quantumCapacity` of the channel A is the supremum of the achievable rates, i.e. `sSup { R : ℝ | AchievesRate A R }`.
2. A channel A `εApproximates` channel B (of the same dimensions) if for every state ρ, the
fidelity F(A(ρ), B(ρ)) is at least 1-ε.
3. A channel A `AchievesRate` R:ℝ if for every ε>0, n copies of A emulates some channel B such
that log2(dimout(B))/n ≥ R, and that B is εApproximately the identity.
4. The `quantumCapacity` of the channel A is the supremum of the achievable rates, i.e.
`sSup { R : ℝ | AchievesRate A R }`.

## ii. Key results

The most basic facts:
* `emulates_self`: Every channel emulates itself.
* `emulates_trans`: If A emulates B and B emulates C, then A emulates C. (That is, emulation is an ordering.)
* `εApproximates A B ε` is equivalent to the existence of some δ (depending ε and dims(A)) so that |A-B| has diamond norm at most δ, and δ→0 as ε→0.
* `emulates_trans`: If A emulates B and B emulates C, then A emulates C. (That is, emulation
is an ordering.)
* `εApproximates A B ε` is equivalent to the existence of some δ (depending on ε and dims(A))
so that |A-B| has diamond norm at most δ, and δ→0 as ε→0.
* `achievesRate_0`: Every channel out of a nonempty space achievesRate 0. So, in that case,
the set of achievable rates is Nonempty.
* If a channel achievesRate R₁, it also every achievesRate R₂ every R₂ ≤ R₁, i.e. it is an interval extending left towards -∞. Achievable rates are `¬BddBelow`.
* `bddAbove_achievesRate`: A channel C : dimX → dimY cannot achievesRate R with `R > log2(min(dimX, dimY))`. Thus, the interval is `BddAbove`.
* If a channel achievesRate R₁, it also achievesRate every R₂ ≤ R₁, i.e. it is an interval
extending left towards -∞. Achievable rates are `¬BddBelow`.
* `bddAbove_achievesRate`: A channel C : dimX → dimY cannot achievesRate R with
`R > log2(min(dimX, dimY))`. Thus, the interval is `BddAbove`.

The nice lemmas we would want:
* Capacity of a replacement channel is zero.
* Capacity of an identity channel is `log2(D)`.
* Capacity is superadditive under tensor products. (That is, at least additive. Showing that it isn't _exactly_ additive, unlike classical capacity which is additive, is a much harder task.)
* Capacity is superadditive under tensor products. (That is, at least additive. Showing that
it isn't _exactly_ additive, unlike classical capacity which is additive, is a much harder
task.)
* Capacity of a kth tensor power is exactly k times the capacity of the original channel.
* Capacity does not decrease under tensor sums.
* Capacity does not increase under composition.

Then, we should show that our definition is equivalent to some above. Most, except (3), should be not too hard to prove.
Then, we should show that our definition is equivalent to some above. Most, except (3), should
be not too hard to prove.

Then the LSD theorem establishes that the single-copy coherent information is a lower bound. This is stated in `coherentInfo_le_quantumCapacity`. The corollary, that the n-copy coherent information converges to the capacity, is `quantumCapacity_eq_piProd_coherentInfo`.
Then the LSD theorem establishes that the single-copy coherent information is a lower bound.
This is stated in `coherentInfo_le_quantumCapacity`. The corollary, that the n-copy coherent
information converges to the capacity, is `quantumCapacity_eq_piProd_coherentInfo`.

# TODO

The only notion of "capacity" here currently is "quantum capacity" in the usual sense. But there are several non-equal capacities relevant to quantum channels, see e.g. [Watrous's notes](https://cs.uwaterloo.ca/~watrous/TQI/TQI.8.pdf) for a list:
TODO: The only notion of "capacity" here currently is "quantum capacity" in the usual sense.
But there are several non-equal capacities relevant to quantum channels, see e.g. [Watrous's
notes](https://cs.uwaterloo.ca/~watrous/TQI/TQI.8.pdf) for a list:
* Quantum capacity (`quantumCapacity`)
* Quantum 1-shot capacity
* Entanglement-assisted classical capacity
Expand All @@ -62,15 +83,35 @@ The only notion of "capacity" here currently is "quantum capacity" in the usual
* Entanglement-assisted quantum capacity
* One- and two-way distillable entanglement

And other important theorems like superdense coding, nonadditivity, superactivation
And other important theorems like superdense coding, nonadditivity, superactivation.

## iii. Table of contents

- A. Basic definitions
- B. Emulation between channels
- C. Approximation between channels
- D. Achievable rates
- E. The quantum capacity

## iv. References

* [Watrous's notes](https://cs.uwaterloo.ca/~watrous/TQI/TQI.8.pdf), Chapter 8 of
*The Theory of Quantum Information*.
-/

@[expose] public section

namespace CPTPMap

variable {d₁ d₂ d₃ d₄ d₅ d₆ : Type*}
variable [Fintype d₁] [Fintype d₂] [Fintype d₃] [Fintype d₄] [Fintype d₅] [Fintype d₆] [DecidableEq d₁] [DecidableEq d₂]
variable [Fintype d₁] [Fintype d₂] [Fintype d₃] [Fintype d₄] [Fintype d₅] [Fintype d₆]
variable [DecidableEq d₁] [DecidableEq d₂]

/-!

## A. Basic definitions

-/

variable [DecidableEq d₃] [DecidableEq d₄] in
/--
Expand All @@ -80,13 +121,15 @@ def Emulates (Λ₁ : CPTPMap d₁ d₂) (Λ₂ : CPTPMap d₃ d₄) : Prop :=
∃ (E : CPTPMap d₃ d₁) (D : CPTPMap d₂ d₄), D.compose (Λ₁.compose E) = Λ₂

/--
A channel A `εApproximates` channel B of the same dimensions if the for every state ρ, the fidelity F(A(ρ), B(ρ)) is at least 1-ε.
A channel A `εApproximates` channel B of the same dimensions if for every state ρ, the
fidelity F(A(ρ), B(ρ)) is at least 1-ε.
-/
def εApproximates (A B : CPTPMap d₁ d₂) (ε : ℝ) : Prop :=
∀ (ρ : MState d₁), (A ρ).fidelity (B ρ) ≥ 1-ε

/--
A channel A `AchievesRate` R:ℝ if for every ε>0, some n copies of A emulates a channel B such that log2(dimout(B))/n ≥ R, and that B εApproximates the identity channel.
A channel A `AchievesRate` R:ℝ if for every ε>0, some n copies of A emulates a channel B such
that log2(dimout(B))/n ≥ R, and that B εApproximates the identity channel.
-/
def AchievesRate (A : CPTPMap d₁ d₂) (R : ℝ) : Prop :=
∀ ε : ℝ, ε > 0 →
Expand All @@ -95,9 +138,18 @@ def AchievesRate (A : CPTPMap d₁ d₂) (R : ℝ) : Prop :=
Real.logb 2 dimB ≥ R*n ∧
B.εApproximates CPTPMap.id ε

/-- The quantum capacity of a channel A: the supremum of all rates R such that
`A.AchievesRate R`, i.e. the maximum asymptotic rate at which quantum information can be
coherently transmitted through the channel. -/
noncomputable def quantumCapacity (A : CPTPMap d₁ d₂) : ℝ :=
sSup { R : ℝ | AchievesRate A R }

/-!

## B. Emulation between channels

-/

section emulates
variable [DecidableEq d₃] [DecidableEq d₄] [DecidableEq d₅]

Expand All @@ -109,13 +161,19 @@ theorem emulates_self (Λ : CPTPMap d₁ d₂) : Λ.Emulates Λ :=
/-- If a quantum channel A emulates B, and B emulates C, then A emulates C. -/
@[trans]
theorem emulates_trans (Λ₁ : CPTPMap d₁ d₂) (Λ₂ : CPTPMap d₃ d₄) (Λ₃ : CPTPMap d₅ d₆)
(h₁₂ : Λ₁.Emulates Λ₂) (h₂₃ : Λ₂.Emulates Λ₃) : Λ₁.Emulates Λ₃ := by
(h₁₂ : Λ₁.Emulates Λ₂) (h₂₃ : Λ₂.Emulates Λ₃) : Λ₁.Emulates Λ₃ := by
obtain ⟨E₁, D₁, hED₁⟩ := h₁₂
obtain ⟨E₂, D₂, hED₂⟩ := h₂₃
exact ⟨E₁.compose E₂, D₂.compose D₁, by classical simp [← hED₁, ← hED₂, compose_assoc]⟩

end emulates

/-!

## C. Approximation between channels

-/

section εApproximates

/-- Every quantum channel perfectly approximates itself, that is, `εApproximates` with `ε = 0`. -/
Expand All @@ -129,6 +187,12 @@ theorem εApproximates_monotone {A B : CPTPMap d₁ d₂} {ε₀ : ℝ} (h : A.

end εApproximates

/-!

## D. Achievable rates

-/

section AchievesRate

/-- Every quantum channel out of a nonempty space achieves at least a rate of zero. -/
Expand All @@ -139,22 +203,24 @@ theorem achievesRate_0 (Λ : CPTPMap d₁ d₂) [Nonempty d₁] : Λ.AchievesRat
εApproximates_monotone (εApproximates_self (id (dIn := Fin 1))) hε.le

/-- The identity channel on D dimensional space achieves a rate of log2(D). -/
theorem id_achievesRate_log_dim : (id (dIn := d₁)).AchievesRate (Real.logb 2 (Fintype.card d₁)) := by
theorem id_achievesRate_log_dim :
(id (dIn := d₁)).AchievesRate (Real.logb 2 (Fintype.card d₁)) := by
intro ε hε
use 1, zero_lt_one, Fintype.card d₁, id
constructor
· --piProd of id's is id, then use emulates_self up to equivalence
rw [show (fun (_ : Fin 1) ↦ id (dIn := d₁)) = (fun _ ↦ id) from rfl, piProd_id]
exact let σ := Fintype.equivFinOfCardEq (by simp +decide : Fintype.card (Fin 1 → d₁) = Fintype.card d₁)
exact let σ := Fintype.equivFinOfCardEq (by simp +decide :
Fintype.card (Fin 1 → d₁) = Fintype.card d₁)
⟨ofEquiv σ.symm, ofEquiv σ, by ext1; simp⟩
constructor
· norm_num
· exact εApproximates_monotone (εApproximates_self id) hε.le

/-- A channel cannot achieve a rate greater than log2(D), where D is the input dimension. -/
@[sorryful]
theorem not_achievesRate_gt_log_dim_in (Λ : CPTPMap d₁ d₂) {R : ℝ} (hR : Real.logb 2 (Fintype.card d₁) < R) :
¬Λ.AchievesRate R := by
theorem not_achievesRate_gt_log_dim_in (Λ : CPTPMap d₁ d₂) {R : ℝ}
(hR : Real.logb 2 (Fintype.card d₁) < R) : ¬Λ.AchievesRate R := by
sorry

noncomputable section AristotleLemmas
Expand All @@ -163,16 +229,21 @@ end AristotleLemmas

/-- A channel cannot achieve a rate greater than log2(D), where D is the output dimension. -/
@[sorryful]
theorem not_achievesRate_gt_log_dim_out (Λ : CPTPMap d₁ d₂) {R : ℝ} (hR : Real.logb 2 (Fintype.card d₂) < R): ¬Λ.AchievesRate R := by
theorem not_achievesRate_gt_log_dim_out (Λ : CPTPMap d₁ d₂) {R : ℝ}
(hR : Real.logb 2 (Fintype.card d₂) < R) : ¬Λ.AchievesRate R := by
intro h;
-- We show that the identity channel on the output space `d₂` emulates `Λ`. Since capacity is monotonic under emulation, `Q(Λ) ≤ Q(id_{d₂})`.
-- We show that the identity channel on the output space `d₂` emulates `Λ`. Since capacity
-- is monotonic under emulation, `Q(Λ) ≤ Q(id_{d₂})`.
have h_emulate : (CPTPMap.id (dIn := d₂)).Emulates Λ := by
exact ⟨Λ, CPTPMap.id, by simp⟩
-- If `Λ` achieves rate `R`, then `id_{d₂}` achieves rate `R`. This follows because if `Λ^{\otimes n}` emulates `B`, and `id^{\otimes n}` emulates `Λ^{\otimes n}` (by functoriality of tensor product), then `id^{\otimes n}` emulates `B`.
-- If `Λ` achieves rate `R`, then `id_{d₂}` achieves rate `R`. This follows because if
-- `Λ^{\otimes n}` emulates `B`, and `id^{\otimes n}` emulates `Λ^{\otimes n}` (by
-- functoriality of tensor product), then `id^{\otimes n}` emulates `B`.
have h_id_achieves : (CPTPMap.id (dIn := d₂)).AchievesRate R := by
intro ε hε_pos
obtain ⟨n, hn, dimB, B, hB_emulate, hB_rate, hB_approx⟩ := h ε hε_pos
have h_id_emulate : (CPTPMap.piProd (fun (_ : Fin n) => CPTPMap.id (dIn := d₂))).Emulates B := by
have h_id_emulate :
(CPTPMap.piProd (fun (_ : Fin n) => CPTPMap.id (dIn := d₂))).Emulates B := by
rw [piProd_id]
obtain ⟨E, D, hD⟩ := h_emulate
exact emulates_trans _ _ _ ⟨piProd fun _ => E, piProd fun _ => D,
Expand All @@ -191,6 +262,12 @@ theorem bddAbove_achievesRate (Λ : CPTPMap d₁ d₂) : BddAbove {R | Λ.Achiev

end AchievesRate

/-!

## E. The quantum capacity

-/

section capacity

/-- Quantum channel capacity is nonnegative for channels out of a nonempty space. -/
Expand All @@ -201,7 +278,8 @@ theorem zero_le_quantumCapacity (Λ : CPTPMap d₁ d₂) [Nonempty d₁] :

/-- Quantum channel capacity is at most log2(D), where D is the input dimension. -/
@[sorryful]
theorem quantumCapacity_ge_log_dim_in (Λ : CPTPMap d₁ d₂) : Λ.quantumCapacity ≤ Real.logb 2 (Fintype.card d₁) :=
theorem quantumCapacity_ge_log_dim_in (Λ : CPTPMap d₁ d₂) :
Λ.quantumCapacity ≤ Real.logb 2 (Fintype.card d₁) :=
Real.sSup_le (by
intro R h
contrapose h
Expand All @@ -211,12 +289,14 @@ theorem quantumCapacity_ge_log_dim_in (Λ : CPTPMap d₁ d₂) : Λ.quantumCapac
· apply Real.logb_nonneg one_lt_two (Nat.one_le_cast.mpr Fintype.card_pos)
· simp [not_nonempty_iff.mp h])

/-- The LSD (Lloyd-Shor-Devetak) theorem: the quantum capacity is at least as large the single-copy coherent
information. The "coherent information" is used in literature to refer to both a function of state and
a channel (`coherentInfo`), or a function of just a channel. In the latter case, the state is implicitly
maximized over. Here we use the former definition and state that the lower bound is true for all states. -/
/-- The LSD (Lloyd-Shor-Devetak) theorem: the quantum capacity is at least as large the
single-copy coherent information. The "coherent information" is used in literature to refer to
both a function of state and a channel (`coherentInfo`), or a function of just a channel. In
the latter case, the state is implicitly maximized over. Here we use the former definition and
state that the lower bound is true for all states. -/
@[sorryful]
theorem coherentInfo_le_quantumCapacity (Λ : CPTPMap d₁ d₂) (ρ : MState d₁) : coherentInfo ρ Λ ≤ Λ.quantumCapacity := by
theorem coherentInfo_le_quantumCapacity (Λ : CPTPMap d₁ d₂) (ρ : MState d₁) :
coherentInfo ρ Λ ≤ Λ.quantumCapacity := by
sorry

/-- The quantum capacity is the limit of the coherent information of n-copy uses of the channel. -/
Expand Down
Loading
Loading