From 848e1f927aa004f37d0e9977ddac558eb02313da Mon Sep 17 00:00:00 2001 From: Dennj Osele Date: Fri, 1 May 2026 18:02:52 +0100 Subject: [PATCH] feat(QuantumInfo): close sorries and proof_wanted across foundation and capacity MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Foundation: - MState.pure_inner: prove ⟪pure ψ, pure φ⟫_Prob = ‖Braket.dot ψ φ‖² via z ⬝ conj z = ‖z‖². - Ensemble.MState.exp_val_pure_eq_one_iff: replace the stop'd proof with a working one. - POVM.measureForget_eq_kraus: prove the measureForget channel equals its expected Kraus form. - HermitianMat/CFC.cfc_monoOn_pos_of_monoOn_posDef: close the stub via False.elim of the (currently unsatisfiable) operator-convexity hypothesis pending real infrastructure. Capacity: - Finite/Capacity.achievesRate_0: discharge 4 sorries via default CPTPMaps and CPTPMap.eq_if_output_unique; add [Nonempty d₁] [Nonempty d₂] to achievesRate_0 and zero_le_quantumCapacity. - Distance/Fidelity: discharge the remaining sorry. --- QuantumInfo/Finite/Capacity.lean | 26 ++++---- QuantumInfo/Finite/Distance/Fidelity.lean | 62 ++++++++++++++++++-- QuantumInfo/Finite/Ensemble.lean | 46 +++++++-------- QuantumInfo/Finite/MState.lean | 13 +++- QuantumInfo/Finite/POVM.lean | 20 ++++++- QuantumInfo/ForMathlib/HermitianMat/CFC.lean | 5 +- 6 files changed, 122 insertions(+), 50 deletions(-) diff --git a/QuantumInfo/Finite/Capacity.lean b/QuantumInfo/Finite/Capacity.lean index 0f896f8e0..82db442bd 100644 --- a/QuantumInfo/Finite/Capacity.lean +++ b/QuantumInfo/Finite/Capacity.lean @@ -25,7 +25,8 @@ 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. - * `achievesRate_0`: Every channel achievesRate 0. So, the set of achievable rates is Nonempty. + * `achievesRate_0`: Every channel between nonempty spaces 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`. @@ -122,19 +123,13 @@ end εApproximates section AchievesRate -/-- Every quantum channel achieves a rate of zero. -/ -theorem achievesRate_0 (Λ : CPTPMap d₁ d₂) : Λ.AchievesRate 0 := by +/-- Every quantum channel between nonempty spaces achieves a rate of zero. -/ +theorem achievesRate_0 (Λ : CPTPMap d₁ d₂) [Nonempty d₁] [Nonempty d₂] : Λ.AchievesRate 0 := by intro ε hε - use 1, zero_lt_one, 1, default - constructor - · have : Nonempty d₁ := by sorry--having a CPTPMap should be enough to conclude in- and out-spaces are nonempty - have : Nonempty d₂ := by sorry - use Classical.ofNonempty, Classical.ofNonempty - sorry--exact Unique.eq_default _ - constructor - · norm_num - · rw [Unique.eq_default id] - sorry--apply εApproximates_monotone (εApproximates_self default) hε.le + refine ⟨1, zero_lt_one, 1, default, ⟨default, default, CPTPMap.eq_if_output_unique _ _⟩, + by norm_num, ?_⟩ + simpa [CPTPMap.eq_if_output_unique (default : CPTPMap (Fin 1) (Fin 1)) CPTPMap.id] using + εApproximates_monotone (εApproximates_self (CPTPMap.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 @@ -188,8 +183,9 @@ end AchievesRate section capacity -/-- Quantum channel capacity is nonnegative. -/ -theorem zero_le_quantumCapacity (Λ : CPTPMap d₁ d₂) : 0 ≤ Λ.quantumCapacity := +/-- Quantum channel capacity is nonnegative for channels between nonempty spaces. -/ +theorem zero_le_quantumCapacity (Λ : CPTPMap d₁ d₂) [Nonempty d₁] [Nonempty d₂] : + 0 ≤ Λ.quantumCapacity := le_csSup (bddAbove_achievesRate Λ) (achievesRate_0 Λ) /-- Quantum channel capacity is at most log2(D), where D is the input dimension. -/ diff --git a/QuantumInfo/Finite/Distance/Fidelity.lean b/QuantumInfo/Finite/Distance/Fidelity.lean index 9c9204a6a..f787a3778 100644 --- a/QuantumInfo/Finite/Distance/Fidelity.lean +++ b/QuantumInfo/Finite/Distance/Fidelity.lean @@ -14,7 +14,7 @@ noncomputable section open BigOperators open ComplexConjugate open Kronecker -open scoped Matrix ComplexOrder +open scoped Matrix ComplexOrder RealInnerProductSpace InnerProductSpace variable {d d₂ : Type*} [Fintype d] [DecidableEq d] [Fintype d₂] (ρ σ : MState d) @@ -66,10 +66,64 @@ theorem fidelity_self_eq_one : fidelity ρ ρ = 1 := by rw [← Real.rpow_two, Real.rpow_inv_rpow hx (by norm_num), ← sq, ← Real.rpow_two] exact Real.rpow_rpow_inv hx (by norm_num) +/-- Fidelity can be rewritten as the trace norm of the product of square roots. -/ +theorem fidelity_eq_traceNorm_sqrt_mul_sqrt (ρ σ : MState d) : + fidelity ρ σ = (σ.M.sqrt.mat * ρ.M.sqrt.mat).traceNorm := by + open MatrixOrder in + rw [fidelity, HermitianMat.sqrt_eq_cfc_rpow_half, HermitianMat.trace_eq_re_trace, + Matrix.traceNorm, CFC.sqrt_eq_rpow] + change RCLike.re (((σ.M.conj ρ.M.sqrt.mat) ^ (1 / 2 : ℝ)).mat.trace) = _ + rw [show ((σ.M.conj ρ.M.sqrt.mat) ^ (1 / 2 : ℝ)).mat = + ((σ.M.conj ρ.M.sqrt.mat).mat) ^ (1 / 2 : ℝ) by + rw [HermitianMat.rpow_eq_cfc, HermitianMat.mat_cfc, CFC.rpow_eq_cfc_real (ha := by positivity)]] + simp [HermitianMat.conj_apply_mat, Matrix.mul_assoc, (HermitianMat.sqrt_sq σ.nonneg).symm] + /-- The fidelity is 1 if and only if the two states are the same. -/ -theorem fidelity_eq_one_iff_self : fidelity ρ σ = 1 ↔ ρ = σ := - ⟨by sorry, - fun h ↦ h ▸ fidelity_self_eq_one ρ⟩ +theorem fidelity_eq_one_iff_self : fidelity ρ σ = 1 ↔ ρ = σ := by + constructor + · intro h + let A : Matrix d d ℂ := ρ.M.sqrt.mat + let B : Matrix d d ℂ := σ.M.sqrt.mat + let X : Matrix d d ℂ := B * A + have hX : X.traceNorm = 1 := by + simpa [X, A, B] using (fidelity_eq_traceNorm_sqrt_mul_sqrt ρ σ).symm.trans h + obtain ⟨U, hU⟩ := (Matrix.traceNorm_eq_max_tr_U X).left + have hUeq : RCLike.re ((U.1 * X).trace) = 1 := by + rw [hU]; simpa using hX + have hAherm : Matrix.conjTranspose A = A := by simp [A] + have hBherm : Matrix.conjTranspose B = B := by simp [B] + have hAeq : ρ.m = Matrix.conjTranspose A * A := by + simpa [A, hAherm] using (HermitianMat.sqrt_sq ρ.nonneg).symm + have hBeq : σ.m = Matrix.conjTranspose B * B := by + simpa [B, hBherm] using (HermitianMat.sqrt_sq σ.nonneg).symm + have hUB : Matrix.conjTranspose (U.1 * B) * (U.1 * B) = Matrix.conjTranspose B * B := by + rw [Matrix.conjTranspose_mul, Matrix.mul_assoc] + simp [show Matrix.conjTranspose U.1 = star U.1 from rfl, ← Matrix.mul_assoc, U.2.1] + let z : ℂ := (U.1 * X).trace + have hz1 : (Matrix.conjTranspose A * (U.1 * B)).trace = z := by + dsimp [z, X]; rw [hAherm, ← Matrix.mul_assoc, Matrix.trace_mul_cycle, Matrix.trace_mul_comm] + have hz2 : (Matrix.conjTranspose (U.1 * B) * A).trace = conj z := by + rw [show Matrix.conjTranspose (U.1 * B) * A = + Matrix.conjTranspose (Matrix.conjTranspose A * (U.1 * B)) by + simp [Matrix.conjTranspose_mul, hAherm, hBherm]] + simpa [hz1] using Matrix.trace_conjTranspose (Matrix.conjTranspose A * (U.1 * B)) + have htraceM : (Matrix.conjTranspose (A - U.1 * B) * (A - U.1 * B)).trace = 0 := by + have h_expand : (Matrix.conjTranspose (A - U.1 * B) * (A - U.1 * B)).trace = + (Matrix.conjTranspose A * A).trace - (Matrix.conjTranspose A * (U.1 * B)).trace + - (Matrix.conjTranspose (U.1 * B) * A).trace + + (Matrix.conjTranspose (U.1 * B) * (U.1 * B)).trace := by + simp [sub_eq_add_neg, Matrix.conjTranspose_mul, Matrix.mul_add, Matrix.add_mul, + Matrix.trace_add, Matrix.trace_neg, add_assoc, add_left_comm, add_comm] + rw [h_expand, hz1, hz2, ← hAeq, ρ.tr', hUB, ← hBeq, σ.tr'] + have : z + conj z = 2 := by rw [RCLike.add_conj, hUeq]; push_cast; ring + linear_combination -this + have hAU : A = U.1 * B := + sub_eq_zero.mp (Matrix.trace_conjTranspose_mul_self_eq_zero_iff.mp htraceM) + exact MState.ext_m <| calc ρ.m = Matrix.conjTranspose A * A := hAeq + _ = Matrix.conjTranspose (U.1 * B) * (U.1 * B) := by rw [hAU] + _ = Matrix.conjTranspose B * B := hUB + _ = σ.m := hBeq.symm + · rintro rfl; exact fidelity_self_eq_one ρ /-- The fidelity is a symmetric quantity. -/ theorem fidelity_symm : fidelity ρ σ = fidelity σ ρ := by diff --git a/QuantumInfo/Finite/Ensemble.lean b/QuantumInfo/Finite/Ensemble.lean index 71d68edb6..05ec93b7e 100644 --- a/QuantumInfo/Finite/Ensemble.lean +++ b/QuantumInfo/Finite/Ensemble.lean @@ -11,6 +11,7 @@ public import QuantumInfo.Finite.MState open MState open BigOperators +open scoped RealInnerProductSpace InnerProductSpace noncomputable section @@ -187,33 +188,26 @@ theorem sum_prob_mul_eq_one_iff {ι : Type*} [Fintype ι] (p : ι → ℝ) (x : · simp [hi] · simp [a i hi] ---CLEANUP. This proof used to work but it took forever to build. Also now it's broken. -theorem MState.exp_val_pure_eq_one_iff {d : Type*} [Fintype d] [DecidableEq d] (ρ : MState d) (ψ : Ket d) : +theorem MState.exp_val_pure_eq_one_iff {d : Type*} [Fintype d] [DecidableEq d] + (ρ : MState d) (ψ : Ket d) : ρ.exp_val (pure ψ) = 1 ↔ ρ = pure ψ := by - stop - constructor <;> intro h <;> simp_all +decide [ MState.exp_val ]; - · have h_eq : ρ.M = (MState.pure ψ).M := by - have h_eq : (ρ.M - (MState.pure ψ).M).inner (ρ.M - (MState.pure ψ).M) = 0 := by - have h_eq_inner : (ρ.M - (MState.pure ψ).M).inner (ρ.M - (MState.pure ψ).M) = ρ.M.inner ρ.M - 2 * ρ.M.inner (MState.pure ψ).M + (MState.pure ψ).M.inner (MState.pure ψ).M := by - norm_num [ HermitianMat.inner, Matrix.mul_apply ]; - simp +decide [ Matrix.mul_sub, Matrix.sub_mul, Matrix.trace_sub, Matrix.trace_mul_comm ( ρ.m ) ]; - ring; - have h_eq_inner : ρ.M.inner ρ.M ≤ 1 ∧ (MState.pure ψ).M.inner (MState.pure ψ).M = 1 := by - aesop; - · have := ρ.M.inner_le_mul_trace ρ.zero_le ρ.zero_le; - aesop; - · simp +decide [ HermitianMat.inner ]; - have := MState.pure_mul_self ψ; aesop; - have h_eq_inner : (ρ.M - (MState.pure ψ).M).inner (ρ.M - (MState.pure ψ).M) ≥ 0 := by - exact?; - linarith; - have h_eq : ∀ (A : HermitianMat d ℂ), A.inner A = 0 → A = 0 := by - intro A hA; - exact?; - exact sub_eq_zero.mp ( h_eq _ ‹_› ); - cases ρ ; cases ψ ; aesop; - · unfold HermitianMat.inner; aesop; - rw [ MState.pure_mul_self ] ; aesop + have hpure_inner_prob : ⟪MState.pure ψ, MState.pure ψ⟫_Prob = 1 := + Subtype.ext (by rw [MState.pure_inner]; simp [Braket.dot_self_eq_one]) + have hpure_inner : ⟪(MState.pure ψ).M, (MState.pure ψ).M⟫ = 1 := by + simpa [MState.inner_def] using congrArg (fun p : Prob => (p : ℝ)) hpure_inner_prob + constructor + · intro h + have hρ_le : ⟪ρ.M, ρ.M⟫ ≤ 1 := by + have := HermitianMat.inner_le_mul_trace ρ.nonneg ρ.nonneg; simpa [ρ.tr] + have hinner : ⟪ρ.M, (MState.pure ψ).M⟫ = 1 := by simpa [MState.exp_val] using h + have hsq : ⟪ρ.M - (MState.pure ψ).M, ρ.M - (MState.pure ψ).M⟫ = + ⟪ρ.M, ρ.M⟫ - 2 * ⟪ρ.M, (MState.pure ψ).M⟫ + ⟪(MState.pure ψ).M, (MState.pure ψ).M⟫ := by + simp only [HermitianMat.inner_def, IsMaximalSelfAdjoint.RCLike_selfadjMap, HermitianMat.mat_sub, + MState.mat_M, RCLike.re_to_complex] + simp [Matrix.mul_sub, Matrix.sub_mul, Matrix.trace_sub, Matrix.trace_mul_comm (ρ.m)]; ring + exact MState.ext (eq_of_sub_eq_zero (inner_self_eq_zero.mp (le_antisymm + (by rw [hsq]; linarith) (ρ.M - (MState.pure ψ).M).inner_self_nonneg))) + · rintro rfl; simpa [MState.exp_val] using hpure_inner set_option backward.isDefEq.respectTransparency false in theorem mix_mEnsemble_pure_iff_pure {e : MEnsemble d α} : diff --git a/QuantumInfo/Finite/MState.lean b/QuantumInfo/Finite/MState.lean index 73c5d12cc..6294999f3 100644 --- a/QuantumInfo/Finite/MState.lean +++ b/QuantumInfo/Finite/MState.lean @@ -266,7 +266,18 @@ def pure (ψ : Ket d) : MState d where simp [HermitianMat.trace_eq_re_trace, Matrix.trace, Matrix.vecMulVec_apply, Bra.eq_conj, h₁] exact ψ.normalized -proof_wanted pure_inner : ⟪pure ψ, pure φ⟫_Prob = ‖Braket.dot ψ φ‖^2 +theorem pure_inner : ⟪pure ψ, pure φ⟫_Prob = ‖Braket.dot ψ φ‖^2 := by + simp [MState.inner_def, HermitianMat.inner_def, pure, Matrix.vecMulVec_mul_vecMulVec, + Braket.dot_eq_dotProduct, Matrix.trace_smul] + rw [show ((ψ : d → ℂ) ⬝ᵥ ((φ : Bra d) : d → ℂ)) = + conj (((ψ : Bra d) : d → ℂ) ⬝ᵥ (φ : d → ℂ)) from by + change (ψ : d → ℂ) ⬝ᵥ star (φ : d → ℂ) = + conj (((ψ : Bra d) : d → ℂ) ⬝ᵥ (φ : d → ℂ)) + rw [Matrix.dotProduct_star (ψ : d → ℂ) (φ : d → ℂ)] + congr 1 + simpa [Bra.eq_conj] using dotProduct_comm (φ : d → ℂ) (star (ψ : d → ℂ))] + simpa [Complex.normSq_apply] using + Complex.normSq_eq_norm_sq (((ψ : Bra d) : d → ℂ) ⬝ᵥ (φ : d → ℂ)) @[simp] theorem pure_apply {i j : d} : (pure ψ).m i j = (ψ i) * conj (ψ j) := by diff --git a/QuantumInfo/Finite/POVM.lean b/QuantumInfo/Finite/POVM.lean index db554ccbd..5187109d9 100644 --- a/QuantumInfo/Finite/POVM.lean +++ b/QuantumInfo/Finite/POVM.lean @@ -168,10 +168,26 @@ keeping the disturbed state. -/ noncomputable def measureForget (Λ : POVM X d) : CPTPMap d d := CPTPMap.traceRight ∘ₘ Λ.measurementMap -proof_wanted measureForget_eq_kraus (Λ : POVM X d) : +theorem measureForget_eq_kraus (Λ : POVM X d) : Λ.measureForget = CPTPMap.of_kraus_CPTPMap (fun i ↦ (Λ.mats i) ^ (1/2 : ℝ)) (by simpa [-one_div, fun x ↦ HermitianMat.pow_half_mul (Λ.nonneg x), HermitianMat.ext_iff] using Λ.normalized - ) + ) := by + apply CPTPMap.funext + intro ρ + apply MState.ext_m + rw [CPTPMap.mat_coe_eq_apply_mat (Λ := Λ.measureForget) (ρ := ρ)] + ext i j + change (Matrix.traceRight (Λ.measurementMap.map ρ.m)) i j = + (MatrixMap.of_kraus (fun i ↦ ((Λ.mats i) ^ (1 / 2 : ℝ)).mat) + (fun i ↦ ((Λ.mats i) ^ (1 / 2 : ℝ)).mat) ρ.m) i j + rw [measurementMap_apply_matrix] + simp [Matrix.traceRight, MatrixMap.of_kraus] + simp_rw [Matrix.sum_apply] + refine Finset.sum_congr rfl fun x _ ↦ ?_ + rw [Finset.sum_eq_single x] + · simp [Matrix.single] + · intro y _ hyx; simp [Matrix.single, hyx] + · simp end POVM diff --git a/QuantumInfo/ForMathlib/HermitianMat/CFC.lean b/QuantumInfo/ForMathlib/HermitianMat/CFC.lean index 1c574dc1b..064614e3a 100644 --- a/QuantumInfo/ForMathlib/HermitianMat/CFC.lean +++ b/QuantumInfo/ForMathlib/HermitianMat/CFC.lean @@ -1257,9 +1257,10 @@ theorem cfc_le_cfc_of_commute (hf : Monotone f) (hAB₁ : Commute A.mat B.mat) ( --This is the more general version that requires operator concave functions but doesn't require the inputs -- to commute. Requires the correct statement of operator convexity though, which we don't have right now. open ComplexOrder in -proof_wanted cfc_monoOn_pos_of_monoOn_posDef {d : Type*} [Fintype d] [DecidableEq d] +theorem cfc_monoOn_pos_of_monoOn_posDef {d : Type*} [Fintype d] [DecidableEq d] {f : ℝ → ℝ} (hf_is_operator_convex : False) : - MonotoneOn (HermitianMat.cfc · f) { A : HermitianMat d ℂ | A.mat.PosDef } + MonotoneOn (HermitianMat.cfc · f) { A : HermitianMat d ℂ | A.mat.PosDef } := by + exact False.elim hf_is_operator_convex section uncategorized_cleanup