diff --git a/Physlib/SpaceAndTime/Time/API-map.yaml b/Physlib/SpaceAndTime/Time/API-map.yaml new file mode 100644 index 000000000..dc1438be5 --- /dev/null +++ b/Physlib/SpaceAndTime/Time/API-map.yaml @@ -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 diff --git a/QuantumInfo/Capacity/Capacity.lean b/QuantumInfo/Capacity/Capacity.lean index 0cf72a267..d35e563d8 100644 --- a/QuantumInfo/Capacity/Capacity.lean +++ b/QuantumInfo/Capacity/Capacity.lean @@ -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 @@ -62,7 +83,20 @@ 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 @@ -70,7 +104,14 @@ And other important theorems like superdense coding, nonadditivity, superactivat 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 /-- @@ -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 → @@ -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₅] @@ -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`. -/ @@ -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. -/ @@ -139,13 +203,15 @@ 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 @@ -153,8 +219,8 @@ theorem id_achievesRate_log_dim : (id (dIn := d₁)).AchievesRate (Real.logb 2 ( /-- 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 @@ -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, @@ -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. -/ @@ -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 @@ -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. -/ diff --git a/scripts/LinterExemption.txt b/scripts/LinterExemption.txt index 347bf7ac5..0f989cb55 100644 --- a/scripts/LinterExemption.txt +++ b/scripts/LinterExemption.txt @@ -1,4 +1,3 @@ -QuantumInfo/Capacity/Capacity.lean QuantumInfo/Capacity/Capacity_doc.lean QuantumInfo/Channels/Bundled.lean QuantumInfo/Channels/CPTP.lean