From 1c3763f6726979ba074d5dc8fa9fb2e2a605f398 Mon Sep 17 00:00:00 2001 From: suzuki Date: Thu, 30 Apr 2026 18:40:06 +0000 Subject: [PATCH 1/2] build: bump lean to v4.30.0-rc2 --- .devcontainer/Dockerfile | 2 +- .gitignore | 3 +++ lake-manifest.json | 35 ++++++++++++++++++----------------- lakefile.toml | 2 +- lean-toolchain | 2 +- 5 files changed, 24 insertions(+), 20 deletions(-) diff --git a/.devcontainer/Dockerfile b/.devcontainer/Dockerfile index 869d95d..c9a9f4d 100644 --- a/.devcontainer/Dockerfile +++ b/.devcontainer/Dockerfile @@ -14,5 +14,5 @@ RUN apt-get update && \ USER vscode WORKDIR /home/vscode -RUN curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:4.27.0-rc1 +RUN curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:4.30.0-rc2 ENV PATH="/home/vscode/.elan/bin:${PATH}" diff --git a/.gitignore b/.gitignore index 76d5743..89a592c 100644 --- a/.gitignore +++ b/.gitignore @@ -5,3 +5,6 @@ lefthook-local.yml references/ skill-creator-tests/ **/__pycache__/ + +# Ignore until https://github.com/microsoft/vscode-remote-release/issues/11616 is fixed. +devcontainer-lock.json diff --git a/lake-manifest.json b/lake-manifest.json index 3bad3ce..8676834 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,21 +1,21 @@ -{"version": "1.1.0", +{"version": "1.2.0", "packagesDir": ".lake/packages", "packages": [{"url": "https://github.com/leanprover-community/mathlib4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "32d24245c7a12ded17325299fd41d412022cd3fe", + "rev": "5450b53e5ddc75d46418fabb605edbf36bd0beb6", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.27.0-rc1", + "inputRev": "v4.30.0-rc2", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "8d3713f36dda48467eb61f8c1c4db89c49a6251a", + "rev": "86210d4ad1b08b086d0bd638637a75246523dbb8", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "19e5f5cc9c21199be466ef99489e3acab370f079", + "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "4eb26e1a4806b200ddfe5179d0c2a0fae56c54a7", + "rev": "cdab3938ccabbdb044be6896e251b5814bec932e", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,51 +45,52 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "ef8377f31b5535430b6753a974d685b0019d0681", + "rev": "2db6054a44326f8c0230ee0570e2ddb894816511", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.84", + "inputRev": "v0.0.98", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "fb12f5535c80e40119286d9575c9393562252d21", + "rev": "f0c6e183ea26531e82773feb4b73ab6595ca17a5", "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "v4.30.0-rc2", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "523ec6fc8062d2f470fdc8de6f822fe89552b5e6", + "rev": "1cc7e819b9b9bc1e87c9edcccb62e0269e00a809", "name": "Qq", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "v4.30.0-rc2", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "6254bed25866358ce4f841fa5a13b77de04ffbc8", + "rev": "5c57f3857ba81924a88b2cdf4f062e34ec04ff11", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "v4.30.0-rc2", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, "scope": "leanprover", - "rev": "726b98c53e2da249c1de768fbbbb5e67bc9cef60", + "rev": "13567aed1ac4f12aea9484178e07e51f8c9f7658", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.27.0-rc1", + "inputRev": "v4.30.0-rc2", "inherited": true, "configFile": "lakefile.toml"}], "name": "QuantumSystem", - "lakeDir": ".lake"} + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/lakefile.toml b/lakefile.toml index 0499d4d..b5cf638 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -14,7 +14,7 @@ leanOptions.linter.style.longLine = false [[require]] name = "mathlib" scope = "leanprover-community" -rev = "v4.27.0-rc1" +rev = "v4.30.0-rc2" [[lean_exe]] name = "mk_all" diff --git a/lean-toolchain b/lean-toolchain index bd19bde..6c7e31f 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.27.0-rc1 +leanprover/lean4:v4.30.0-rc2 From c911f10f7550e35933e9e8655d5bac52b383a817 Mon Sep 17 00:00:00 2001 From: suzuki Date: Fri, 1 May 2026 09:49:28 +0000 Subject: [PATCH 2/2] chore: make compatible with v4.30.0-rc2 --- .../CStarAlgebra/GNS/Construction.lean | 57 ++-- .../Algebra/CStarAlgebra/GNS/DirectSum.lean | 2 +- .../Algebra/CStarAlgebra/GNS/PureState.lean | 51 ++-- .../CStarAlgebra/GNS/Representation.lean | 6 +- .../Algebra/CStarAlgebra/PureState.lean | 93 ++++++- .../Algebra/CStarAlgebra/QuasiState.lean | 13 +- QuantumSystem/Algebra/CStarAlgebra/State.lean | 2 +- .../CStarAlgebra/State/Continuity.lean | 4 +- .../Algebra/CStarAlgebra/State/Faithful.lean | 2 +- QuantumSystem/Analysis/CFC/Diagonal.lean | 30 ++- .../Analysis/Entropy/RelativeEntropy.lean | 72 +++-- .../Analysis/Entropy/VonNeumannEntropy.lean | 21 +- QuantumSystem/Analysis/Matrix/Effros.lean | 57 ++-- .../Matrix/HermitianFunctionalCalculus.lean | 53 +++- .../Analysis/Matrix/LiebConcavity.lean | 248 +++++++++++------- QuantumSystem/Analysis/Matrix/Order.lean | 217 +++++++++++---- QuantumSystem/Analysis/Matrix/PosDef.lean | 28 +- QuantumSystem/Channel.lean | 5 +- .../Analysis/CStarAlgebra/Ideal.lean | 4 +- .../Analysis/CStarAlgebra/WeakDual.lean | 26 +- .../Analysis/Calculus/Deriv/Sign.lean | 2 +- .../ForMathlib/Analysis/Matrix/Basic.lean | 125 ++++++--- .../ForMathlib/Analysis/Matrix/Hermitian.lean | 10 +- .../ForMathlib/Analysis/Matrix/Order.lean | 2 +- .../ContinuousFunctionalCalculus/Abs.lean | 8 + .../PartialIsometry.lean | 4 +- .../LinearAlgebra/Matrix/StarAlgEquiv.lean | 39 ++- QuantumSystem/State.lean | 30 ++- 28 files changed, 859 insertions(+), 352 deletions(-) diff --git a/QuantumSystem/Algebra/CStarAlgebra/GNS/Construction.lean b/QuantumSystem/Algebra/CStarAlgebra/GNS/Construction.lean index 672bf21..c5b4645 100644 --- a/QuantumSystem/Algebra/CStarAlgebra/GNS/Construction.lean +++ b/QuantumSystem/Algebra/CStarAlgebra/GNS/Construction.lean @@ -18,7 +18,7 @@ open ComplexConjugate NNReal Topology Filter variable {A : Type*} [NonUnitalCStarAlgebra A] variable (ω : State ℂ A) -def Nω : CStarAlgebraIdeal A where +@[reducible] def Nω : CStarAlgebraIdeal A where carrier := { x : A | ω (star x * x) = 0 } zero_mem' := by change ω (star (0 : A) * (0 : A)) = 0 @@ -42,7 +42,7 @@ local notation "Nω" => (Nω ω) `⟪[x], [y]⟫ = ω (star x * y)`. Well-defined because the kernel ideal `Nω` is the null space with respect to the positive sesquilinear form coming from the state `ω` (ultimately a consequence of the Cauchy–Schwarz inequality for states). -/ -def innerQuotient (xq yq : A ⧸ Nω) : ℂ := +noncomputable def innerQuotient (xq yq : A ⧸ Nω) : ℂ := Quotient.liftOn₂' xq yq (fun x y => ω (star x * y)) (fun x₁ y₁ x₂ y₂ (hx : CStarAlgebraIdeal.leftRel Nω x₁ x₂) (hy : CStarAlgebraIdeal.leftRel Nω y₁ y₂) => by rw [CStarAlgebraIdeal.leftRel, QuotientAddGroup.leftRel_apply] at hx hy @@ -54,7 +54,7 @@ def innerQuotient (xq yq : A ⧸ Nω) : ℂ := _ = ω (star x₂ * y₂) := (State.equiv_right (ω := ω) (x := x₂) (y₁ := y₂) (y₂ := y₁) hy').symm) /-- The inner product space core structure on the quotient. -/ -instance instInnerProductSpaceCore : InnerProductSpace.Core ℂ (A ⧸ Nω) where +noncomputable abbrev innerProductSpaceCoreQuot : InnerProductSpace.Core ℂ (A ⧸ Nω) where inner := innerQuotient ω conj_inner_symm := fun x y => Quotient.inductionOn₂' x y fun a b => by simp only [innerQuotient, Quotient.liftOn₂'_mk''] @@ -81,34 +81,39 @@ instance instInnerProductSpaceCore : InnerProductSpace.Core ℂ (A ⧸ Nω) wher definite := fun x hx => Quotient.inductionOn' x (fun a ha => by have ha' : ω (star a * a) = 0 := by simpa [innerQuotient] using ha - exact Quotient.sound' (by - simpa [CStarAlgebraIdeal.leftRel, QuotientAddGroup.leftRel_apply] using ha')) hx + apply Quotient.sound' + rw [CStarAlgebraIdeal.leftRel, QuotientAddGroup.leftRel_apply] + simpa using ha') hx --- Pattern adapted from Mathlib 4.25+ Matrix.PosDef --- First define NormedAddCommGroup from the Core (not an instance yet) -noncomputable def normedAddCommGroupQuot : NormedAddCommGroup (A ⧸ Nω) := - @InnerProductSpace.Core.toNormedAddCommGroup ℂ _ _ _ _ (instInnerProductSpaceCore (ω := ω)) - --- Then define InnerProductSpace using ofCore with explicit SeminormedAddCommGroup -noncomputable def innerProductSpaceQuot : @InnerProductSpace ℂ (A ⧸ Nω) _ (normedAddCommGroupQuot (ω := ω)).toSeminormedAddCommGroup := - letI : InnerProductSpace.Core ℂ (A ⧸ Nω) := instInnerProductSpaceCore (ω := ω) - @InnerProductSpace.ofCore ℂ _ _ (normedAddCommGroupQuot (ω := ω)).toAddCommGroup _ inferInstance - --- Now make them instances +-- Pattern from Mathlib's GelfandNaimarkSegal: separate Core abbrev and IPS instances. noncomputable instance instNormedAddCommGroupQuot : NormedAddCommGroup (A ⧸ Nω) := - normedAddCommGroupQuot (ω := ω) + @InnerProductSpace.Core.toNormedAddCommGroup ℂ (A ⧸ Nω) _ _ _ (innerProductSpaceCoreQuot ω) + +/-- The pre-inner product structure derived from the InnerProductSpace.Core. -/ +noncomputable instance instPreInnerProductSpaceCoreQuot : PreInnerProductSpace.Core ℂ (A ⧸ Nω) where + inner := innerQuotient ω + conj_inner_symm := (innerProductSpaceCoreQuot ω).conj_inner_symm + re_inner_nonneg := (innerProductSpaceCoreQuot ω).re_inner_nonneg + add_left := (innerProductSpaceCoreQuot ω).add_left + smul_left := (innerProductSpaceCoreQuot ω).smul_left noncomputable instance instInnerProductSpaceQuot : InnerProductSpace ℂ (A ⧸ Nω) := - innerProductSpaceQuot (ω := ω) + InnerProductSpace.ofCore (instPreInnerProductSpaceCoreQuot ω) + +/-- Inner product on the quotient is the `innerQuotient` function. This holds because the +`InnerProductSpace` instance on the quotient is built reducibly from the corresponding +`InnerProductSpace.Core`. -/ +private lemma inner_quotient_eq (x y : A ⧸ Nω) : + @inner ℂ (A ⧸ Nω) _ x y = innerQuotient ω x y := rfl /-- The squared norm of the class `[x]` equals the real part `Re (ω (star x * x))`. -/ private lemma norm_sq_eq_inner (x : A) : @norm (A ⧸ Nω) (instNormedAddCommGroupQuot ω).toNorm (Quotient.mk'' x) ^ 2 = (ω (star x * x)).re := by rw [@norm_sq_eq_re_inner ℂ (A ⧸ Nω) _ _] - change ((@inner ℂ (A ⧸ Nω) _ (Quotient.mk'' x) (Quotient.mk'' x))).re = (ω (star x * x)).re - change (innerQuotient ω (Quotient.mk'' x) (Quotient.mk'' x)).re = (ω (star x * x)).re + rw [inner_quotient_eq] unfold innerQuotient simp only [Quotient.liftOn₂'_mk''] + rfl /-- Inner products with elements of the kernel ideal vanish: if `s ∈ Nω` then `ω (star x * s) = 0`. -/ @@ -154,8 +159,7 @@ lemma πω'_norm_sq_le (a : A) (b : A ⧸ Nω) : ‖πω' ω a b‖ ^ 2 ≤ ‖a -- Use inner_self = ‖·‖ * ‖·‖ in a pre-Hilbert setting (core inner product structure) rw [← inner_self_eq_norm_mul_norm (𝕜 := ℂ) (E := A ⧸ Nω) (Quotient.mk'' (a * b'))] rw [← inner_self_eq_norm_mul_norm (𝕜 := ℂ) (E := A ⧸ Nω) (Quotient.mk'' b')] - change (innerQuotient ω (Quotient.mk'' (a * b')) (Quotient.mk'' (a * b'))).re ≤ - ‖a‖ * ‖a‖ * (innerQuotient ω (Quotient.mk'' b') (Quotient.mk'' b')).re + rw [inner_quotient_eq, inner_quotient_eq] unfold innerQuotient; simp only [Quotient.liftOn₂'_mk''] -- Algebraic rearrangement: bring star inside and reassociate to isolate star a * a rw [show star (a * b') * (a * b') = star b' * star a * a * b' by rw [star_mul, mul_assoc, mul_assoc, mul_assoc]] @@ -172,6 +176,7 @@ lemma πω'_norm_sq_le (a : A) (b : A ⧸ Nω) : ‖πω' ω a b‖ ^ 2 ≤ ‖a have : ‖a‖ * ‖a‖ * (ω (star b' * b')).re = ‖a‖ * (‖a‖ * (ω (star b' * b')).re) := mul_assoc _ _ _ have hr_nonneg : (0 : ℝ) ≤ r := r.property -- Finish with linear arithmetic: nonneg remainder r gives desired ≤ + change (ω (star b' * star a * a * b')).re ≤ ‖a‖ * ‖a‖ * (ω (star b' * b')).re linarith /-- Multiplicativity: πω'(ab) = πω'(a) ∘ πω'(b). -/ @@ -184,7 +189,7 @@ lemma πω'_inner (a : A) (b c : A ⧸ Nω) : refine Quotient.inductionOn₂' b c fun b' c' => ?_ unfold πω' simp only [Quotient.liftOn'_mk''] - change innerQuotient ω (Quotient.mk'' (a * b')) (Quotient.mk'' c') = innerQuotient ω (Quotient.mk'' b') (Quotient.mk'' (star a * c')) + rw [inner_quotient_eq, inner_quotient_eq] unfold innerQuotient simp only [Quotient.liftOn₂'_mk'', star_mul, mul_assoc] @@ -380,7 +385,7 @@ lemma stateOnQuotFun_bound (x : A ⧸ Nω) : ‖stateOnQuotFun ω x‖ ≤ 1 * -- Derive global bound by contradiction if limit were strictly larger have : ‖ω a‖ ^ 2 ≤ (ω (star a * a)).re := by haveI : (CStarAlgebra.approximateUnit A).NeBot := h_approx.toIsApproximateUnit.neBot - by_contra hlt; push_neg at hlt + by_contra hlt; push Not at hlt set δ : ℝ := (‖ω a‖ ^ 2 - (ω (star a * a)).re) / 2 have hδ_pos : 0 < δ := half_pos (sub_pos.mpr hlt) have h_close := (Metric.tendsto_nhds.mp h_tendsto) δ hδ_pos @@ -528,11 +533,11 @@ lemma ξω_norm : ‖ξω ω‖ = 1 := by suffices 1 ≤ ‖stateOnQuot ω‖ from this.trans h2 have h_norm : ‖ω‖ = 1 := ω.norm_eq_one rw [← h_norm] - by_contra h_not; push_neg at h_not + by_contra h_not; push Not at h_not -- Expand definition of norm via supremum over ratios ‖ω a‖/‖a‖ rw [State.norm_def] at h_not obtain ⟨_, ⟨a, ha, rfl⟩, h_r_large⟩ : ∃ r ∈ {s : ℝ | ∃ a : A, a ≠ 0 ∧ s = ‖ω a‖ / ‖a‖}, ‖stateOnQuot ω‖ < r := by - by_contra h_no; push_neg at h_no + by_contra h_no; push Not at h_no have : sSup {s : ℝ | ∃ a : A, a ≠ 0 ∧ s = ‖ω a‖ / ‖a‖} ≤ ‖stateOnQuot ω‖ := by refine csSup_le ?_ h_no by_contra h_empty diff --git a/QuantumSystem/Algebra/CStarAlgebra/GNS/DirectSum.lean b/QuantumSystem/Algebra/CStarAlgebra/GNS/DirectSum.lean index 070c671..793e5e9 100644 --- a/QuantumSystem/Algebra/CStarAlgebra/GNS/DirectSum.lean +++ b/QuantumSystem/Algebra/CStarAlgebra/GNS/DirectSum.lean @@ -245,7 +245,7 @@ theorem directSumAlgHom_injective : Function.Injective (directSumAlgHom (A := A) simp · simp only [dif_neg h, if_neg h]; simp rw [h_eq] - apply summable_of_finite_support + apply summable_of_hasFiniteSupport have : Function.support (fun ψ' => if ψ' = ψ then ‖ψ.gnsRepresentation.ξ‖ ^ 2 else 0) ⊆ {ψ} := by intro ψ' hψ' diff --git a/QuantumSystem/Algebra/CStarAlgebra/GNS/PureState.lean b/QuantumSystem/Algebra/CStarAlgebra/GNS/PureState.lean index aeabcc3..7ede837 100644 --- a/QuantumSystem/Algebra/CStarAlgebra/GNS/PureState.lean +++ b/QuantumSystem/Algebra/CStarAlgebra/GNS/PureState.lean @@ -54,7 +54,7 @@ lemma isInvariant_orthogonal (T : GNS.Representation ω) (W : Submodule ℂ T.H) refine (W.mem_orthogonal ((T.π a) x)).2 ?_ intro w hw have hw_map : (T.π (star a)) w ∈ W.map (T.π (star a)) := - ⟨w, hw, rfl⟩ + ⟨w, hw, by rfl⟩ have hw' : (T.π (star a)) w ∈ W := (hWinv (star a)) hw_map have hx0 : ⟪(T.π (star a)) w, x⟫ = 0 := by -- `x ∈ Wᗮ` means it is orthogonal to every element of `W`. @@ -167,7 +167,7 @@ lemma vectorFunctional_isPositive (T : GNS.Representation ω) (v : T.H) : rw [RCLike.ofReal_eq_complex_ofReal] exact (Complex.ofReal_pow ‖(T.π a) v‖ 2).symm -- Convert the RHS into the form expected by `IsPositive` (with an `ℝ≥0` witness). - simp [h] + rw [h]; rfl lemma opNorm_vectorFunctional_le (T : GNS.Representation ω) (v : T.H) : ‖WeakDual.toStrongDual (T.vectorFunctional v)‖ ≤ ‖v‖ ^ 2 := by @@ -259,7 +259,7 @@ lemma normalized_vectorFunctional_mem_quasiStateSpace (T : GNS.Representation ω · -- Positivity have hpos := vectorFunctional_isPositive T v let c : ℝ≥0 := ⟨(‖v‖ ^ 2)⁻¹, inv_nonneg.mpr (sq_nonneg _)⟩ - have : (‖v‖ ^ 2 : ℂ)⁻¹ = (c : ℂ) := by simp [c, Complex.ofReal_inv] + have : (‖v‖ ^ 2 : ℂ)⁻¹ = (c : ℂ) := by simp [c]; norm_cast rw [this] change _ ∈ {φ | IsPositive A φ} have h_smul : (c : ℂ) • T.vectorFunctional v = c • T.vectorFunctional v := by @@ -284,7 +284,7 @@ lemma trichotomy_from_purity {ψ : PureState A} ‖v₁‖ ^ 2 = 0 ∨ ‖v₁‖ ^ 2 = 1 := by let T := PureState.gnsRepresentation ψ by_contra h_contra - push_neg at h_contra + push Not at h_contra have h_in_Icc := norm_sq_in_Icc T v₁ v₂ hξ horth have h_pos : 0 < ‖v₁‖ ^ 2 := lt_of_le_of_ne h_in_Icc.1 h_contra.1.symm have h_lt_one : ‖v₁‖ ^ 2 < 1 := lt_of_le_of_ne h_in_Icc.2 h_contra.2 @@ -321,12 +321,12 @@ lemma trichotomy_from_purity {ψ : PureState A} have h1_sub_t_ne_c : (1 - (t : ℂ)) ≠ 0 := by have : ((1 - t : ℝ) : ℂ) ≠ 0 := Complex.ofReal_ne_zero.mpr h1_sub_t_ne simpa only [Complex.ofReal_one, Complex.ofReal_sub] using this - have ht_smul : (t : ℝ) • φ = (t : ℂ) • φ := - RCLike.real_smul_eq_coe_smul (K := ℂ) (E := WeakDual ℂ A) t φ + have ht_smul : (t : ℝ) • φ = (t : ℂ) • φ := by + apply ContinuousLinearMap.ext; intro a; rfl have h1_smul : (1 - t : ℝ) • χ = (1 - (t : ℂ)) • χ := by - -- First use RCLike lemma to get (1 - t) • χ = ↑(1 - t) • χ - have step1 : (1 - t : ℝ) • χ = ((1 - t : ℝ) : ℂ) • χ := - RCLike.real_smul_eq_coe_smul (K := ℂ) (E := WeakDual ℂ A) (1 - t) χ + -- First show (1 - t) • χ = ↑(1 - t) • χ + have step1 : (1 - t : ℝ) • χ = ((1 - t : ℝ) : ℂ) • χ := by + apply ContinuousLinearMap.ext; intro a; rfl -- Then rewrite ↑(1 - t) as (1 - ↑t) rw [step1, Complex.ofReal_sub, Complex.ofReal_one] have h_sum_c : ψ.val = (t : ℂ) • φ + (1 - (t : ℂ)) • χ := by @@ -339,9 +339,12 @@ lemma trichotomy_from_purity {ψ : PureState A} have hrhs : ((t : ℂ) • φ + (1 - (t : ℂ)) • χ) a = (T.vectorFunctional v₁) a + (T.vectorFunctional v₂) a := by - rw [ContinuousLinearMap.add_apply, ContinuousLinearMap.smul_apply, ContinuousLinearMap.smul_apply] + change (t : ℂ) • φ a + (1 - (t : ℂ)) • χ a = _ dsimp only [φ, χ] - rw [ContinuousLinearMap.smul_apply, ContinuousLinearMap.smul_apply] + rw [show ((t : ℂ)⁻¹ • T.vectorFunctional v₁) a + = (t : ℂ)⁻¹ • (T.vectorFunctional v₁) a from rfl, + show ((1 - (t : ℂ))⁻¹ • T.vectorFunctional v₂) a + = (1 - (t : ℂ))⁻¹ • (T.vectorFunctional v₂) a from rfl] rw [smul_smul, smul_smul] rw [mul_inv_cancel₀ ht_ne_c, mul_inv_cancel₀ h1_sub_t_ne_c] rw [one_smul, one_smul] @@ -367,10 +370,23 @@ lemma trichotomy_from_purity {ψ : PureState A} have h_eq : φ = χ := by rw [h_eq2, ← h_eq1] -- Contradiction via density have h_dense : Dense (Set.range (fun a => (T.π a) T.ξ)) := by - change Dense (Set.range (T.piApply T.ξ)) - rw [← LinearMap.coe_range] - rw [← Submodule.span_eq (LinearMap.range (T.piApply T.ξ))] - exact T.cyclic + have h_cyc := T.cyclic + -- View `Set.range (fun a => π a ξ)` via `T.piApply T.ξ` as a `LinearMap.range`, + -- then identify it with the cyclic span used by `T.cyclic`. + have h1 : (Set.range (fun a => (T.π a) T.ξ)) + = ((LinearMap.range (T.piApply T.ξ).toLinearMap) : Set T.H) := by + rw [LinearMap.coe_range]; rfl + have h2 : ((LinearMap.range (T.piApply T.ξ).toLinearMap) : Set T.H) + = (Submodule.span ℂ (Set.range (fun a => (T.π a) T.ξ)) : Set T.H) := by + rw [h1] + congr 1 + exact (Submodule.span_eq _).symm + rw [h1, h2] + -- Now reduce `Submodule.span ℂ (Set.range _)` to the set-builder form used by `T.cyclic`. + have h3 : (Set.range (fun a => (T.π a) T.ξ)) = {T.π a T.ξ | a : A} := by + ext y; simp + rw [h3] + exact h_cyc have hv₁_mem_closure : v₁ ∈ closure (Set.range (fun a => (T.π a) T.ξ)) := by rw [h_dense.closure_eq] exact Set.mem_univ v₁ @@ -420,7 +436,7 @@ lemma trichotomy_from_purity {ψ : PureState A} -- Contradiction have h_phi : ‖φ a - 1‖ < 1/2 := by dsimp only [φ] - rw [ContinuousLinearMap.smul_apply] + change ‖(t : ℂ)⁻¹ • (T.vectorFunctional v₁) a - 1‖ < 1/2 have : (t : ℂ)⁻¹ • T.vectorFunctional v₁ a - 1 = (t : ℂ)⁻¹ * ⟪v₁, (T.π a) v₁ - v₁⟫ := by have ht_ne_c : (t : ℂ) ≠ 0 := Complex.ofReal_ne_zero.mpr h_pos.ne' rw [vectorFunctional_apply] @@ -461,7 +477,8 @@ lemma trichotomy_from_purity {ψ : PureState A} _ = 1 / 2 := by simp have h_chi : ‖χ a‖ < 1/2 := by dsimp only [χ] - rw [ContinuousLinearMap.smul_apply, vectorFunctional_apply, smul_eq_mul] + change ‖(1 - (t : ℂ))⁻¹ • (T.vectorFunctional v₂) a‖ < 1/2 + rw [vectorFunctional_apply, smul_eq_mul] rw [norm_mul, ← Complex.ofReal_one, ← Complex.ofReal_sub, norm_inv, Complex.norm_real, Real.norm_eq_abs, abs_of_pos (by linarith : 0 < 1 - t)] calc (1 - t)⁻¹ * ‖⟪v₂, (T.π a) v₂⟫‖ _ ≤ (1 - t)⁻¹ * (‖v₂‖ * ‖(T.π a) v₂‖) := by diff --git a/QuantumSystem/Algebra/CStarAlgebra/GNS/Representation.lean b/QuantumSystem/Algebra/CStarAlgebra/GNS/Representation.lean index 1aeb752..264a2a2 100644 --- a/QuantumSystem/Algebra/CStarAlgebra/GNS/Representation.lean +++ b/QuantumSystem/Algebra/CStarAlgebra/GNS/Representation.lean @@ -49,7 +49,7 @@ variable {ω : State ℂ A} /-- A submodule `W` of the Hilbert space of a GNS representation is invariant if it is stable under the action of `π(a)` for every `a : A`. -/ def IsInvariant (T : Representation ω) (W : Submodule ℂ T.H) : Prop := - ∀ a : A, W.map (T.π a) ≤ W + ∀ a : A, W.map (T.π a).toLinearMap ≤ W /-- A GNS representation is (topologically) irreducible if the only **closed** invariant submodules are `⊥` and `⊤`. -/ @@ -60,11 +60,13 @@ def IsIrreducible (T : Representation ω) : Prop := (W = ⊥ ∨ W = ⊤) @[simp] lemma isInvariant_bot (T : Representation ω) : T.IsInvariant (⊥ : Submodule ℂ T.H) := by + unfold IsInvariant intro a w hw rcases (show w = 0 from by simpa using hw) with rfl simp @[simp] lemma isInvariant_top (T : Representation ω) : T.IsInvariant (⊤ : Submodule ℂ T.H) := by + unfold IsInvariant intro a w hw simp @@ -115,7 +117,7 @@ private lemma norm_cyclic (T₁ T₂ : Representation ω) (a : A) : exact congr_arg RCLike.re (inner_cyclic T₁ T₂ a a) /-- The canonical correspondence on cyclic orbit vectors: `π₁(a) ξ₁ ↦ π₂(a) ξ₂`. -/ -private def cyclicCorrespondence (_T₁ T₂ : Representation ω) (a : A) : T₂.H := +private noncomputable def cyclicCorrespondence (_T₁ T₂ : Representation ω) (a : A) : T₂.H := T₂.π a T₂.ξ /-- Well-definedness of the cyclic correspondence: equality in the first triplet forces diff --git a/QuantumSystem/Algebra/CStarAlgebra/PureState.lean b/QuantumSystem/Algebra/CStarAlgebra/PureState.lean index 63adbfd..cbbd410 100644 --- a/QuantumSystem/Algebra/CStarAlgebra/PureState.lean +++ b/QuantumSystem/Algebra/CStarAlgebra/PureState.lean @@ -8,11 +8,68 @@ public import QuantumSystem.Algebra.CStarAlgebra.QuasiState @[expose] public section +-- The following typeclass instances are no longer auto-derivable in v4.30 +-- (the priority-90 `Complex.Module` instances depend on `Module R ℝ`, which +-- doesn't fire when the surrounding code expects e.g. `SMulCommClass ℂ ℝ ℂ` +-- through `ContinuousLinearMap.isScalarTower`'s side conditions in module mode). +-- We provide explicit replacements via anonymous constructors. + +private instance smulCommClass_complex_real : SMulCommClass ℂ ℝ ℂ := + ⟨fun a b c => by rw [Complex.real_smul, smul_eq_mul, Complex.real_smul]; ring⟩ variable {A : Type*} [NonUnitalCStarAlgebra A] variable {B : Type*} [CStarAlgebra B] [Nontrivial B] -instance : LocallyConvexSpace ℝ (WeakDual ℂ A) := WeakBilin.locallyConvexSpace +/-- Manual `IsScalarTower ℝ ℂ (A →L[ℂ] ℂ)`. Avoids `ContinuousLinearMap.isScalarTower`, +whose side conditions are not synthesizable in module mode. -/ +private instance instCLMScalarTower : IsScalarTower ℝ ℂ (A →L[ℂ] ℂ) where + smul_assoc r c f := by + apply ContinuousLinearMap.ext + intro x + change (r • c) • f x = r • c • f x + exact smul_assoc r c (f x) + +/-- The same instance transported to `WeakDual ℂ A`. -/ +private instance instWeakDualScalarTower : IsScalarTower ℝ ℂ (WeakDual ℂ A) where + smul_assoc r c f := by + apply ContinuousLinearMap.ext + intro x + change (r • c) • f x = r • c • f x + exact smul_assoc r c (f x) + +/-- `IsScalarTower ℝ ℂ B` for a unital C*-algebra `B`. -/ +private instance instCStarBScalarTower : IsScalarTower ℝ ℂ B where + smul_assoc r c b := by + rw [show (r • c : ℂ) = (r : ℂ) * c from rfl, mul_smul] + rfl + +/-- `IsScalarTower ℝ ℂ (Unitization ℂ A)`. -/ +private instance instUnitScalarTower : IsScalarTower ℝ ℂ (Unitization ℂ A) where + smul_assoc r c x := by + rw [show (r • c : ℂ) = (r : ℂ) * c from rfl, mul_smul] + rfl + +instance : LocallyConvexSpace ℝ (WeakDual ℂ A) := + @WeakBilin.locallyConvexSpace ℂ (A →L[ℂ] ℂ) A _ _ _ _ _ _ _ instCLMScalarTower _ + +/-- `ContinuousSMul ℝ (WeakDual ℂ A)` via the existing `WeakDual.instContinuousSMul`, +provided manually because the implicit `SMulCommClass ℂ ℝ ℂ` is otherwise hidden. -/ +private instance instContinuousSMulRealWeakDual : ContinuousSMul ℝ (WeakDual ℂ A) := + @WeakDual.instContinuousSMul ℂ A _ _ _ _ _ _ _ ℝ _ _ smulCommClass_complex_real _ _ + +/-- `LinearMap.CompatibleSMul` for `restrictScalars` from ℂ to ℝ on `WeakDual ℂ A → ℂ`. +Provided explicitly because the auto-derivation via `IsScalarTower.compatibleSMul` +fails to fire when the side `IsScalarTower ℝ ℂ (WeakDual ℂ A)` instance is private. -/ +private instance instCompatibleSMulWeakDual : + LinearMap.CompatibleSMul (WeakDual ℂ A) ℂ ℝ ℂ where + map_smul := fun f c x => by + have h1 : (c : ℝ) • x = (c : ℂ) • x := by + apply ContinuousLinearMap.ext; intro y + change c • x y = (c : ℂ) • x y + rw [Complex.real_smul, smul_eq_mul] + have h2 : (c : ℝ) • f x = (c : ℂ) • f x := by rw [Complex.real_smul]; rfl + change f ((c : ℝ) • x) = (c : ℝ) • f x + rw [h1, LinearMap.map_smul, h2] /-- A pure state is an extreme point of the quasi-state space, excluding zero. -/ def IsPureState (φ : WeakDual ℂ A) : Prop := @@ -151,7 +208,7 @@ private lemma exists_quasiState_pos_re (b : A) (hb : 0 ≤ b) (hb_ne : b ≠ 0) LinearIsometry.coe_mk, inrLM, LinearMap.coe_mk, AddHom.coe_mk] change ψ (Unitization.inr (star a * a)) = _ rw [Unitization.inr_mul, Unitization.inr_star] - rw [← hr] + exact hr have hφ_norm : ‖φ‖ ≤ 1 := by calc ‖φ‖ ≤ ‖ψ‖ * ‖inrCLM‖ := ContinuousLinearMap.opNorm_comp_le _ _ @@ -198,7 +255,7 @@ lemma norm_eq_one {φ : WeakDual ℂ A} (h : IsPureState φ) : ‖WeakDual.toStr let s' : ℝ := (s : ℝ) * r⁻¹ have hs' : 0 ≤ s' := mul_nonneg s.2 (inv_nonneg.mpr (le_of_lt h_norm_pos)) use ⟨s', hs'⟩ - rw [ContinuousLinearMap.smul_apply] + change (r⁻¹ : ℂ) • φ (star a * a) = ↑↑(⟨s', hs'⟩ : NNReal) simp only [hs, smul_eq_mul] dsimp [s'] -- rewrite the RHS (a real product) as a product in ℂ @@ -232,7 +289,7 @@ lemma norm_eq_one {φ : WeakDual ℂ A} (h : IsPureState φ) : ‖WeakDual.toStr · linarith · linarith · rw [h_eq] - simp + rfl have h_zero_mem : 0 ∈ QuasiStateSpace A := by refine ⟨IsPositive.zero A, ?_⟩ simp only [Set.mem_preimage, Metric.mem_closedBall, dist_zero_right] @@ -274,7 +331,7 @@ noncomputable def toState {φ : WeakDual ℂ A} (h : IsPureState φ) : State ℂ -- φ ≠ 0 means there exists a ≠ 0 such that φ a ≠ 0 have h_exists : ∃ a : A, a ≠ 0 := by by_contra h_all_zero - push_neg at h_all_zero + push Not at h_all_zero have : (0 : WeakDual ℂ A) = φ := by apply WeakDual.toStrongDual.injective ext a @@ -332,13 +389,23 @@ lemma exists_pos_re_of_ne_zero (a : A) (ha : a ≠ 0) : apply AddSubmonoid.subset_closure use a obtain ⟨ω, hω_mem, r, hrpos, hω_eq⟩ := exists_quasiState_pos_re b hb_pos hb_ne_zero - let eval_b : WeakDual ℂ A →L[ℂ] ℂ := { - toFun := fun φ => φ b - map_add' := fun φ ψ => rfl - map_smul' := fun c φ => rfl - cont := WeakDual.eval_continuous b + let l : WeakDual ℂ A →L[ℝ] ℝ := { + toFun := fun φ => (φ b).re + map_add' := fun φ ψ => by + change (φ b + ψ b).re = (φ b).re + (ψ b).re + exact Complex.add_re _ _ + map_smul' := fun c φ => by + change ((c • φ : WeakDual ℂ A) b).re = c • (φ b).re + have hcsmul : (c • φ : WeakDual ℂ A) b = (c : ℂ) * φ b := by + change ((c : ℝ) • φ : WeakDual ℂ A) b = (c : ℂ) * φ b + change (c : ℝ) • φ b = (c : ℂ) * φ b + rw [Complex.real_smul] + rw [hcsmul] + change ((c : ℂ) * φ b).re = c * (φ b).re + rw [Complex.mul_re] + simp + cont := Complex.continuous_re.comp (WeakDual.eval_continuous b) } - let l : WeakDual ℂ A →L[ℝ] ℝ := Complex.reCLM.comp (eval_b.restrictScalars ℝ) let f : WeakDual ℂ A → ℝ := l let M := sSup (f '' QuasiStateSpace A) have hf : ContinuousOn f (QuasiStateSpace A) := Continuous.continuousOn l.continuous |>.mono (Set.subset_univ _) @@ -382,6 +449,8 @@ lemma exists_pos_re_of_ne_zero (a : A) (ha : a ≠ 0) : let F := {x ∈ S | ∀ z ∈ S, l z ≤ l x} have hF_nonempty : F.Nonempty := ⟨φ, hφ_mem, fun z hz => hφ_max hz⟩ have hF_compact : IsCompact F := h_exposed.isCompact (QuasiStateSpace.compact A) + haveI : LocallyConvexSpace ℝ (WeakDual ℂ A) := + @WeakBilin.locallyConvexSpace ℂ (A →L[ℂ] ℂ) A _ _ _ _ _ _ _ instCLMScalarTower _ obtain ⟨ψ, hψ_mem_F, hψ_ext⟩ := hF_compact.extremePoints_nonempty hF_nonempty have hψ_ext_S : IsPureState ψ := by constructor @@ -426,7 +495,7 @@ lemma exists_pos_re_of_ne_zero (a : A) (ha : a ≠ 0) : have : (ψ b).re > 0 := by -- unfold the linear functional `l` on this specific argument have h' := this - dsimp [l, eval_b, ContinuousLinearMap.comp_apply, Complex.reCLM] at h' + dsimp [l, ContinuousLinearMap.comp_apply, Complex.reCLM] at h' exact h' exact this -- Then use positivity (membership in `QuasiStateSpace`) to see the value is real. diff --git a/QuantumSystem/Algebra/CStarAlgebra/QuasiState.lean b/QuantumSystem/Algebra/CStarAlgebra/QuasiState.lean index 047d334..0ac76ac 100644 --- a/QuantumSystem/Algebra/CStarAlgebra/QuasiState.lean +++ b/QuantumSystem/Algebra/CStarAlgebra/QuasiState.lean @@ -24,20 +24,21 @@ lemma convex : Convex ℝ (QuasiStateSpace A) := by apply IsPositive.add · convert IsPositive.smul A hx (c := ⟨a, ha⟩) · convert IsPositive.smul A hy (c := ⟨b, hb⟩) - · -- Unit ball is convex - let f : WeakDual ℂ A →ₗ[ℂ] StrongDual ℂ A := + · -- Unit ball is convex. Use the real-linear identity from `WeakDual ℂ A` to + -- `StrongDual ℂ A` to transport the convexity of the closed ball. + let f : WeakDual ℂ A →ₗ[ℝ] StrongDual ℂ A := { toFun := fun x => x map_add' := fun _ _ => rfl map_smul' := fun _ _ => rfl } - have : (WeakDual.toStrongDual ⁻¹' Metric.closedBall (0 : StrongDual ℂ A) 1) = + have heq : (WeakDual.toStrongDual ⁻¹' Metric.closedBall (0 : StrongDual ℂ A) 1) = f ⁻¹' Metric.closedBall (0 : StrongDual ℂ A) 1 := rfl - rw [this] - apply Convex.linear_preimage (convex_closedBall (0 : StrongDual ℂ A) 1) (f.restrictScalars ℝ) + rw [heq] + exact (convex_closedBall (0 : StrongDual ℂ A) 1).linear_preimage f lemma compact : IsCompact (QuasiStateSpace A) := by rw [QuasiStateSpace, Set.inter_comm] apply IsCompact.inter_right - · exact WeakDual.isCompact_closedBall ℂ (0 : StrongDual ℂ A) 1 + · exact WeakDual.isCompact_closedBall (0 : StrongDual ℂ A) 1 · exact IsPositive.isClosed A lemma non_empty : (0 : WeakDual ℂ A) ∈ QuasiStateSpace A := by diff --git a/QuantumSystem/Algebra/CStarAlgebra/State.lean b/QuantumSystem/Algebra/CStarAlgebra/State.lean index 1fe2cb7..791b3e0 100644 --- a/QuantumSystem/Algebra/CStarAlgebra/State.lean +++ b/QuantumSystem/Algebra/CStarAlgebra/State.lean @@ -341,7 +341,7 @@ lemma real_eval_le_of_le {a b : A} (hab : a ≤ b) : (ω a).re ≤ (ω b).re := lemma kernel_vanish_on_elem (hx : ω (star x * x) = 0) : ω x = 0 := by -- Prove by showing ‖ω(x)‖ < ε for all ε > 0 by_contra h_ne - push_neg at h_ne + push Not at h_ne -- If ω(x) ≠ 0, then ‖ω(x)‖ > 0 have h_pos : 0 < ‖ω x‖ := norm_pos_iff.mpr h_ne -- Set ε = ‖ω(x)‖ / 2 > 0 diff --git a/QuantumSystem/Algebra/CStarAlgebra/State/Continuity.lean b/QuantumSystem/Algebra/CStarAlgebra/State/Continuity.lean index 6a34c31..596262a 100644 --- a/QuantumSystem/Algebra/CStarAlgebra/State/Continuity.lean +++ b/QuantumSystem/Algebra/CStarAlgebra/State/Continuity.lean @@ -125,7 +125,7 @@ lemma norm_le_norm (ω : ContinuousState 𝕜 A) (a : A) : ‖ω a‖ ≤ ‖a _ = ‖a‖ := one_mul _ /-- The canonical map from a continuous state to the weak dual. -/ -def toWeakDual (ω : ContinuousState 𝕜 A) : WeakDual 𝕜 A := +noncomputable def toWeakDual (ω : ContinuousState 𝕜 A) : WeakDual 𝕜 A := StrongDual.toWeakDual ω.toContinuousLinearMap end ContinuousState @@ -158,7 +158,7 @@ lemma toContinuousLinearMap_norm (ω : State 𝕜 A) : ‖ω.toContinuousLinearM rw [← h_norm, norm_def ω] apply csSup_le · by_contra h_empty - push_neg at h_empty + push Not at h_empty have : sSup {r : ℝ | ∃ a : A, a ≠ 0 ∧ r = ‖ω a‖ / ‖a‖} = 0 := by rw [Real.sSup_def] simp [h_empty] diff --git a/QuantumSystem/Algebra/CStarAlgebra/State/Faithful.lean b/QuantumSystem/Algebra/CStarAlgebra/State/Faithful.lean index 3aa1d7d..f9f1af0 100644 --- a/QuantumSystem/Algebra/CStarAlgebra/State/Faithful.lean +++ b/QuantumSystem/Algebra/CStarAlgebra/State/Faithful.lean @@ -36,7 +36,7 @@ lemma IsFaithful.pos_of_nonzero {ω : State ℂ A} (hω : ω.IsFaithful) {a : A} rw [hr'] simp only [Complex.ofReal_re] by_contra h_not_pos - push_neg at h_not_pos + push Not at h_not_pos have hr_nonneg : (0 : ℝ) ≤ r := r.property have hr_zero : (r : ℝ) = 0 := le_antisymm h_not_pos hr_nonneg have h0 : ω (star a * a) = 0 := by rw [hr', hr_zero]; simp diff --git a/QuantumSystem/Analysis/CFC/Diagonal.lean b/QuantumSystem/Analysis/CFC/Diagonal.lean index 4cefc70..4b9b092 100644 --- a/QuantumSystem/Analysis/CFC/Diagonal.lean +++ b/QuantumSystem/Analysis/CFC/Diagonal.lean @@ -49,6 +49,16 @@ lemma cfc_log_diagonal_pos letI : NormedAlgebra ℂ (Matrix m m ℂ) := Matrix.linftyOpNormedAlgebra letI : CStarAlgebra (Matrix m m ℂ) := by simpa [CStarMatrix] using CStarMatrix.instCStarAlgebra (n := m) (A := ℂ) + -- Provide CFC instances on `ℂ` and the Pi type `(m → ℂ)`. + letI : ContinuousFunctionalCalculus ℂ ℂ IsStarNormal := + IsStarNormal.instContinuousFunctionalCalculus + letI : ContinuousFunctionalCalculus ℝ ℂ IsSelfAdjoint := + IsSelfAdjoint.instContinuousFunctionalCalculus + letI : CStarAlgebra (m → ℂ) := inferInstance + letI : ContinuousFunctionalCalculus ℂ (m → ℂ) IsStarNormal := + IsStarNormal.instContinuousFunctionalCalculus + letI : ContinuousFunctionalCalculus ℝ (m → ℂ) IsSelfAdjoint := + IsSelfAdjoint.instContinuousFunctionalCalculus -- Pi self-adjoint let dc : m → ℂ := fun i => (d i : ℂ) have hdc_sa : IsSelfAdjoint dc := by @@ -59,8 +69,10 @@ lemma cfc_log_diagonal_pos map_star' := fun v => by change diagonal (star v) = (diagonal v)ᴴ rw [diagonal_conjTranspose] } - have hφ_cont : Continuous φ := - φ.toAlgHom.toLinearMap.continuous_of_finiteDimensional + have hφ_cont : Continuous φ := by + have : (φ : (m → ℂ) → Matrix m m ℂ) = fun v => diagonal v := rfl + rw [show ⇑φ = fun v => diagonal v from this] + exact Continuous.matrix_diagonal continuous_id have hφ_dc : φ dc = diagonal dc := rfl have hφdc_sa : IsSelfAdjoint (φ dc) := by rw [IsSelfAdjoint, ← map_star φ]; exact congr_arg φ hdc_sa.star_eq @@ -112,6 +124,10 @@ lemma cfc_log_unitary_conj_diagonal letI : NormedAlgebra ℂ (Matrix k k ℂ) := Matrix.linftyOpNormedAlgebra letI : CStarAlgebra (Matrix k k ℂ) := by simpa [CStarMatrix] using CStarMatrix.instCStarAlgebra (n := k) (A := ℂ) + letI : ContinuousFunctionalCalculus ℂ (Matrix k k ℂ) IsStarNormal := + IsStarNormal.instContinuousFunctionalCalculus + letI : ContinuousFunctionalCalculus ℝ (Matrix k k ℂ) IsSelfAdjoint := + IsSelfAdjoint.instContinuousFunctionalCalculus have h_diag_sa : IsSelfAdjoint (diagonal (fun i => ((d i : ℝ) : ℂ))) := by rw [IsSelfAdjoint, star_eq_conjTranspose, diagonal_conjTranspose] congr 1 @@ -138,9 +154,13 @@ lemma cfc_log_unitary_conj_diagonal (diagonal (fun i => ((d i : ℝ) : ℂ)))) := by rw [IsSelfAdjoint, ← map_star (Unitary.conjStarAlgAut ℝ (Matrix k k ℂ) W)] exact congr_arg (Unitary.conjStarAlgAut ℝ (Matrix k k ℂ) W) h_diag_sa.star_eq - have h_cont_conj : Continuous (Unitary.conjStarAlgAut ℝ (Matrix k k ℂ) W) := - LinearMap.continuous_of_finiteDimensional - (Unitary.conjStarAlgAut ℝ (Matrix k k ℂ) W).toAlgEquiv.toLinearMap + have h_cont_conj : Continuous (Unitary.conjStarAlgAut ℝ (Matrix k k ℂ) W) := by + have happly : ∀ x, Unitary.conjStarAlgAut ℝ (Matrix k k ℂ) W x = + (W : Matrix k k ℂ) * x * (W : Matrix k k ℂ)ᴴ := by + intro x; simp [Unitary.conjStarAlgAut_apply, star_eq_conjTranspose] + rw [show (Unitary.conjStarAlgAut ℝ (Matrix k k ℂ) W : Matrix k k ℂ → Matrix k k ℂ) = + fun x => (W : Matrix k k ℂ) * x * (W : Matrix k k ℂ)ᴴ from funext happly] + exact (continuous_const.mul continuous_id).mul continuous_const have h_map := StarAlgHomClass.map_cfc (R := ℝ) (S := ℝ) (Unitary.conjStarAlgAut ℝ (Matrix k k ℂ) W) Real.log (diagonal (fun i => ((d i : ℝ) : ℂ))) h_cont h_cont_conj h_diag_sa h_diag_conj_sa diff --git a/QuantumSystem/Analysis/Entropy/RelativeEntropy.lean b/QuantumSystem/Analysis/Entropy/RelativeEntropy.lean index 01ce6e3..87afa6c 100644 --- a/QuantumSystem/Analysis/Entropy/RelativeEntropy.lean +++ b/QuantumSystem/Analysis/Entropy/RelativeEntropy.lean @@ -881,10 +881,17 @@ private lemma rpow_submatrix_fin_one (A.submatrix (Prod.mk 0) (Prod.mk 0)) ^ p := by classical -- Set up normed algebra and C*-algebra instances + letI : SeminormedAddCommGroup (Matrix (Fin 1 × m) (Fin 1 × m) ℂ) := + Matrix.linftyOpSeminormedAddCommGroup + letI : NormedSpace ℝ (Matrix (Fin 1 × m) (Fin 1 × m) ℂ) := Matrix.linftyOpNormedSpace + letI : IsBoundedSMul ℝ (Matrix (Fin 1 × m) (Fin 1 × m) ℂ) := Matrix.linftyOpIsBoundedSMul letI : NormedRing (Matrix (Fin 1 × m) (Fin 1 × m) ℂ) := Matrix.linftyOpNormedRing letI : NormedAlgebra ℝ (Matrix (Fin 1 × m) (Fin 1 × m) ℂ) := Matrix.linftyOpNormedAlgebra letI : CStarAlgebra (Matrix (Fin 1 × m) (Fin 1 × m) ℂ) := by simpa [CStarMatrix] using CStarMatrix.instCStarAlgebra (n := Fin 1 × m) (A := ℂ) + letI : SeminormedAddCommGroup (Matrix m m ℂ) := Matrix.linftyOpSeminormedAddCommGroup + letI : NormedSpace ℝ (Matrix m m ℂ) := Matrix.linftyOpNormedSpace + letI : IsBoundedSMul ℝ (Matrix m m ℂ) := Matrix.linftyOpIsBoundedSMul letI : NormedRing (Matrix m m ℂ) := Matrix.linftyOpNormedRing letI : NormedAlgebra ℝ (Matrix m m ℂ) := Matrix.linftyOpNormedAlgebra letI : CStarAlgebra (Matrix m m ℂ) := by @@ -914,8 +921,11 @@ private lemma rpow_submatrix_fin_one have hψA_le : 0 ≤ ψ A := by rw [hψ_apply]; simpa [Matrix.le_iff] using hA.submatrix (Prod.mk (0 : Fin 1)) -- Continuity of ψ (finite-dimensional) - have hψ_cont : Continuous ψ := - ψ.toAlgEquiv.toLinearMap.continuous_of_finiteDimensional + haveI : FiniteDimensional ℝ (Matrix (Fin 1 × m) (Fin 1 × m) ℂ) := + Module.Finite.matrix + let f : Matrix (Fin 1 × m) (Fin 1 × m) ℂ →ₗ[ℝ] Matrix m m ℂ := ψ.toAlgEquiv.toLinearMap + have hf_cont : Continuous f := f.continuous_of_finiteDimensional + have hψ_cont : Continuous ψ := hf_cont -- Convert LHS rpow to CFC rw [CFC.rpow_eq_cfc_real (a := A) (ha := hA_le)] -- Rewrite: (cfc f A).sub = ψ (cfc f A) @@ -1035,11 +1045,11 @@ private lemma pinching_inequality_Fs {r : ℕ} [NeZero r] have hPω_psd : Pω.PosSemidef := by apply posSemidef_sum intro k _ - exact (hA_psd k).smul (hw_nn k) + exact (hA_psd k).real_smul (hw_nn k) have hPτ_psd : Pτ.PosSemidef := by apply posSemidef_sum intro k _ - exact (hB_psd k).smul (hw_nn k) + exact (hB_psd k).real_smul (hw_nn k) -- Restriction to blocks 1..r+1 let embed : Fin (r + 1) × m → Fin (r + 2) × m := fun ⟨i, a⟩ => (i.succ, a) let Qω := Pω.submatrix embed embed @@ -1064,12 +1074,24 @@ private lemma pinching_inequality_Fs {r : ℕ} [NeZero r] let τ₀₀ := τ.submatrix (Prod.mk (0 : Fin (r + 2))) (Prod.mk 0) -- Reindex via ψ to show P(ω) = fromBlocks ω₀₀ 0 0 Qω classical + letI : SeminormedAddCommGroup (Matrix (Fin (r + 2) × m) (Fin (r + 2) × m) ℂ) := + Matrix.linftyOpSeminormedAddCommGroup + letI : NormedSpace ℝ (Matrix (Fin (r + 2) × m) (Fin (r + 2) × m) ℂ) := + Matrix.linftyOpNormedSpace + letI : IsBoundedSMul ℝ (Matrix (Fin (r + 2) × m) (Fin (r + 2) × m) ℂ) := + Matrix.linftyOpIsBoundedSMul letI : NormedRing (Matrix (Fin (r + 2) × m) (Fin (r + 2) × m) ℂ) := Matrix.linftyOpNormedRing letI : NormedAlgebra ℝ (Matrix (Fin (r + 2) × m) (Fin (r + 2) × m) ℂ) := Matrix.linftyOpNormedAlgebra letI : CStarAlgebra (Matrix (Fin (r + 2) × m) (Fin (r + 2) × m) ℂ) := by simpa [CStarMatrix] using CStarMatrix.instCStarAlgebra (n := Fin (r + 2) × m) (A := ℂ) + letI : SeminormedAddCommGroup (Matrix (m ⊕ (Fin (r + 1) × m)) (m ⊕ (Fin (r + 1) × m)) ℂ) := + Matrix.linftyOpSeminormedAddCommGroup + letI : NormedSpace ℝ (Matrix (m ⊕ (Fin (r + 1) × m)) (m ⊕ (Fin (r + 1) × m)) ℂ) := + Matrix.linftyOpNormedSpace + letI : IsBoundedSMul ℝ (Matrix (m ⊕ (Fin (r + 1) × m)) (m ⊕ (Fin (r + 1) × m)) ℂ) := + Matrix.linftyOpIsBoundedSMul letI : NormedRing (Matrix m m ℂ) := Matrix.linftyOpNormedRing letI : NormedAlgebra ℝ (Matrix m m ℂ) := Matrix.linftyOpNormedAlgebra letI : CStarAlgebra (Matrix m m ℂ) := by @@ -1126,6 +1148,12 @@ private lemma pinching_inequality_Fs {r : ℕ} [NeZero r] simp only [hψ_eq, Matrix.trace, Matrix.diag, Matrix.submatrix_apply] exact Fintype.sum_equiv e.symm _ _ (fun i => rfl) -- ψ preserves rpow (via CFC) + haveI : FiniteDimensional ℝ (Matrix (Fin (r + 2) × m) (Fin (r + 2) × m) ℂ) := + Module.Finite.matrix + let ψf : Matrix (Fin (r + 2) × m) (Fin (r + 2) × m) ℂ →ₗ[ℝ] + Matrix (m ⊕ (Fin (r + 1) × m)) (m ⊕ (Fin (r + 1) × m)) ℂ := ψ.toAlgEquiv.toLinearMap + have hψ_cont : Continuous ψ := (ψf.continuous_of_finiteDimensional : + Continuous (ψf : Matrix (Fin (r + 2) × m) (Fin (r + 2) × m) ℂ → _)) have hψ_rpow : ∀ (M : Matrix (Fin (r + 2) × m) (Fin (r + 2) × m) ℂ), M.PosSemidef → ∀ p : ℝ, 0 < p → ψ (M ^ p) = (ψ M) ^ p := by intro M hM p hp @@ -1139,7 +1167,7 @@ private lemma pinching_inequality_Fs {r : ℕ} [NeZero r] rw [CFC.rpow_eq_cfc_real (ha := hM_le), CFC.rpow_eq_cfc_real (ha := hψM_le)] rw [StarAlgHomClass.map_cfc (R := ℝ) (S := ℝ) ψ _ M ((Real.continuous_rpow_const (by linarith)).continuousOn) - (ψ.toAlgEquiv.toLinearMap.continuous_of_finiteDimensional) + hψ_cont hM_sa hψM_sa] -- Trace splits into block 0 + remaining blocks have htrace_split : @@ -1420,13 +1448,19 @@ private lemma suppSubset_mix (p : ℝ) (hp : 0 ≤ p) (hp1 : 0 ≤ 1 - p) : suppSubset (p • A₁ + (1 - p) • A₂) (p • B₁ + (1 - p) • B₂) := by intro v hv - simp only [Matrix.add_mulVec, Matrix.smul_mulVec] at hv + rw [Matrix.add_mulVec, show (p • B₁) *ᵥ v = p • B₁ *ᵥ v from Matrix.smul_mulVec _ _ _, + show ((1 - p) • B₂) *ᵥ v = (1 - p) • B₂ *ᵥ v from Matrix.smul_mulVec _ _ _] at hv have h₁ : 0 ≤ (star v ⬝ᵥ B₁.mulVec v).re := hB₁.re_dotProduct_nonneg v have h₂ : 0 ≤ (star v ⬝ᵥ B₂.mulVec v).re := hB₂.re_dotProduct_nonneg v have hinner_sum : p * (star v ⬝ᵥ B₁.mulVec v).re + (1 - p) * (star v ⬝ᵥ B₂.mulVec v).re = 0 := by + have hsmul₁ : star v ⬝ᵥ p • B₁.mulVec v = p • (star v ⬝ᵥ B₁.mulVec v) := + dotProduct_smul p (star v) (B₁.mulVec v) + have hsmul₂ : star v ⬝ᵥ (1 - p) • B₂.mulVec v = (1 - p) • (star v ⬝ᵥ B₂.mulVec v) := + dotProduct_smul (1 - p) (star v) (B₂.mulVec v) have h : p * (star v ⬝ᵥ B₁.mulVec v).re + (1 - p) * (star v ⬝ᵥ B₂.mulVec v).re = (star v ⬝ᵥ (p • B₁.mulVec v + (1 - p) • B₂.mulVec v)).re := by - simp [dotProduct_add, dotProduct_smul] + rw [dotProduct_add, hsmul₁, hsmul₂] + simp [Complex.real_smul, Complex.add_re, Complex.mul_re] rw [h, hv]; simp have hpB₁ : p * (star v ⬝ᵥ B₁.mulVec v).re = 0 := by nlinarith [mul_nonneg hp h₁, mul_nonneg hp1 h₂] @@ -1434,13 +1468,15 @@ private lemma suppSubset_mix nlinarith [mul_nonneg hp h₁, mul_nonneg hp1 h₂] have hpA₁ : p • A₁.mulVec v = 0 := by rcases mul_eq_zero.mp hpB₁ with hp0 | h₁0 - · simp [hp0] - · simp [hsup₁ v (mulVec_eq_zero_of_re_inner_zero hB₁ v h₁0)] + · subst hp0; exact zero_smul ℝ _ + · rw [hsup₁ v (mulVec_eq_zero_of_re_inner_zero hB₁ v h₁0)]; exact smul_zero _ have h1pA₂ : (1 - p) • A₂.mulVec v = 0 := by rcases mul_eq_zero.mp h1pB₂ with hp10 | h₂0 - · simp [hp10] - · simp [hsup₂ v (mulVec_eq_zero_of_re_inner_zero hB₂ v h₂0)] - simp [Matrix.add_mulVec, Matrix.smul_mulVec, hpA₁, h1pA₂] + · rw [hp10]; exact zero_smul ℝ _ + · rw [hsup₂ v (mulVec_eq_zero_of_re_inner_zero hB₂ v h₂0)]; exact smul_zero _ + rw [Matrix.add_mulVec, show (p • A₁) *ᵥ v = p • A₁ *ᵥ v from Matrix.smul_mulVec _ _ _, + show ((1 - p) • A₂) *ᵥ v = (1 - p) • A₂ *ᵥ v from Matrix.smul_mulVec _ _ _, + hpA₁, h1pA₂, add_zero] omit [DecidableEq n] [DecidableEq m] in /-- Support subset is preserved by a single Kraus conjugation K ρ K†. @@ -1549,8 +1585,10 @@ theorem relativeEntropy_jointly_convex -- Handle boundary cases p = 0 and p = 1 rcases hp.eq_or_lt' with rfl | hp0 · -- p = 0: mixture = ρ₂, σ₂; RHS = 0 + D₂ = D₂ - have hρ_eq : ρ_mix = ρ₂ := DensityMatrix.ext (by simp [ρ_mix, DensityMatrix.mix]) - have hσ_eq : σ_mix = σ₂ := DensityMatrix.ext (by simp [σ_mix, DensityMatrix.mix]) + have hρ_eq : ρ_mix = ρ₂ := DensityMatrix.ext (by + simp only [ρ_mix, DensityMatrix.mix, sub_zero]; module) + have hσ_eq : σ_mix = σ₂ := DensityMatrix.ext (by + simp only [σ_mix, DensityMatrix.mix, sub_zero]; module) rw [hρ_eq, hσ_eq]; simp [relativeEntropy] rcases hp1.lt_or_eq with hp1' | rfl · -- 0 < p < 1: handle the three sub-cases @@ -1647,8 +1685,10 @@ theorem relativeEntropy_jointly_convex (EReal.mul_nonneg (by norm_cast) (relativeEntropy_nonneg ρ₁ σ₁))))] exact le_top · -- p = 1: mixture = ρ₁, σ₁; RHS = D₁ + 0 = D₁ - have hρ_eq : ρ_mix = ρ₁ := DensityMatrix.ext (by simp [ρ_mix, DensityMatrix.mix]) - have hσ_eq : σ_mix = σ₁ := DensityMatrix.ext (by simp [σ_mix, DensityMatrix.mix]) + have hρ_eq : ρ_mix = ρ₁ := DensityMatrix.ext (by + simp only [ρ_mix, DensityMatrix.mix, sub_self]; module) + have hσ_eq : σ_mix = σ₁ := DensityMatrix.ext (by + simp only [σ_mix, DensityMatrix.mix, sub_self]; module) rw [hρ_eq, hσ_eq] have h1sub1 : (1 : EReal) - 1 = 0 := EReal.sub_self (EReal.coe_ne_top 1) (EReal.coe_ne_bot 1) diff --git a/QuantumSystem/Analysis/Entropy/VonNeumannEntropy.lean b/QuantumSystem/Analysis/Entropy/VonNeumannEntropy.lean index 552666a..fdbdd62 100644 --- a/QuantumSystem/Analysis/Entropy/VonNeumannEntropy.lean +++ b/QuantumSystem/Analysis/Entropy/VonNeumannEntropy.lean @@ -32,7 +32,7 @@ theorem entropyFun_nonneg {x : ℝ} (hx : 0 ≤ x) (hx1 : x ≤ 1) : 0 ≤ entro unfold entropyFun split_ifs with hle · exact le_refl 0 - · push_neg at hle + · push Not at hle have hlog : Real.log x ≤ 0 := Real.log_nonpos hx hx1 nlinarith [hle, hlog] @@ -207,7 +207,8 @@ lemma trace_rpow_concave (A B : Matrix n n ℂ) (hA : A.PosSemidef) (hB : B.PosS (p : ℝ) (hp : 0 ≤ p) (hp1 : p ≤ 1) (s : ℝ) (hs0 : 0 < s) (hs1 : s ≤ 1) : p * (Tr (A ^ s)).re + (1 - p) * (Tr (B ^ s)).re ≤ (Tr ((p • A + (1 - p) • B) ^ s)).re := by - have hpsd_mix : (p • A + (1 - p) • B).PosSemidef := (hA.smul hp).add (hB.smul (by linarith)) + have hpsd_mix : (p • A + (1 - p) • B).PosSemidef := + (hA.real_smul hp).add (hB.real_smul (by linarith)) have hlowner := rpow_isLownerConcave hs0 hs1 n A B hA hB p hp hp1 hpsd_mix.1 simp only [] at hlowner have hfunc_eq : (fun x : ℝ => ((-x ^ s : ℝ) : ℂ)) = (fun x : ℝ => -(((x ^ s : ℝ) : ℂ))) := by @@ -218,13 +219,17 @@ lemma trace_rpow_concave (A B : Matrix n n ℂ) (hA : A.PosSemidef) (hB : B.PosS matrixFunction_rpow_eq hA, matrixFunction_rpow_eq hB, matrixFunction_rpow_eq hpsd_mix] at hlowner have hlowner' : p • A ^ s + (1 - p) • B ^ s ≤ (p • A + (1 - p) • B) ^ s := by have heq : p • -A ^ s + (1 - p) • -B ^ s = -(p • A ^ s + (1 - p) • B ^ s) := by - simp [smul_neg] - abel + have h1 : p • -A ^ s = -(p • A ^ s) := smul_neg p (A ^ s) + have h2 : (1 - p) • -B ^ s = -((1 - p) • B ^ s) := smul_neg (1 - p) (B ^ s) + rw [h1, h2, ← neg_add] rw [heq] at hlowner rwa [neg_le_neg_iff] at hlowner rw [Matrix.le_iff] at hlowner' have htrace := (Complex.nonneg_iff.mp hlowner'.trace_nonneg).1 - rw [Matrix.trace_sub, Matrix.trace_add, Matrix.trace_smul, Matrix.trace_smul] at htrace + have htr1 : Tr (p • A ^ s) = (p : ℝ) • Tr (A ^ s) := Matrix.trace_smul (p : ℝ) (A ^ s) + have htr2 : Tr ((1 - p) • B ^ s) = (1 - p : ℝ) • Tr (B ^ s) := + Matrix.trace_smul (1 - p : ℝ) (B ^ s) + rw [Matrix.trace_sub, Matrix.trace_add, htr1, htr2] at htrace simp only [Complex.sub_re, Complex.add_re, Complex.real_smul, Complex.mul_re, Complex.ofReal_re, Complex.ofReal_im] at htrace linarith @@ -305,7 +310,7 @@ theorem vonNeumannEntropy_concave (ρ₁ ρ₂ : DensityMatrix n) (p : ℝ) (hp unfold entropyFun split_ifs with h · simp [le_antisymm h (ρ_mix.eigenvalues_nonneg i)] - · push_neg at h + · push Not at h ring have h₁_eq : ∑ i, ρ₁.isHermitian.eigenvalues i * Real.log (ρ₁.isHermitian.eigenvalues i) = -vonNeumannEntropy ρ₁ := by @@ -315,7 +320,7 @@ theorem vonNeumannEntropy_concave (ρ₁ ρ₂ : DensityMatrix n) (p : ℝ) (hp unfold entropyFun split_ifs with h · simp [le_antisymm h (ρ₁.eigenvalues_nonneg i)] - · push_neg at h + · push Not at h ring have h₂_eq : ∑ i, ρ₂.isHermitian.eigenvalues i * Real.log (ρ₂.isHermitian.eigenvalues i) = -vonNeumannEntropy ρ₂ := by @@ -325,7 +330,7 @@ theorem vonNeumannEntropy_concave (ρ₁ ρ₂ : DensityMatrix n) (p : ℝ) (hp unfold entropyFun split_ifs with h · simp [le_antisymm h (ρ₂.eigenvalues_nonneg i)] - · push_neg at h + · push Not at h ring rw [hmix_eq, h₁_eq, h₂_eq] at hderiv_g_nonpos linarith diff --git a/QuantumSystem/Analysis/Matrix/Effros.lean b/QuantumSystem/Analysis/Matrix/Effros.lean index dfbb6d4..d7738b4 100644 --- a/QuantumSystem/Analysis/Matrix/Effros.lean +++ b/QuantumSystem/Analysis/Matrix/Effros.lean @@ -442,12 +442,18 @@ noncomputable def leftMulStarAlgHom {m : Type*} [Fintype m] [DecidableEq m] : lemma leftMulStarAlgHom_continuous {m : Type*} [Fintype m] [DecidableEq m] : Continuous (leftMulStarAlgHom : Matrix m m ℂ →⋆ₐ[ℝ] Matrix (m × m) (m × m) ℂ) := by -- leftMulMatrix is a linear map between finite-dimensional normed spaces, hence continuous - letI : NormedRing (Matrix m m ℂ) := Matrix.linftyOpNormedRing - letI : NormedAlgebra ℝ (Matrix m m ℂ) := Matrix.linftyOpNormedAlgebra - letI : NormedRing (Matrix (m × m) (m × m) ℂ) := Matrix.linftyOpNormedRing - letI : NormedAlgebra ℝ (Matrix (m × m) (m × m) ℂ) := Matrix.linftyOpNormedAlgebra - change Continuous (leftMulStarAlgHom.toAlgHom.toLinearMap : Matrix m m ℂ →ₗ[ℝ] Matrix (m × m) (m × m) ℂ) - exact leftMulStarAlgHom.toAlgHom.toLinearMap.continuous_of_finiteDimensional + letI : SeminormedAddCommGroup (Matrix m m ℂ) := Matrix.linftyOpSeminormedAddCommGroup + letI : NormedSpace ℝ (Matrix m m ℂ) := Matrix.linftyOpNormedSpace + letI : IsBoundedSMul ℝ (Matrix m m ℂ) := Matrix.linftyOpIsBoundedSMul + letI : SeminormedAddCommGroup (Matrix (m × m) (m × m) ℂ) := + Matrix.linftyOpSeminormedAddCommGroup + letI : NormedSpace ℝ (Matrix (m × m) (m × m) ℂ) := Matrix.linftyOpNormedSpace + letI : IsBoundedSMul ℝ (Matrix (m × m) (m × m) ℂ) := Matrix.linftyOpIsBoundedSMul + haveI : FiniteDimensional ℝ (Matrix m m ℂ) := inferInstance + let f : Matrix m m ℂ →ₗ[ℝ] Matrix (m × m) (m × m) ℂ := + (leftMulStarAlgHom : Matrix m m ℂ →⋆ₐ[ℝ] _).toAlgHom.toLinearMap + change Continuous (f : Matrix m m ℂ → _) + exact f.continuous_of_finiteDimensional /-- CFC commutes with leftMulMatrix: for self-adjoint A and continuous f, leftMulMatrix (cfc f A) = cfc f (leftMulMatrix A). -/ @@ -523,11 +529,18 @@ noncomputable def rightMulConjTransposeStarAlgHom {m : Type*} [Fintype m] [Decid lemma rightMulConjTransposeStarAlgHom_continuous {m : Type*} [Fintype m] [DecidableEq m] : Continuous (rightMulConjTransposeStarAlgHom : Matrix m m ℂ →⋆ₐ[ℝ] Matrix (m × m) (m × m) ℂ) := by - letI : NormedRing (Matrix m m ℂ) := Matrix.linftyOpNormedRing - letI : NormedAlgebra ℝ (Matrix m m ℂ) := Matrix.linftyOpNormedAlgebra - letI : NormedRing (Matrix (m × m) (m × m) ℂ) := Matrix.linftyOpNormedRing - letI : NormedAlgebra ℝ (Matrix (m × m) (m × m) ℂ) := Matrix.linftyOpNormedAlgebra - exact rightMulConjTransposeStarAlgHom.toAlgHom.toLinearMap.continuous_of_finiteDimensional + letI : SeminormedAddCommGroup (Matrix m m ℂ) := Matrix.linftyOpSeminormedAddCommGroup + letI : NormedSpace ℝ (Matrix m m ℂ) := Matrix.linftyOpNormedSpace + letI : IsBoundedSMul ℝ (Matrix m m ℂ) := Matrix.linftyOpIsBoundedSMul + letI : SeminormedAddCommGroup (Matrix (m × m) (m × m) ℂ) := + Matrix.linftyOpSeminormedAddCommGroup + letI : NormedSpace ℝ (Matrix (m × m) (m × m) ℂ) := Matrix.linftyOpNormedSpace + letI : IsBoundedSMul ℝ (Matrix (m × m) (m × m) ℂ) := Matrix.linftyOpIsBoundedSMul + haveI : FiniteDimensional ℝ (Matrix m m ℂ) := inferInstance + let f : Matrix m m ℂ →ₗ[ℝ] Matrix (m × m) (m × m) ℂ := + (rightMulConjTransposeStarAlgHom : Matrix m m ℂ →⋆ₐ[ℝ] _).toAlgHom.toLinearMap + change Continuous (f : Matrix m m ℂ → _) + exact f.continuous_of_finiteDimensional /-- CFC commutes with rightMulMatrix for self-adjoint (Hermitian) matrices. Uses the `rightMulConjTransposeStarAlgHom` to transport CFC via `StarAlgHom.map_cfc`. @@ -710,7 +723,7 @@ theorem matrixPerspective_joint_convex.{v} {m : Type v} [Fintype m] [DecidableEq (hR₁ : R₁.PosDef) (hR₂ : R₂.PosDef) {w₁ w₂ : ℝ} (hw₁ : 0 ≤ w₁) (hw₂ : 0 ≤ w₂) (hw : w₁ + w₂ = 1) : matrixPerspective f (w₁ • L₁ + w₂ • L₂) (w₁ • R₁ + w₂ • R₂) - ((hL₁.smul hw₁).add (hL₂.smul hw₂)) + ((hL₁.real_smul hw₁).add (hL₂.real_smul hw₂)) (PosDef.convex_comb_nonneg hR₁ hR₂ hw₁ hw₂ hw) ≤ w₁ • matrixPerspective f L₁ R₁ hL₁ hR₁ + w₂ • matrixPerspective f L₂ R₂ hL₂ hR₂ := by @@ -737,9 +750,11 @@ theorem matrixPerspective_joint_convex.{v} {m : Type v} [Fintype m] [DecidableEq have hR₂half_herm : R₂half.IsHermitian := matrixSqrt_isHermitian hR₂.posSemidef have hRhalf_herm : Rhalf.IsHermitian := matrixSqrt_isHermitian hR.posSemidef have hA₁_adj : A₁ᴴ = (Real.sqrt w₁ : ℂ) • (Rinv * R₁half) := by - simp [A₁, hRinv_herm.eq, hR₁half_herm.eq, Matrix.conjTranspose_mul] + simp only [A₁, Matrix.conjTranspose_smul, Matrix.conjTranspose_mul, + hRinv_herm.eq, hR₁half_herm.eq, Complex.star_def, Complex.conj_ofReal] have hA₂_adj : A₂ᴴ = (Real.sqrt w₂ : ℂ) • (Rinv * R₂half) := by - simp [A₂, hRinv_herm.eq, hR₂half_herm.eq, Matrix.conjTranspose_mul] + simp only [A₂, Matrix.conjTranspose_smul, Matrix.conjTranspose_mul, + hRinv_herm.eq, hR₂half_herm.eq, Complex.star_def, Complex.conj_ofReal] have hsqrt₁_real : Real.sqrt w₁ * Real.sqrt w₁ = w₁ := Real.mul_self_sqrt hw₁ have hsqrt₂_real : Real.sqrt w₂ * Real.sqrt w₂ = w₂ := Real.mul_self_sqrt hw₂ have hsqrt₁ : (Real.sqrt w₁ : ℂ) * (Real.sqrt w₁ : ℂ) = (w₁ : ℂ) := by @@ -761,7 +776,7 @@ theorem matrixPerspective_joint_convex.{v} {m : Type v} [Fintype m] [DecidableEq _ = Rinv * ((w₁ : ℂ) • R₁ + (w₂ : ℂ) • R₂) * Rinv := by simp [mul_add, add_mul, mul_assoc] _ = Rinv * R * Rinv := by - simp [R] + congr 2 have hAB : A₁ᴴ * A₁ + A₂ᴴ * A₂ ≤ (1 : Matrix m m ℂ) := by have hRinv_mul : Rinv * R * Rinv = (1 : Matrix m m ℂ) := by simpa [Rinv, R] using matrixInvSqrt_mul_self hR @@ -810,7 +825,8 @@ theorem matrixPerspective_joint_convex.{v} {m : Type v} [Fintype m] [DecidableEq _ = Rinv * ((w₁ : ℂ) • L₁ + (w₂ : ℂ) • L₂) * Rinv := by simp [mul_add, add_mul, mul_assoc] _ = Rinvᴴ * L * Rinv := by - simp [L, hRinv_herm.eq] + rw [hRinv_herm.eq] + congr 2 -- Cancellation lemmas for Rhalf and Rinv have hRhalf_Rinv : Rhalf * Rinv = 1 := by simpa [Rhalf, Rinv] using matrixSqrt_mul_matrixInvSqrt hR @@ -830,11 +846,11 @@ theorem matrixPerspective_joint_convex.{v} {m : Type v} [Fintype m] [DecidableEq (A₁ᴴ * T₁ * A₁ + A₂ᴴ * T₂ * A₂) hC = matrixFunction (fun x => (f x : ℂ)) (Rinvᴴ * L * Rinv) (isHermitian_conjTranspose_mul_mul (B := Rinv) (A := L) - ((hL₁.smul hw₁).add (hL₂.smul hw₂)).1) := + ((hL₁.real_smul hw₁).add (hL₂.real_smul hw₂)).1) := matrixFunction_congr (fun x => (f x : ℂ)) hC _ hinner -- Final step: apply sandwich equation and conclude have hfinal : - matrixPerspective f L R ((hL₁.smul hw₁).add (hL₂.smul hw₂)) hR ≤ + matrixPerspective f L R ((hL₁.real_smul hw₁).add (hL₂.real_smul hw₂)) hR ≤ w₁ • matrixPerspective f L₁ R₁ hL₁ hR₁ + w₂ • matrixPerspective f L₂ R₂ hL₂ hR₂ := by rw [Matrix.le_iff] @@ -853,7 +869,7 @@ lemma signMatrix_mem_unitary {m : Type*} [Fintype m] [DecidableEq m] : fromBlocks_multiply, fromBlocks_one]) /-- The sign matrix is self-adjoint: Σ* = Σ. -/ -lemma signMatrix_star_eq {m : Type*} [Fintype m] [DecidableEq m] : +lemma signMatrix_star_eq {m : Type*} [DecidableEq m] : star (fromBlocks (1 : Matrix m m ℂ) 0 0 (-1 : Matrix m m ℂ)) = fromBlocks (1 : Matrix m m ℂ) 0 0 (-1 : Matrix m m ℂ) := by simp [star_eq_conjTranspose, fromBlocks_conjTranspose] @@ -921,7 +937,8 @@ lemma perspective_inner_eq_mul_inv {n : Type*} [Fintype n] [DecidableEq n] rw [← CFC.rpow_add hRunit (x := (-1 / 2 : ℝ)) (y := (-1 / 2 : ℝ))] norm_num -- goal: R ^ (-1 : ℝ) * R = 1 - have := CFC.rpow_neg_mul_rpow (1 : ℝ) hRunit hR0 + have hRpos : IsStrictlyPositive R := IsUnit.isStrictlyPositive hRunit hR0 + have := CFC.rpow_neg_mul_rpow (1 : ℝ) hRpos rwa [CFC.rpow_one R hR0] at this have hdet : IsUnit R.det := (Matrix.isUnit_iff_isUnit_det R).mp hRunit diff --git a/QuantumSystem/Analysis/Matrix/HermitianFunctionalCalculus.lean b/QuantumSystem/Analysis/Matrix/HermitianFunctionalCalculus.lean index 4c6b5d7..50f7dad 100644 --- a/QuantumSystem/Analysis/Matrix/HermitianFunctionalCalculus.lean +++ b/QuantumSystem/Analysis/Matrix/HermitianFunctionalCalculus.lean @@ -1,6 +1,7 @@ module public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute +public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi public import Mathlib.Analysis.CStarAlgebra.CStarMatrix public import Mathlib.LinearAlgebra.Lagrange public import QuantumSystem.ForMathlib.Analysis.Matrix.Basic @@ -208,10 +209,15 @@ lemma matrixFunction_add_const {m : Type*} [Fintype m] [DecidableEq m] diagonal (fun i => ((hA.eigenvalues i + t : ℝ) : ℂ)) = diagonal (fun i => (hA.eigenvalues i : ℂ)) + (t : ℂ) • 1 := by ext i j + change (diagonal (fun i => ((hA.eigenvalues i + t : ℝ) : ℂ))) i j = + (diagonal (fun i => (hA.eigenvalues i : ℂ))) i j + ((t : ℂ) • (1 : Matrix m m ℂ)) i j by_cases h : i = j · subst h - simp - · simp [h] + rw [Matrix.diagonal_apply_eq, Matrix.diagonal_apply_eq, Matrix.smul_apply, + Matrix.one_apply_eq, smul_eq_mul, mul_one] + push_cast; ring + · rw [Matrix.diagonal_apply_ne _ h, Matrix.diagonal_apply_ne _ h, Matrix.smul_apply, + Matrix.one_apply_ne h, smul_zero, add_zero] rw [hdiag] simp only [Matrix.mul_add, Matrix.add_mul] have hU : U * Uᴴ = 1 := by @@ -523,8 +529,20 @@ theorem matrixLog_map_starAlgEquiv {m n : Type*} [Fintype m] [DecidableEq m] { toAlgHom := (φ.toAlgEquiv.restrictScalars ℝ).toAlgHom map_star' := fun X => map_star φ X } have h_ψ_apply : ∀ X, ψ X = φ X := fun _ => rfl - have hψ_cont : Continuous ψ := - ψ.toAlgHom.toLinearMap.continuous_of_finiteDimensional + have hψ_cont : Continuous ψ := by + -- ψ x = φ x, so it suffices to show φ is continuous. + -- Continuity follows entrywise: each entry `(φ A) i j` is a ℂ-linear functional in `A`, + -- and ℂ-linear maps on a finite-dimensional ℂ-space are automatically continuous. + have hcont_φ : Continuous (φ : Matrix m m ℂ → Matrix n n ℂ) := by + refine continuous_matrix fun i j => ?_ + -- The entry map is ℂ-linear; package it as a `LinearMap`. + let g : Matrix m m ℂ →ₗ[ℂ] ℂ := + { toFun := fun A => (φ A) i j + map_add' := fun A B => by simp + map_smul' := fun c A => by simp } + change Continuous fun A => g A + exact g.continuous_of_finiteDimensional + exact hcont_φ have hM_sa : IsSelfAdjoint M := hM.1 have hψM_sa : IsSelfAdjoint (ψ M) := by rw [IsSelfAdjoint, ← map_star ψ] @@ -761,8 +779,13 @@ lemma cfc_unitary_conjugation' {m : Type*} [Fintype m] [DecidableEq m] cfc f ((U : Matrix m m ℂ) * M * star (U : Matrix m m ℂ)) := by change (Unitary.conjStarAlgAut ℝ _ U) (cfc f M) = cfc f ((Unitary.conjStarAlgAut ℝ _ U) M) - have hcont : Continuous (Unitary.conjStarAlgAut ℝ (Matrix m m ℂ) U) := - (Unitary.conjStarAlgAut ℝ (Matrix m m ℂ) U).toAlgEquiv.toLinearMap.continuous_of_finiteDimensional + have hcont : Continuous (Unitary.conjStarAlgAut ℝ (Matrix m m ℂ) U) := by + have happly : ∀ x, Unitary.conjStarAlgAut ℝ (Matrix m m ℂ) U x = + (U : Matrix m m ℂ) * x * (U : Matrix m m ℂ)ᴴ := by + intro x; simp [Unitary.conjStarAlgAut_apply, star_eq_conjTranspose] + rw [show (Unitary.conjStarAlgAut ℝ (Matrix m m ℂ) U : Matrix m m ℂ → Matrix m m ℂ) = + fun x => (U : Matrix m m ℂ) * x * (U : Matrix m m ℂ)ᴴ from funext happly] + exact (continuous_const.mul continuous_id).mul continuous_const exact StarAlgHomClass.map_cfc (Unitary.conjStarAlgAut ℝ _ U) f M hf hcont hM /-- Block diagonal embedding as a star algebra homomorphism. @@ -792,6 +815,13 @@ lemma cfc_fromBlocks_diag {m : Type*} [Fintype m] [DecidableEq m] letI : NormedAlgebra ℂ (Matrix m m ℂ) := Matrix.linftyOpNormedAlgebra letI : CStarAlgebra (Matrix m m ℂ) := by simpa [CStarMatrix] using CStarMatrix.instCStarAlgebra (n := m) (A := ℂ) + letI : ContinuousFunctionalCalculus ℂ (Matrix m m ℂ) IsStarNormal := + IsStarNormal.instContinuousFunctionalCalculus + letI : CStarAlgebra (Matrix m m ℂ × Matrix m m ℂ) := inferInstance + letI : ContinuousFunctionalCalculus ℂ (Matrix m m ℂ × Matrix m m ℂ) IsStarNormal := + IsStarNormal.instContinuousFunctionalCalculus + letI : ContinuousFunctionalCalculus ℝ (Matrix m m ℂ × Matrix m m ℂ) IsSelfAdjoint := + IsSelfAdjoint.instContinuousFunctionalCalculus have hcont : Continuous (blockDiagEmbed m) := by change Continuous fun p : Matrix m m ℂ × Matrix m m ℂ => fromBlocks p.1 0 0 p.2 fun_prop @@ -836,6 +866,15 @@ lemma cfc_fromBlocks_diag' {n m : Type*} [Fintype n] [DecidableEq n] [Fintype m] letI : NormedAlgebra ℂ (Matrix m m ℂ) := Matrix.linftyOpNormedAlgebra letI : CStarAlgebra (Matrix m m ℂ) := by simpa [CStarMatrix] using CStarMatrix.instCStarAlgebra (n := m) (A := ℂ) + letI : ContinuousFunctionalCalculus ℂ (Matrix n n ℂ) IsStarNormal := + IsStarNormal.instContinuousFunctionalCalculus + letI : ContinuousFunctionalCalculus ℂ (Matrix m m ℂ) IsStarNormal := + IsStarNormal.instContinuousFunctionalCalculus + letI : CStarAlgebra (Matrix n n ℂ × Matrix m m ℂ) := inferInstance + letI : ContinuousFunctionalCalculus ℂ (Matrix n n ℂ × Matrix m m ℂ) IsStarNormal := + IsStarNormal.instContinuousFunctionalCalculus + letI : ContinuousFunctionalCalculus ℝ (Matrix n n ℂ × Matrix m m ℂ) IsSelfAdjoint := + IsSelfAdjoint.instContinuousFunctionalCalculus have hcont : Continuous (blockDiagEmbed' n m) := by change Continuous fun p : Matrix n n ℂ × Matrix m m ℂ => fromBlocks p.1 0 0 p.2 fun_prop @@ -949,7 +988,7 @@ lemma eigenvalues_compression_subset {n m : Type*} intro lam hlam by_contra h_not_spec rw [spectrum.mem_iff] at h_not_spec hlam - push_neg at h_not_spec + push Not at h_not_spec -- h_not_spec : IsUnit (algebraMap ℂ (Matrix n n ℂ) lam - M) -- The compression V†(λI - M)V = (λI - V†MV) and inverse transfers -- This is standard linear algebra: V†AV invertible iff A restricted to range(V) is invertible diff --git a/QuantumSystem/Analysis/Matrix/LiebConcavity.lean b/QuantumSystem/Analysis/Matrix/LiebConcavity.lean index 5820f07..46b111b 100644 --- a/QuantumSystem/Analysis/Matrix/LiebConcavity.lean +++ b/QuantumSystem/Analysis/Matrix/LiebConcavity.lean @@ -180,8 +180,8 @@ private lemma lieb_concavity_effros {m : Type*} [Fintype m] [DecidableEq m] w₁ * (liebJointFunction K p A₁ hA₁.posSemidef B₁ hB₁.posSemidef).re + w₂ * (liebJointFunction K p A₂ hA₂.posSemidef B₂ hB₂.posSemidef).re ≤ (liebJointFunction K p - (w₁ • A₁ + w₂ • A₂) ((hA₁.posSemidef.smul hw₁).add (hA₂.posSemidef.smul hw₂)) - (w₁ • B₁ + w₂ • B₂) ((hB₁.posSemidef.smul hw₁).add (hB₂.posSemidef.smul hw₂))).re := by + (w₁ • A₁ + w₂ • A₂) ((hA₁.posSemidef.real_smul hw₁).add (hA₂.posSemidef.real_smul hw₂)) + (w₁ • B₁ + w₂ • B₂) ((hB₁.posSemidef.real_smul hw₁).add (hB₂.posSemidef.real_smul hw₂))).re := by classical /- Proof by Effros's Matrix Perspective Approach -/ -- 1. Setup the function f(x) = -x^p, which is Matrix Convex. @@ -212,7 +212,8 @@ private lemma lieb_concavity_effros {m : Type*} [Fintype m] [DecidableEq m] -- We assume the identity: ⟨matrixPerspective f L R K†, K†⟩_HS = -Lieb(A, B). let term1 := matrixPerspective f L₁ R₁ hL₁_psd hR₁_pd let term2 := matrixPerspective f L₂ R₂ hL₂_psd hR₂_pd - let term_comb := matrixPerspective f L R ((hL₁_psd.smul hw₁).add (hL₂_psd.smul hw₂)) hR_pd + let term_comb := + matrixPerspective f L R ((hL₁_psd.real_smul hw₁).add (hL₂_psd.real_smul hw₂)) hR_pd -- The inequality is term_comb ≤ w₁ term1 + w₂ term2 -- Apply ⟨· K†, K†⟩ which preserves order. let v : (m × m) → ℂ := fun x => Kᴴ x.1 x.2 @@ -221,8 +222,8 @@ private lemma lieb_concavity_effros {m : Type*} [Fintype m] [DecidableEq m] -- Use that (RHS - LHS) is PSD => ⟨v, (RHS - LHS) v⟩ ≥ 0 have h_vec_nonneg := h_jconv_le.dotProduct_mulVec_nonneg v -- Expand LHS linearity - simp only [Matrix.sub_mulVec, Matrix.add_mulVec, Matrix.smul_mulVec] at h_vec_nonneg - simp only [dotProduct_sub, dotProduct_add, dotProduct_smul] at h_vec_nonneg + simp only [Matrix.sub_mulVec, Matrix.add_mulVec] at h_vec_nonneg + simp only [dotProduct_sub, dotProduct_add] at h_vec_nonneg -- Connect to Lieb function -- Use the spectral identity: ⟨v, matrixPerspective(f, L_A, R_B) v⟩ = -liebJointFunction(K, p, A, B) have h_ident1 : (star v ⬝ᵥ (term1 *ᵥ v)).re = -(liebJointFunction K p A₁ hA₁.posSemidef B₁ hB₁.posSemidef).re := by @@ -237,8 +238,9 @@ private lemma lieb_concavity_effros {m : Type*} [Fintype m] [DecidableEq m] -- applied to the convex combinations, after identifying L = leftMulMatrix(w₁A₁+w₂A₂) -- and R = rightMulMatrix(w₁B₁+w₂B₂) via linearity of leftMulMatrix/rightMulMatrix. have h_ident_comb : (star v ⬝ᵥ (term_comb *ᵥ v)).re = -(liebJointFunction K p - (w₁ • A₁ + w₂ • A₂) ((hA₁.posSemidef.smul hw₁).add (hA₂.posSemidef.smul hw₂)) - (w₁ • B₁ + w₂ • B₂) ((hB₁.posSemidef.smul hw₁).add (hB₂.posSemidef.smul hw₂))).re := by + (w₁ • A₁ + w₂ • A₂) ((hA₁.posSemidef.real_smul hw₁).add (hA₂.posSemidef.real_smul hw₂)) + (w₁ • B₁ + w₂ • B₂) + ((hB₁.posSemidef.real_smul hw₁).add (hB₂.posSemidef.real_smul hw₂))).re := by have hLlin : L = 𝐋 (w₁ • A₁ + w₂ • A₂) := by ext ij kl rcases ij with ⟨i, j⟩ @@ -257,7 +259,7 @@ private lemma lieb_concavity_effros {m : Type*} [Fintype m] [DecidableEq m] · simp [R, R₁, R₂, rightMulMatrix_apply, h] have hR_pd' : (𝐑 (w₁ • B₁ + w₂ • B₂)).PosDef := by rw [← hRlin]; exact hR_pd have hL_psd' : (𝐋 (w₁ • A₁ + w₂ • A₂)).PosSemidef := by - rw [← hLlin]; exact (hL₁_psd.smul hw₁).add (hL₂_psd.smul hw₂) + rw [← hLlin]; exact (hL₁_psd.real_smul hw₁).add (hL₂_psd.real_smul hw₂) -- Apply matrixPerspective_inner_eq_neg_liebJointFunction to the convex combination -- The key identity relates the HS inner product to the Lieb function. -- After establishing that term_comb = matrixPerspective f (leftMulMatrix (w₁•A₁+w₂•A₂)) @@ -289,17 +291,28 @@ private lemma lieb_concavity_effros {m : Type*} [Fintype m] [DecidableEq m] (by rw [rightMulMatrix_add, ← rightMulMatrix_smul_real, ← rightMulMatrix_smul_real]) rw [hpersp_eq] exact h_apply - -- Substitute identities into the nonnegativity inequality - have h_vec_re : - 0 ≤ - (w₁ • (star v ⬝ᵥ (term1 *ᵥ v)) + w₂ • (star v ⬝ᵥ (term2 *ᵥ v)) - - (star v ⬝ᵥ (term_comb *ᵥ v))).re := by - exact (Complex.nonneg_iff.mp h_vec_nonneg).1 + -- Substitute identities into the nonnegativity inequality. + -- After the simp rewrites, `h_vec_nonneg` is + -- 0 ≤ (star v ⬝ᵥ (w₁ • term1) *ᵥ v + star v ⬝ᵥ (w₂ • term2) *ᵥ v + -- - star v ⬝ᵥ term_comb *ᵥ v).re + -- Push the real scalars out of `mulVec` and `dotProduct` via the ℂ-coercion + -- (since `PosSMulMono ℝ ℂ` is unavailable, we route through `Complex.real_smul`). + have hsmul₁ : star v ⬝ᵥ (w₁ • term1) *ᵥ v = (w₁ : ℂ) * (star v ⬝ᵥ term1 *ᵥ v) := by + rw [show (w₁ • term1 : Matrix (m × m) (m × m) ℂ) = (w₁ : ℂ) • term1 from by + ext i j; simp [Complex.real_smul]] + rw [Matrix.smul_mulVec, dotProduct_smul]; rfl + have hsmul₂ : star v ⬝ᵥ (w₂ • term2) *ᵥ v = (w₂ : ℂ) * (star v ⬝ᵥ term2 *ᵥ v) := by + rw [show (w₂ • term2 : Matrix (m × m) (m × m) ℂ) = (w₂ : ℂ) • term2 from by + ext i j; simp [Complex.real_smul]] + rw [Matrix.smul_mulVec, dotProduct_smul]; rfl + rw [hsmul₁, hsmul₂] at h_vec_nonneg have h_vec_re' : 0 ≤ (w₁ * (star v ⬝ᵥ (term1 *ᵥ v)).re + w₂ * (star v ⬝ᵥ (term2 *ᵥ v)).re - (star v ⬝ᵥ (term_comb *ᵥ v)).re) := by - simpa [Complex.add_re, Complex.sub_re, Complex.real_smul] using h_vec_re + have := (Complex.nonneg_iff.mp h_vec_nonneg).1 + simpa [Complex.add_re, Complex.sub_re, Complex.mul_re, + Complex.ofReal_re, Complex.ofReal_im] using this rw [h_ident1, h_ident2, h_ident_comb] at h_vec_re' linarith @@ -313,18 +326,20 @@ private lemma lieb_joint_concavity {m : Type*} [Fintype m] [DecidableEq m] w₁ * (liebJointFunction K p A₁ hA₁.posSemidef B₁ hB₁.posSemidef).re + w₂ * (liebJointFunction K p A₂ hA₂.posSemidef B₂ hB₂.posSemidef).re ≤ (liebJointFunction K p - (w₁ • A₁ + w₂ • A₂) ((hA₁.posSemidef.smul hw₁).add (hA₂.posSemidef.smul hw₂)) - (w₁ • B₁ + w₂ • B₂) ((hB₁.posSemidef.smul hw₁).add (hB₂.posSemidef.smul hw₂))).re := by + (w₁ • A₁ + w₂ • A₂) ((hA₁.posSemidef.real_smul hw₁).add (hA₂.posSemidef.real_smul hw₂)) + (w₁ • B₁ + w₂ • B₂) ((hB₁.posSemidef.real_smul hw₁).add (hB₂.posSemidef.real_smul hw₂))).re := by -- Handle boundary cases p = 0 and p = 1 separately rcases eq_or_lt_of_le hp0 with rfl | hp0' · -- p = 0: Tr(K†BK) is linear in B, so equality holds rw [liebJointFunction_zero_eq, liebJointFunction_zero_eq, liebJointFunction_zero_eq] + have hcast : ∀ (w : ℝ) (M : Matrix m m ℂ), (w • M : Matrix m m ℂ) = (w : ℂ) • M := by + intro w M; ext i j; simp [Complex.real_smul] have h_linear : (Kᴴ * (w₁ • B₁ + w₂ • B₂) * K).trace = (w₁ : ℂ) * (Kᴴ * B₁ * K).trace + (w₂ : ℂ) * (Kᴴ * B₂ * K).trace := by - rw [Matrix.mul_add, Matrix.add_mul] + rw [Matrix.mul_add, Matrix.add_mul, hcast w₁ B₁, hcast w₂ B₂] rw [Matrix.mul_smul, Matrix.smul_mul, Matrix.mul_smul, Matrix.smul_mul] rw [trace_add, trace_smul, trace_smul] - simp only [Complex.real_smul] + simp [smul_eq_mul] rw [h_linear] simp only [Complex.add_re, Complex.mul_re, Complex.ofReal_re, Complex.ofReal_im, zero_mul, sub_zero] @@ -332,12 +347,14 @@ private lemma lieb_joint_concavity {m : Type*} [Fintype m] [DecidableEq m] rcases eq_or_lt_of_le hp1 with rfl | hp1' · -- p = 1: Tr(AK†K) is linear in A, so equality holds rw [liebJointFunction_one_eq, liebJointFunction_one_eq, liebJointFunction_one_eq] + have hcast : ∀ (w : ℝ) (M : Matrix m m ℂ), (w • M : Matrix m m ℂ) = (w : ℂ) • M := by + intro w M; ext i j; simp [Complex.real_smul] have h_linear : ((w₁ • A₁ + w₂ • A₂) * Kᴴ * K).trace = (w₁ : ℂ) * (A₁ * Kᴴ * K).trace + (w₂ : ℂ) * (A₂ * Kᴴ * K).trace := by - rw [Matrix.add_mul, Matrix.add_mul] + rw [Matrix.add_mul, Matrix.add_mul, hcast w₁ A₁, hcast w₂ A₂] rw [Matrix.smul_mul, Matrix.smul_mul, Matrix.smul_mul, Matrix.smul_mul] rw [trace_add, trace_smul, trace_smul] - simp only [Complex.real_smul] + simp [smul_eq_mul] rw [h_linear] simp only [Complex.add_re, Complex.mul_re, Complex.ofReal_re, Complex.ofReal_im, zero_mul, sub_zero] @@ -432,8 +449,8 @@ theorem lieb_joint_concavity_semidef {m : Type*} [Fintype m] [DecidableEq m] w₁ * (liebJointFunction K p A₁ hA₁ B₁ hB₁).re + w₂ * (liebJointFunction K p A₂ hA₂ B₂ hB₂).re ≤ (liebJointFunction K p - (w₁ • A₁ + w₂ • A₂) ((hA₁.smul hw₁).add (hA₂.smul hw₂)) - (w₁ • B₁ + w₂ • B₂) ((hB₁.smul hw₁).add (hB₂.smul hw₂))).re := by + (w₁ • A₁ + w₂ • A₂) ((hA₁.real_smul hw₁).add (hA₂.real_smul hw₂)) + (w₁ • B₁ + w₂ • B₂) ((hB₁.real_smul hw₁).add (hB₂.real_smul hw₂))).re := by -- For each ε > 0, Aᵢ + ε•1 is PosDef; the inequality holds by lieb_joint_concavity -- Use unfolded form to avoid PosSemidef proof dependencies in the type have hε_ineq : ∀ ε : ℝ, 0 < ε → @@ -443,20 +460,31 @@ theorem lieb_joint_concavity_semidef {m : Type*} [Fintype m] [DecidableEq m] (w₁ • B₁ + w₂ • B₂ + (ε:ℂ) • 1) ^ (1 - p) * K).trace.re := by intro ε hε -- Key: w₁•(Aᵢ + ε•1) + w₂•(Aᵢ + ε•1) = w₁•Aᵢ + w₂•Aᵢ + ε•1 (using w₁ + w₂ = 1) - have hcomb_A : w₁ • (A₁ + (ε:ℂ) • 1) + w₂ • (A₂ + (ε:ℂ) • 1) = w₁ • A₁ + w₂ • A₂ + (ε:ℂ) • 1 := - calc w₁ • (A₁ + (ε:ℂ) • 1) + w₂ • (A₂ + (ε:ℂ) • 1) - = w₁ • A₁ + w₁ • ((ε:ℂ) • 1) + (w₂ • A₂ + w₂ • ((ε:ℂ) • 1)) := by - simp [smul_add] - _ = w₁ • A₁ + w₂ • A₂ + (w₁ • ((ε:ℂ) • 1) + w₂ • ((ε:ℂ) • 1)) := by abel - _ = w₁ • A₁ + w₂ • A₂ + (w₁ + w₂) • ((ε:ℂ) • 1) := by rw [← add_smul] - _ = w₁ • A₁ + w₂ • A₂ + (ε:ℂ) • 1 := by rw [hw, one_smul] - have hcomb_B : w₁ • (B₁ + (ε:ℂ) • 1) + w₂ • (B₂ + (ε:ℂ) • 1) = w₁ • B₁ + w₂ • B₂ + (ε:ℂ) • 1 := - calc w₁ • (B₁ + (ε:ℂ) • 1) + w₂ • (B₂ + (ε:ℂ) • 1) - = w₁ • B₁ + w₁ • ((ε:ℂ) • 1) + (w₂ • B₂ + w₂ • ((ε:ℂ) • 1)) := by - simp [smul_add] - _ = w₁ • B₁ + w₂ • B₂ + (w₁ • ((ε:ℂ) • 1) + w₂ • ((ε:ℂ) • 1)) := by abel - _ = w₁ • B₁ + w₂ • B₂ + (w₁ + w₂) • ((ε:ℂ) • 1) := by rw [← add_smul] - _ = w₁ • B₁ + w₂ • B₂ + (ε:ℂ) • 1 := by rw [hw, one_smul] + -- Convert real smul to complex smul to enable distributivity rewrites + have hcast : ∀ (w : ℝ) (M : Matrix m m ℂ), (w • M : Matrix m m ℂ) = (w : ℂ) • M := by + intro w M; ext i j; simp [Complex.real_smul] + have hsum_smul_one : (w₁ : ℂ) • ((ε:ℂ) • (1 : Matrix m m ℂ)) + + (w₂ : ℂ) • ((ε:ℂ) • 1) = (ε:ℂ) • 1 := by + have heqcast : (w₁ : ℂ) + (w₂ : ℂ) = ((w₁ + w₂ : ℝ) : ℂ) := by push_cast; ring + rw [← add_smul, heqcast, hw, Complex.ofReal_one, one_smul] + have hcomb_A : w₁ • (A₁ + (ε:ℂ) • 1) + w₂ • (A₂ + (ε:ℂ) • 1) = + w₁ • A₁ + w₂ • A₂ + (ε:ℂ) • 1 := by + rw [hcast w₁ (A₁ + _), hcast w₂ (A₂ + _), hcast w₁ A₁, hcast w₂ A₂, + smul_add, smul_add] + have heq : (w₁ : ℂ) • A₁ + (w₁ : ℂ) • ((ε:ℂ) • (1 : Matrix m m ℂ)) + + ((w₂ : ℂ) • A₂ + (w₂ : ℂ) • ((ε:ℂ) • 1)) = + (w₁ : ℂ) • A₁ + (w₂ : ℂ) • A₂ + + ((w₁ : ℂ) • ((ε:ℂ) • (1 : Matrix m m ℂ)) + (w₂ : ℂ) • ((ε:ℂ) • 1)) := by abel + rw [heq, hsum_smul_one] + have hcomb_B : w₁ • (B₁ + (ε:ℂ) • 1) + w₂ • (B₂ + (ε:ℂ) • 1) = + w₁ • B₁ + w₂ • B₂ + (ε:ℂ) • 1 := by + rw [hcast w₁ (B₁ + _), hcast w₂ (B₂ + _), hcast w₁ B₁, hcast w₂ B₂, + smul_add, smul_add] + have heq : (w₁ : ℂ) • B₁ + (w₁ : ℂ) • ((ε:ℂ) • (1 : Matrix m m ℂ)) + + ((w₂ : ℂ) • B₂ + (w₂ : ℂ) • ((ε:ℂ) • 1)) = + (w₁ : ℂ) • B₁ + (w₂ : ℂ) • B₂ + + ((w₁ : ℂ) • ((ε:ℂ) • (1 : Matrix m m ℂ)) + (w₂ : ℂ) • ((ε:ℂ) • 1)) := by abel + rw [heq, hsum_smul_one] have h := lieb_joint_concavity (A₁ + (ε:ℂ) • 1) (A₂ + (ε:ℂ) • 1) (B₁ + (ε:ℂ) • 1) (B₂ + (ε:ℂ) • 1) (hA₁.add_smul_one_posDef hε) (hA₂.add_smul_one_posDef hε) @@ -487,21 +515,27 @@ theorem lieb_joint_concavity_semidef {m : Type*} [Fintype m] [DecidableEq m] ((w₁ • A₁ + w₂ • A₂ + (ε:ℂ) • 1) ^ p * Kᴴ * (w₁ • B₁ + w₂ • B₂ + (ε:ℂ) • 1) ^ (1 - p) * K).trace.re) (nhdsWithin 0 (Set.Ioi 0)) - (nhds (liebJointFunction K p (w₁ • A₁ + w₂ • A₂) ((hA₁.smul hw₁).add (hA₂.smul hw₂)) - (w₁ • B₁ + w₂ • B₂) ((hB₁.smul hw₁).add (hB₂.smul hw₂))).re) := by + (nhds (liebJointFunction K p (w₁ • A₁ + w₂ • A₂) + ((hA₁.real_smul hw₁).add (hA₂.real_smul hw₂)) + (w₁ • B₁ + w₂ • B₂) + ((hB₁.real_smul hw₁).add (hB₂.real_smul hw₂))).re) := by simp only [liebJointFunction] apply (Complex.continuous_re.comp continuous_id.matrix_trace).continuousAt.tendsto.comp - exact ((rpow_tendsto_smul_one ((hA₁.smul hw₁).add (hA₂.smul hw₂)) p hp0).mul_const Kᴴ).mul - (rpow_tendsto_smul_one ((hB₁.smul hw₁).add (hB₂.smul hw₂)) (1 - p) (by linarith)) |>.mul_const K + exact ((rpow_tendsto_smul_one ((hA₁.real_smul hw₁).add (hA₂.real_smul hw₂)) + p hp0).mul_const Kᴴ).mul + (rpow_tendsto_smul_one ((hB₁.real_smul hw₁).add (hB₂.real_smul hw₂)) + (1 - p) (by linarith)) |>.mul_const K -- Combine: lhs_limit ≤ rhs_limit via the ε-pointwise inequality apply le_of_tendsto_of_tendsto hconv_lhs hconv_rhs filter_upwards [self_mem_nhdsWithin (s := Set.Ioi (0:ℝ))] with ε (hε : ε ∈ Set.Ioi 0) exact hε_ineq ε (Set.mem_Ioi.mp hε) /-- Block diagonal matrix `fromBlocks A 0 0 0` is positive semidefinite when `A` is. -/ -private lemma fromBlocks_top_posSemidef {n m : Type*} [Fintype n] [Fintype m] +private lemma fromBlocks_top_posSemidef {n m : Type*} [Finite n] [Finite m] {A : Matrix n n ℂ} (hA : A.PosSemidef) : (Matrix.fromBlocks A 0 0 (0 : Matrix m m ℂ)).PosSemidef := by + letI := Fintype.ofFinite n + letI := Fintype.ofFinite m refine PosSemidef.of_dotProduct_mulVec_nonneg (by simpa using Matrix.IsHermitian.fromBlocks hA.1 (by simp) Matrix.isHermitian_zero) ?_ intro v @@ -513,9 +547,11 @@ private lemma fromBlocks_top_posSemidef {n m : Type*} [Fintype n] [Fintype m] exact hA.dotProduct_mulVec_nonneg _ /-- Block diagonal matrix `fromBlocks 0 0 0 B` is positive semidefinite when `B` is. -/ -private lemma fromBlocks_bot_posSemidef {n m : Type*} [Fintype n] [Fintype m] +private lemma fromBlocks_bot_posSemidef {n m : Type*} [Finite n] [Finite m] {B : Matrix m m ℂ} (hB : B.PosSemidef) : (Matrix.fromBlocks (0 : Matrix n n ℂ) 0 0 B).PosSemidef := by + letI := Fintype.ofFinite n + letI := Fintype.ofFinite m refine PosSemidef.of_dotProduct_mulVec_nonneg (by simpa using Matrix.IsHermitian.fromBlocks Matrix.isHermitian_zero (by simp) hB.1) ?_ intro v @@ -598,17 +634,17 @@ private lemma liebJointFunction_eq_block {n m : Type*} [Fintype n] [DecidableEq simp only [fromBlocks_multiply] simp [Matrix.trace, Fintype.sum_sum_type] -private lemma fromBlocks_smul_top {n m : Type*} [Fintype n] [Fintype m] +private lemma fromBlocks_smul_top {n m : Type*} (A : Matrix n n ℂ) (w : ℝ) : w • (fromBlocks A 0 0 (0 : Matrix m m ℂ)) = fromBlocks (w • A) 0 0 0 := by ext i j - rcases i with i | i <;> rcases j with j | j <;> simp [fromBlocks, smul_zero] + rcases i with i | i <;> rcases j with j | j <;> simp [fromBlocks] -private lemma fromBlocks_smul_bot {n m : Type*} [Fintype n] [Fintype m] +private lemma fromBlocks_smul_bot {n m : Type*} (B : Matrix m m ℂ) (w : ℝ) : w • (fromBlocks (0 : Matrix n n ℂ) 0 0 B) = fromBlocks 0 0 0 (w • B) := by ext i j - rcases i with i | i <;> rcases j with j | j <;> simp [fromBlocks, smul_zero] + rcases i with i | i <;> rcases j with j | j <;> simp [fromBlocks] /-- **Lieb's Joint Concavity Theorem for Rectangular Matrices (PosSemidef extension)** @@ -632,17 +668,20 @@ theorem lieb_joint_concavity_rect_semidef {n m : Type*} [Fintype n] [DecidableEq w₁ * (liebJointFunction K p A₁ hA₁ B₁ hB₁).re + w₂ * (liebJointFunction K p A₂ hA₂ B₂ hB₂).re ≤ (liebJointFunction K p - (w₁ • A₁ + w₂ • A₂) ((hA₁.smul hw₁).add (hA₂.smul hw₂)) - (w₁ • B₁ + w₂ • B₂) ((hB₁.smul hw₁).add (hB₂.smul hw₂))).re := by + (w₁ • A₁ + w₂ • A₂) ((hA₁.real_smul hw₁).add (hA₂.real_smul hw₂)) + (w₁ • B₁ + w₂ • B₂) ((hB₁.real_smul hw₁).add (hB₂.real_smul hw₂))).re := by -- Boundary cases p = 0 and p = 1: both sides are linear, giving equality rcases eq_or_lt_of_le hp0 with rfl | hp0' · -- p = 0: Tr(K†BK) is linear in B simp only [liebJointFunction_zero_eq] + have hcastB : ∀ (w : ℝ) (M : Matrix m m ℂ), (w • M : Matrix m m ℂ) = (w : ℂ) • M := by + intro w M; ext i j; simp [Complex.real_smul] have h_linear : (Kᴴ * (w₁ • B₁ + w₂ • B₂) * K).trace = (w₁ : ℂ) * (Kᴴ * B₁ * K).trace + (w₂ : ℂ) * (Kᴴ * B₂ * K).trace := by - rw [Matrix.mul_add, Matrix.add_mul, Matrix.mul_smul, Matrix.smul_mul, + rw [Matrix.mul_add, Matrix.add_mul, hcastB w₁ B₁, hcastB w₂ B₂, + Matrix.mul_smul, Matrix.smul_mul, Matrix.mul_smul, Matrix.smul_mul, trace_add, trace_smul, trace_smul] - simp [Complex.real_smul] + simp [smul_eq_mul] rw [h_linear] simp only [Complex.add_re, Complex.mul_re, Complex.ofReal_re, Complex.ofReal_im, zero_mul, sub_zero] @@ -650,11 +689,14 @@ theorem lieb_joint_concavity_rect_semidef {n m : Type*} [Fintype n] [DecidableEq rcases eq_or_lt_of_le hp1 with rfl | hp1' · -- p = 1: Tr(AK†K) is linear in A simp only [liebJointFunction_one_eq] + have hcastA : ∀ (w : ℝ) (M : Matrix n n ℂ), (w • M : Matrix n n ℂ) = (w : ℂ) • M := by + intro w M; ext i j; simp [Complex.real_smul] have h_linear : ((w₁ • A₁ + w₂ • A₂) * Kᴴ * K).trace = (w₁ : ℂ) * (A₁ * Kᴴ * K).trace + (w₂ : ℂ) * (A₂ * Kᴴ * K).trace := by - rw [Matrix.add_mul, Matrix.add_mul, Matrix.smul_mul, Matrix.smul_mul, + rw [Matrix.add_mul, Matrix.add_mul, hcastA w₁ A₁, hcastA w₂ A₂, + Matrix.smul_mul, Matrix.smul_mul, Matrix.smul_mul, Matrix.smul_mul, trace_add, trace_smul, trace_smul] - simp [Complex.real_smul] + simp [smul_eq_mul] rw [h_linear] simp only [Complex.add_re, Complex.mul_re, Complex.ofReal_re, Complex.ofReal_im, zero_mul, sub_zero] @@ -682,17 +724,19 @@ theorem lieb_joint_concavity_rect_semidef {n m : Type*} [Fintype n] [DecidableEq simp only [Ablock1, Ablock2, fromBlocks_smul_top, fromBlocks_add, add_zero] have hBcomb : w₁ • Bblock1 + w₂ • Bblock2 = fromBlocks 0 0 0 (w₁ • B₁ + w₂ • B₂) := by simp only [Bblock1, Bblock2, fromBlocks_smul_bot, fromBlocks_add, zero_add] - have hAcomb_psd : (w₁ • Ablock1 + w₂ • Ablock2).PosSemidef := (hAb1.smul hw₁).add (hAb2.smul hw₂) - have hBcomb_psd : (w₁ • Bblock1 + w₂ • Bblock2).PosSemidef := (hBb1.smul hw₁).add (hBb2.smul hw₂) + have hAcomb_psd : (w₁ • Ablock1 + w₂ • Ablock2).PosSemidef := + (hAb1.real_smul hw₁).add (hAb2.real_smul hw₂) + have hBcomb_psd : (w₁ • Bblock1 + w₂ • Bblock2).PosSemidef := + (hBb1.real_smul hw₁).add (hBb2.real_smul hw₂) have hidcomb : liebJointFunction Kblock p (w₁ • Ablock1 + w₂ • Ablock2) hAcomb_psd (w₁ • Bblock1 + w₂ • Bblock2) hBcomb_psd = - liebJointFunction K p (w₁ • A₁ + w₂ • A₂) ((hA₁.smul hw₁).add (hA₂.smul hw₂)) - (w₁ • B₁ + w₂ • B₂) ((hB₁.smul hw₁).add (hB₂.smul hw₂)) := by + liebJointFunction K p (w₁ • A₁ + w₂ • A₂) ((hA₁.real_smul hw₁).add (hA₂.real_smul hw₂)) + (w₁ • B₁ + w₂ • B₂) ((hB₁.real_smul hw₁).add (hB₂.real_smul hw₂)) := by simp only [liebJointFunction] conv_lhs => rw [hAcomb, hBcomb] have key2 := liebJointFunction_eq_block K p hp0' hp1' - (w₁ • A₁ + w₂ • A₂) ((hA₁.smul hw₁).add (hA₂.smul hw₂)) - (w₁ • B₁ + w₂ • B₂) ((hB₁.smul hw₁).add (hB₂.smul hw₂)) + (w₁ • A₁ + w₂ • A₂) ((hA₁.real_smul hw₁).add (hA₂.real_smul hw₂)) + (w₁ • B₁ + w₂ • B₂) ((hB₁.real_smul hw₁).add (hB₂.real_smul hw₂)) simp only [liebJointFunction] at key2 exact key2 -- Rewrite key inequality using the block identities @@ -727,15 +771,18 @@ lemma rpow_nonneg_smul {α : Type*} [Fintype α] [DecidableEq α] -- c • diag(ev) = diag(c * ev) have hsmul_diag : c • diagonal (fun i => (ev i : ℂ)) = diagonal (fun i => ((c * ev i : ℝ) : ℂ)) := by - ext i j; simp only [Matrix.smul_apply, diagonal_apply, smul_ite, smul_zero] - split_ifs <;> [simp [Complex.ofReal_mul]; rfl] + ext i j + simp only [Matrix.smul_apply, diagonal_apply] + split_ifs with h + · simp [Complex.ofReal_mul, Complex.real_smul] + · simp -- c • A = U * diag(c * ev) * U† have hcA_spec : c • A = U * diagonal (fun i => ((c * ev i : ℝ) : ℂ)) * Uᴴ := by conv_lhs => rw [hspec] -- c • ((U * D) * Uᴴ) = (c • (U * D)) * Uᴴ = (U * (c • D)) * Uᴴ = (U * D') * Uᴴ rw [← smul_mul_assoc, ← mul_smul_comm, hsmul_diag] -- (c • A)^s = U * diag((c*ev)^s) * U† - have hcA_nonneg : 0 ≤ c • A := by rw [Matrix.le_iff, sub_zero]; exact hA.smul hc + have hcA_nonneg : 0 ≤ c • A := by rw [Matrix.le_iff, sub_zero]; exact hA.real_smul hc have h_lhs : (c • A) ^ s = U * diagonal (fun i => (((c * ev i) ^ s : ℝ) : ℂ)) * Uᴴ := by conv_lhs => rw [hcA_spec] @@ -764,7 +811,7 @@ lemma rpow_nonneg_smul {α : Type*} [Fintype α] [DecidableEq α] simp only [if_true, Complex.real_smul] rw [Real.mul_rpow hc (hev_nn i)] simp only [Complex.ofReal_mul] - · simp only [hij, if_false, smul_zero] + · simp [hij] /-- Degree-1 homogeneity of F_s: F_s(cA, cB) = c ⋅ F_s(A, B). -/ lemma Fs_homogeneous {α : Type*} [Fintype α] [DecidableEq α] @@ -790,8 +837,10 @@ lemma Fs_homogeneous {α : Type*} [Fintype α] [DecidableEq α] rw [← Real.rpow_add hc_pos, show s + (1 - s) = 1 by ring, Real.rpow_one] rw [this] -- Goal: (c • (A^s * B^{1-s})).trace.re = c * (A^s * B^{1-s}).trace.re - simp only [Matrix.trace_smul, Complex.real_smul, Complex.mul_re, - Complex.ofReal_re, Complex.ofReal_im, zero_mul, sub_zero] + -- Route through `(c : ℂ) • _` since `PosSMulMono ℝ ℂ` is unavailable. + rw [show (c • (A ^ s * B ^ (1 - s)) : Matrix α α ℂ) = + (c : ℂ) • (A ^ s * B ^ (1 - s)) from by ext i j; simp [Complex.real_smul]] + rw [Matrix.trace_smul]; simp /-- Weighted multi-term Lieb concavity (K = I, square matrices): ∑ᵢ wᵢ Tr (Aᵢˢ Bᵢ¹⁻ˢ) ≤ Tr ((∑ᵢ wᵢ Aᵢ)ˢ (∑ᵢ wᵢ Bᵢ)¹⁻ˢ) @@ -822,17 +871,19 @@ lemma lieb_concavity_weighted {r : ℕ} {α : Type*} [Fintype α] [DecidableEq have hwr_le : wr ≤ 1 := by linarith -- PSD of weighted sums have hSA_psd : (∑ i : Fin r, w' i • A' i).PosSemidef := - posSemidef_sum Finset.univ fun i _ => (hA (Fin.castSucc i)).smul (hw_nn (Fin.castSucc i)) + posSemidef_sum Finset.univ fun i _ => + (hA (Fin.castSucc i)).real_smul (hw_nn (Fin.castSucc i)) have hSB_psd : (∑ i : Fin r, w' i • B' i).PosSemidef := - posSemidef_sum Finset.univ fun i _ => (hB (Fin.castSucc i)).smul (hw_nn (Fin.castSucc i)) + posSemidef_sum Finset.univ fun i _ => + (hB (Fin.castSucc i)).real_smul (hw_nn (Fin.castSucc i)) have hAr_psd : Ar.PosSemidef := hA (Fin.last r) have hBr_psd : Br.PosSemidef := hB (Fin.last r) -- Use the 2-term Lieb concavity (K = 1) with weights W and wr have h2term := lieb_joint_concavity_semidef (∑ i : Fin r, w' i • A' i) (wr • Ar) (∑ i : Fin r, w' i • B' i) (wr • Br) - hSA_psd ((hA (Fin.last r)).smul hwr_nn) - hSB_psd ((hB (Fin.last r)).smul hwr_nn) + hSA_psd ((hA (Fin.last r)).real_smul hwr_nn) + hSB_psd ((hB (Fin.last r)).real_smul hwr_nn) 1 s hs0 hs1 W wr hW_nn hwr_nn hW_eq simp only [liebJointFunction, conjTranspose_one, Matrix.mul_one] at h2term -- Case split: W = 0 → trivial; W > 0 → IH with wᵢ/W then 2-term concavity @@ -845,14 +896,21 @@ lemma lieb_concavity_weighted {r : ℕ} {α : Type*} [Fintype α] [DecidableEq exact this i (Finset.mem_univ _) have hwr_one : wr = 1 := by linarith have hA_zero : ∑ i : Fin r, w' i • A' i = 0 := by - apply Finset.sum_eq_zero; intro i _; simp [hw'_zero i] + apply Finset.sum_eq_zero; intro i _ + rw [hw'_zero i]; ext; simp [Complex.real_smul] have hB_zero : ∑ i : Fin r, w' i • B' i = 0 := by - apply Finset.sum_eq_zero; intro i _; simp [hw'_zero i] + apply Finset.sum_eq_zero; intro i _ + rw [hw'_zero i]; ext; simp [Complex.real_smul] have hF_zero : ∑ i : Fin r, w' i * ((A' i) ^ s * (B' i) ^ (1 - s)).trace.re = 0 := by apply Finset.sum_eq_zero; intro i _; simp [hw'_zero i] -- Unfold the set definitions so simp can match simp only [w', A', B', Ar, Br, wr] at hwr_one hA_zero hB_zero hF_zero ⊢ - simp only [hwr_one, one_mul, one_smul, hA_zero, hB_zero, hF_zero, zero_add, le_refl] + rw [hwr_one, hF_zero, hA_zero, hB_zero] + rw [show (1 : ℝ) • A (Fin.last r) = A (Fin.last r) from by + ext; simp [Complex.real_smul]] + rw [show (1 : ℝ) • B (Fin.last r) = B (Fin.last r) from by + ext; simp [Complex.real_smul]] + simp · -- W > 0 have hW_pos : 0 < W := lt_of_le_of_ne hW_nn (Ne.symm hW) -- Divide weights by W for IH @@ -863,34 +921,46 @@ lemma lieb_concavity_weighted {r : ℕ} {α : Type*} [Fintype α] [DecidableEq have ih' := ih A' B' (fun i => hA (Fin.castSucc i)) (fun i => hB (Fin.castSucc i)) (fun i => w' i / W) hw'_nn hw'_sum -- Factor out 1/W from weighted sums - have hSA_div : ∑ i : Fin r, (w' i / W) • A' i = (1 / W) • ∑ i : Fin r, w' i • A' i := by - rw [Finset.smul_sum] - congr 1 - funext i - rw [show (w' i / W) = (1 / W) * w' i from by ring] - rw [smul_smul] - have hSB_div : ∑ i : Fin r, (w' i / W) • B' i = (1 / W) • ∑ i : Fin r, w' i • B' i := by - rw [Finset.smul_sum] - congr 1 - funext i - rw [show (w' i / W) = (1 / W) * w' i from by ring] - rw [smul_smul] + -- `Finset.smul_sum`/`smul_smul` over `ℝ • Matrix _ _ ℂ` are unavailable + -- (no `PosSMulMono ℝ ℂ`); decompose via `ext` and reduce to `ℝ`-arithmetic. + have hSA_div : ∑ i : Fin r, (w' i / W) • A' i = + (1 / W) • ∑ i : Fin r, w' i • A' i := by + ext j k + simp only [Matrix.sum_apply, Matrix.smul_apply, Complex.real_smul] + rw [Finset.mul_sum] + refine Finset.sum_congr rfl ?_ + intro i _ + push_cast; ring + have hSB_div : ∑ i : Fin r, (w' i / W) • B' i = + (1 / W) • ∑ i : Fin r, w' i • B' i := by + ext j k + simp only [Matrix.sum_apply, Matrix.smul_apply, Complex.real_smul] + rw [Finset.mul_sum] + refine Finset.sum_congr rfl ?_ + intro i _ + push_cast; ring -- 2-term Lieb concavity with X = (1/W)•Σw'A, Y = (1/W)•Σw'B have hX_psd : ((1 / W) • ∑ i : Fin r, w' i • A' i).PosSemidef := - hSA_psd.smul (div_nonneg zero_le_one hW_nn) + hSA_psd.real_smul (div_nonneg zero_le_one hW_nn) have hY_psd : ((1 / W) • ∑ i : Fin r, w' i • B' i).PosSemidef := - hSB_psd.smul (div_nonneg zero_le_one hW_nn) + hSB_psd.real_smul (div_nonneg zero_le_one hW_nn) have h2 := lieb_joint_concavity_semidef ((1 / W) • ∑ i : Fin r, w' i • A' i) Ar ((1 / W) • ∑ i : Fin r, w' i • B' i) Br hX_psd hAr_psd hY_psd hBr_psd 1 s hs0 hs1 W wr hW_nn hwr_nn hW_eq simp only [liebJointFunction, conjTranspose_one, Matrix.mul_one] at h2 - -- Simplify W • (1/W • X) = X + -- Simplify W • (1/W • X) = X via the ℂ-coercion (no `PosSMulMono ℝ ℂ`). have hWX_A : W • ((1 / W) • ∑ i : Fin r, w' i • A' i) = ∑ i : Fin r, w' i • A' i := by - rw [smul_smul, mul_one_div_cancel (ne_of_gt hW_pos), one_smul] + ext j k + simp only [Matrix.smul_apply, Complex.real_smul] + push_cast + field_simp have hWX_B : W • ((1 / W) • ∑ i : Fin r, w' i • B' i) = ∑ i : Fin r, w' i • B' i := by - rw [smul_smul, mul_one_div_cancel (ne_of_gt hW_pos), one_smul] + ext j k + simp only [Matrix.smul_apply, Complex.real_smul] + push_cast + field_simp rw [hWX_A, hWX_B] at h2 -- Combine h2 (2-term concavity) with IH (normalized weights) have ih_simple : ∑ i : Fin r, (w' i / W) * ((A' i) ^ s * (B' i) ^ (1 - s)).trace.re ≤ diff --git a/QuantumSystem/Analysis/Matrix/Order.lean b/QuantumSystem/Analysis/Matrix/Order.lean index a7dd4d5..b9d1502 100644 --- a/QuantumSystem/Analysis/Matrix/Order.lean +++ b/QuantumSystem/Analysis/Matrix/Order.lean @@ -43,7 +43,7 @@ and related operator-convexity results. namespace Matrix open Real NNReal MeasureTheory Set -open scoped MatrixOrder ComplexOrder +open scoped MatrixOrder ComplexOrder NNReal /-- A real function f is Löwner monotone on positive semidefinite matrices if A ≤ B (in the Löwner order) implies f(A) ≤ f(B). -/ @@ -105,10 +105,12 @@ def IsJensenConcave (f : ℝ → ℝ) : Prop := fC ≤ Aᴴ * fT₁ * A + Bᴴ * fT₂ * B /-- Block diagonal matrix is positive semidefinite if blocks are positive semidefinite. -/ -private lemma fromBlocks_posSemidef_diag {m n : Type*} [Fintype m] [Fintype n] +private lemma fromBlocks_posSemidef_diag {m n : Type*} [Finite m] [Finite n] {A : Matrix m m ℂ} {D : Matrix n n ℂ} (hA : A.PosSemidef) (hD : D.PosSemidef) : (Matrix.fromBlocks A 0 0 D).PosSemidef := by + letI := Fintype.ofFinite m + letI := Fintype.ofFinite n classical refine PosSemidef.of_dotProduct_mulVec_nonneg ?_ ?_ · -- Hermitian @@ -305,28 +307,31 @@ lemma lownerConvex_compression_le.{v} {n : Type v} {m : Type v} [Fintype n] [Fin have hM_comm : M * (W * Wᴴ) = (W * Wᴴ) * M := by rw [← hP_def] suffices h : M * P = P * M from h - rw [hM_def] - rw [Matrix.add_mul, Matrix.mul_add, Matrix.smul_mul, Matrix.smul_mul, - Matrix.mul_smul, Matrix.mul_smul, + rw [hM_def, Matrix.add_mul, Matrix.mul_add, smul_mul_assoc, smul_mul_assoc, + mul_smul_comm, mul_smul_comm, show S * T' * S * P = S * T' * (S * P) from by simp only [Matrix.mul_assoc], hSP, show P * (S * T' * S) = (P * S) * T' * S from by - simp only [Matrix.mul_assoc], hPS, - ← smul_add, ← smul_add] - congr 1 + simp only [Matrix.mul_assoc], hPS] have hST'P : S * T' * P = P * T' * P + P * T' * P - T' * P := by rw [hS_def, h2P, sub_mul, one_mul, add_mul, sub_mul, add_mul] have hPT'S : P * T' * S = P * T' * P + P * T' * P - P * T' := by rw [hS_def, h2P, mul_sub, mul_one, mul_add] - rw [hST'P, hPT'S]; abel + rw [hST'P, hPT'S] + module have hWMW : Wᴴ * M * W = Wᴴ * T' * W := by - rw [hM_def, - Matrix.mul_add, Matrix.add_mul, Matrix.mul_smul, Matrix.smul_mul, - Matrix.mul_smul, Matrix.smul_mul, + rw [hM_def, Matrix.mul_add, Matrix.add_mul, + show Wᴴ * (1/2 : ℝ) • T' = (1/2 : ℝ) • (Wᴴ * T') from Matrix.mul_smul _ _ _, + show Wᴴ * (1/2 : ℝ) • (S * T' * S) = (1/2 : ℝ) • (Wᴴ * (S * T' * S)) + from Matrix.mul_smul _ _ _, + show (1/2 : ℝ) • (Wᴴ * T') * W = (1/2 : ℝ) • (Wᴴ * T' * W) + from Matrix.smul_mul _ _ _, + show (1/2 : ℝ) • (Wᴴ * (S * T' * S)) * W = (1/2 : ℝ) • (Wᴴ * (S * T' * S) * W) + from Matrix.smul_mul _ _ _, show Wᴴ * (S * T' * S) * W = (Wᴴ * S) * T' * (S * W) from by simp only [Matrix.mul_assoc], - hWhS, hSW, ← smul_add, ← two_smul ℝ (Wᴴ * T' * W), smul_smul, - show (1 / 2 : ℝ) * 2 = 1 from by norm_num, one_smul] + hWhS, hSW] + module have hWMW_herm : (Wᴴ * M * W).IsHermitian := isHermitian_conjTranspose_mul_mul (B := W) (A := M) hM_herm' have h_comp := matrixFunction_compression_of_commuting W M hM_herm' hWW hM_comm f hWMW_herm @@ -338,16 +343,21 @@ lemma lownerConvex_compression_le.{v} {n : Type v} {m : Type v} [Fintype n] [Fin ≤ Wᴴ * ((1 / 2 : ℝ) • cfc f T' + (1 - 1 / 2 : ℝ) • cfc f (S * T' * S)) * W := h_compress _ = Wᴴ * cfc f T' * W := by - rw [h_half, ← hcfc_conj, - Matrix.mul_add, Matrix.add_mul, Matrix.mul_smul, Matrix.smul_mul, - Matrix.mul_smul, Matrix.smul_mul, + rw [h_half, ← hcfc_conj, Matrix.mul_add, Matrix.add_mul, + show Wᴴ * (1/2 : ℝ) • cfc f T' = (1/2 : ℝ) • (Wᴴ * cfc f T') + from Matrix.mul_smul _ _ _, + show Wᴴ * (1/2 : ℝ) • (S * cfc f T' * S) = + (1/2 : ℝ) • (Wᴴ * (S * cfc f T' * S)) + from Matrix.mul_smul _ _ _, + show (1/2 : ℝ) • (Wᴴ * cfc f T') * W = (1/2 : ℝ) • (Wᴴ * cfc f T' * W) + from Matrix.smul_mul _ _ _, + show (1/2 : ℝ) • (Wᴴ * (S * cfc f T' * S)) * W = + (1/2 : ℝ) • (Wᴴ * (S * cfc f T' * S) * W) + from Matrix.smul_mul _ _ _, show Wᴴ * (S * cfc f T' * S) * W = (Wᴴ * S) * cfc f T' * (S * W) from by simp only [Matrix.mul_assoc], - hWhS, hSW, ← smul_add, - show Wᴴ * cfc f T' * W + Wᴴ * cfc f T' * W = (2 : ℝ) • (Wᴴ * cfc f T' * W) from - (two_smul ℝ _).symm, - smul_smul, show (1 / 2 : ℝ) * 2 = 1 from by norm_num, - one_smul] + hWhS, hSW] + module rw [hWTW] at h_jensen rw [hWfTW'] at h_jensen calc cfc f (Vᴴ * T * V) @@ -480,10 +490,14 @@ private lemma inv_lowner_convex_le {m : Type*} [Fintype m] [DecidableEq m] classical by_cases ht_zero : t = 0 · subst ht_zero - simp + have h1 : ((0 : ℝ) • A + ((1 : ℝ) - 0) • B : Matrix m m ℂ) = B := by module + have h2 : ((0 : ℝ) • A⁻¹ + ((1 : ℝ) - 0) • B⁻¹ : Matrix m m ℂ) = B⁻¹ := by module + exact le_of_eq ((congrArg (·⁻¹) h1).trans h2.symm) by_cases ht_one : t = 1 · subst ht_one - simp + have h1 : ((1 : ℝ) • A + ((1 : ℝ) - 1) • B : Matrix m m ℂ) = A := by module + have h2 : ((1 : ℝ) • A⁻¹ + ((1 : ℝ) - 1) • B⁻¹ : Matrix m m ℂ) = A⁻¹ := by module + exact le_of_eq ((congrArg (·⁻¹) h1).trans h2.symm) have ht_pos : 0 < t := lt_of_le_of_ne ht0 (Ne.symm ht_zero) have h1t_pos : 0 < 1 - t := by have ht1' : t < 1 := lt_of_le_of_ne ht1 ht_one @@ -495,8 +509,17 @@ private lemma inv_lowner_convex_le {m : Type*} [Fintype m] [DecidableEq m] have hB_blk : (Matrix.fromBlocks B 1 1 B⁻¹).PosSemidef := fromBlocks_inv_posSemidef hB have hsum : (t • Matrix.fromBlocks A 1 1 A⁻¹ + (1 - t) • Matrix.fromBlocks B 1 1 B⁻¹).PosSemidef := by - exact (Matrix.PosSemidef.add (Matrix.PosSemidef.smul hA_blk ht0) - (Matrix.PosSemidef.smul hB_blk (by linarith))) + have hA_smul : + t • Matrix.fromBlocks A 1 1 A⁻¹ = ((t : ℂ)) • Matrix.fromBlocks A 1 1 A⁻¹ := by + ext i j; simp [Matrix.smul_apply, Complex.real_smul] + have hB_smul : + (1 - t) • Matrix.fromBlocks B 1 1 B⁻¹ = + ((1 - t : ℝ) : ℂ) • Matrix.fromBlocks B 1 1 B⁻¹ := by + ext i j; simp [Matrix.smul_apply, Complex.real_smul] + rw [hA_smul, hB_smul] + refine (Matrix.PosSemidef.smul hA_blk ?_).add (Matrix.PosSemidef.smul hB_blk ?_) + · exact_mod_cast ht0 + · exact_mod_cast (by linarith : (0 : ℝ) ≤ 1 - t) have hblocks_eq : t • Matrix.fromBlocks A 1 1 A⁻¹ + (1 - t) • Matrix.fromBlocks B 1 1 B⁻¹ = Matrix.fromBlocks C 1 1 (t • A⁻¹ + (1 - t) • B⁻¹) := by @@ -558,7 +581,12 @@ private lemma resolvent_lowner_concave_le {m : Type*} [Fintype m] [DecidableEq m have hconv_psd : (t • A'⁻¹ + (1 - t) • B'⁻¹ - C'⁻¹).PosSemidef := by simpa [Matrix.le_iff] using hconv have hconv_psd' : (r • (t • A'⁻¹ + (1 - t) • B'⁻¹ - C'⁻¹)).PosSemidef := by - exact hconv_psd.smul (by linarith : 0 ≤ r) + have hr_smul : + r • (t • A'⁻¹ + (1 - t) • B'⁻¹ - C'⁻¹) = + ((r : ℂ)) • (t • A'⁻¹ + (1 - t) • B'⁻¹ - C'⁻¹) := by + ext i j; simp [Matrix.smul_apply, Complex.real_smul] + rw [hr_smul] + exact hconv_psd.smul (by exact_mod_cast (show (0 : ℝ) ≤ r by linarith)) rw [Matrix.le_iff] -- Reduce to the PSD of the inverse convexity difference. have hcalc : @@ -567,6 +595,18 @@ private lemma resolvent_lowner_concave_le {m : Type*} [Fintype m] [DecidableEq m module simpa [hcalc, A', B', C', C] using hconv_psd' +section RpowOperatorConcaveAux + +-- Activate the linfty operator norm tower on `Matrix _ _ ℂ` for the proof of +-- `rpow_operator_concave_le` below. These instances are defined as `local +-- instance` in Mathlib and need to be re-activated with `attribute [local +-- instance]` here so that `Integrable.smul`, `integral_smul`, `integral_mono_ae` +-- etc. can synthesise the required typeclass tower. +attribute [local instance] Matrix.linftyOpNormedRing + Matrix.linftyOpNormedAlgebra Matrix.linftyOpIsBoundedSMul + Matrix.linftyOpNormSMulClass Matrix.linftyOpNormedAddCommGroup + Matrix.linftyOpNonUnitalNormedRing + /-- Core operator concavity lemma for matrices. Uses the integral representation of xˢ and resolvent operator concavity. @@ -580,7 +620,7 @@ for any PSD matrices A, B and t ∈ [0,1]. 2. Identify the integrand with the resolvent form `1 - u * (x + u)⁻¹` using CFC. 3. Apply the resolvent operator concavity inequality pointwise in u. 4. Integrate and rewrite with `matrixFunction_rpow_eq` to conclude the inequality. -/ -private lemma rpow_operator_concave_le {m : Type*} [Fintype m] [DecidableEq m] [Fintype (m × m)] +private lemma rpow_operator_concave_le {m : Type*} [Fintype m] [DecidableEq m] {s : ℝ} (hs0 : 0 < s) (hs1 : s ≤ 1) (A B : Matrix m m ℂ) (hA : A.PosSemidef) (hB : B.PosSemidef) (t : ℝ) (ht0 : 0 ≤ t) (ht1 : t ≤ 1) @@ -592,26 +632,72 @@ private lemma rpow_operator_concave_le {m : Type*} [Fintype m] [DecidableEq m] [ by_cases hs_eq : s = 1 · subst hs_eq simp [Real.rpow_one, matrixFunction_id] - letI : NormedRing (Matrix m m ℂ) := Matrix.linftyOpNormedRing - letI : NormedAlgebra ℝ (Matrix m m ℂ) := Matrix.linftyOpNormedAlgebra - letI : CompleteSpace (Matrix m m ℂ) := by infer_instance + -- The `attribute [local instance]` directives at the top of this + -- `RpowOperatorConcaveAux` section activate the linfty operator-norm tower + -- on `Matrix _ _ ℂ`. We additionally need to pin a few non-instance + -- theorems and routes that Mathlib v4.30 does not pick up automatically. letI : NonUnitalCStarAlgebra (Matrix m m ℂ) := by simpa [CStarMatrix] using (CStarMatrix.instNonUnitalCStarAlgebra (n := m) (A := ℂ)) - letI : NonUnitalContinuousFunctionalCalculus ℝ (Matrix m m ℂ) IsSelfAdjoint := by - infer_instance + letI nucfc : NonUnitalContinuousFunctionalCalculus ℝ (Matrix m m ℂ) IsSelfAdjoint := by + letI : CStarAlgebra (Matrix m m ℂ) := by + simpa [CStarMatrix] using (CStarMatrix.instCStarAlgebra (n := m) (A := ℂ)) + letI : ContinuousFunctionalCalculus ℂ (Matrix m m ℂ) IsStarNormal := + IsStarNormal.instContinuousFunctionalCalculus + letI : ContinuousFunctionalCalculus ℝ (Matrix m m ℂ) IsSelfAdjoint := + IsSelfAdjoint.instContinuousFunctionalCalculus + exact ContinuousFunctionalCalculus.toNonUnital + letI scc : SMulCommClass ℝ (Matrix m m ℂ) (Matrix m m ℂ) := + Matrix.Semiring.smulCommClass + letI ist : IsScalarTower ℝ (Matrix m m ℂ) (Matrix m m ℂ) := inferInstance + letI sor : StarOrderedRing (Matrix m m ℂ) := Matrix.instStarOrderedRing + letI nsc : NonnegSpectrumClass ℝ (Matrix m m ℂ) := Matrix.instNonnegSpectrumClass + -- `integral_mono_ae` requires `ClosedIciTopology` on the target. The Löwner + -- order on `Matrix m m ℂ` makes `Set.Ici a` closed because `PosSemidef` is a + -- closed condition: it is the intersection of `IsHermitian` (closed under + -- `star`) and `∀ y, 0 ≤ star y ⬝ᵥ M.mulVec y` (each is a closed condition + -- since the dot-product map is continuous). + letI cit : ClosedIciTopology (Matrix m m ℂ) := by + refine ⟨fun a => ?_⟩ + have hSet : Set.Ici a = {M : Matrix m m ℂ | (M - a).PosSemidef} := by + ext M; exact Matrix.le_iff + rw [hSet] + have hcont : Continuous fun M : Matrix m m ℂ => M - a := by fun_prop + suffices hPSD : IsClosed {M : Matrix m m ℂ | M.PosSemidef} from + hPSD.preimage hcont + have heq : {M : Matrix m m ℂ | M.PosSemidef} = + {M | M.IsHermitian} ∩ ⋂ y : m → ℂ, {M | 0 ≤ star y ⬝ᵥ M.mulVec y} := by + ext M + simp only [Set.mem_setOf_eq, Set.mem_inter_iff, Set.mem_iInter] + exact Matrix.posSemidef_iff_dotProduct_mulVec + rw [heq] + refine IsClosed.inter ?_ ?_ + · -- {M | M.IsHermitian} = {M | M.conjTranspose = M} + exact isClosed_eq (by fun_prop) continuous_id + · refine isClosed_iInter (fun y => ?_) + exact isClosed_le continuous_const (by fun_prop) have hs_lt : s < 1 := lt_of_le_of_ne hs1 hs_eq let q : ℝ≥0 := ⟨s, le_of_lt hs0⟩ have hq : (q : ℝ) ∈ Set.Ioo (0 : ℝ) 1 := ⟨hs0, hs_lt⟩ obtain ⟨μ, hμ⟩ := - CFC.exists_measure_nnrpow_eq_integral_cfcₙ_rpowIntegrand₀₁ - (A := Matrix m m ℂ) hq + @CFC.exists_measure_nnrpow_eq_integral_cfcₙ_rpowIntegrand₀₁ (Matrix m m ℂ) + inferInstance inferInstance inferInstance scc ist inferInstance sor + nsc nucfc inferInstance q hq set C : Matrix m m ℂ := t • A + (1 - t) • B have hA0 : (0 : Matrix m m ℂ) ≤ A := by simpa [Matrix.le_iff] using hA have hB0 : (0 : Matrix m m ℂ) ≤ B := by simpa [Matrix.le_iff] using hB - have hCpsd : C.PosSemidef := (hA.smul ht0).add (hB.smul (by linarith)) + have hCpsd : C.PosSemidef := by + have hA_smul : t • A = ((t : ℂ)) • A := by + ext i j; simp [Matrix.smul_apply, Complex.real_smul] + have hB_smul : (1 - t) • B = ((1 - t : ℝ) : ℂ) • B := by + ext i j; simp [Matrix.smul_apply, Complex.real_smul] + refine (Matrix.PosSemidef.add ?_ ?_) + · rw [show t • A = ((t : ℂ)) • A from hA_smul] + exact hA.smul (by exact_mod_cast ht0) + · rw [show (1 - t) • B = ((1 - t : ℝ) : ℂ) • B from hB_smul] + exact hB.smul (by exact_mod_cast (show (0 : ℝ) ≤ 1 - t by linarith)) have hC0 : (0 : Matrix m m ℂ) ≤ C := by simpa [Matrix.le_iff, C] using hCpsd have hA_int : IntegrableOn (fun u => cfcₙ (rpowIntegrand₀₁ q u) A) (Ioi 0) μ := @@ -769,6 +855,9 @@ private lemma rpow_operator_concave_le {m : Type*} [Fintype m] [DecidableEq m] [ ((1 : Matrix m m ℂ) - (u : ℂ) • (C + (u : ℂ) • 1)⁻¹) := by have hnonneg : 0 ≤ u ^ (s - 1) := by exact Real.rpow_nonneg (le_of_lt hu') _ + have hnonneg_C : (0 : ℂ) ≤ ((u ^ (s - 1) : ℝ) : ℂ) := by + rw [show (0 : ℂ) = ((0 : ℝ) : ℂ) from rfl, Complex.real_le_real] + exact hnonneg rw [Matrix.le_iff] at hres_le ⊢ have hpsd : (((u ^ (s - 1) : ℝ) : ℂ) • @@ -776,7 +865,7 @@ private lemma rpow_operator_concave_le {m : Type*} [Fintype m] [DecidableEq m] [ ((u ^ (s - 1) : ℝ) : ℂ) • (t • ((1 : Matrix m m ℂ) - (u : ℂ) • (A + (u : ℂ) • 1)⁻¹) + (1 - t) • ((1 : Matrix m m ℂ) - (u : ℂ) • (B + (u : ℂ) • 1)⁻¹))).PosSemidef := by - simpa [smul_sub] using hres_le.smul hnonneg + simpa [smul_sub] using hres_le.smul hnonneg_C simpa [smul_sub] using hpsd -- Replace with the matrixFunction form. have hscale' : @@ -788,17 +877,34 @@ private lemma rpow_operator_concave_le {m : Type*} [Fintype m] [DecidableEq m] [ have hscale' := hscale rw [hA_res.symm, hB_res.symm, hC_res.symm] at hscale' exact hscale' - simpa [hA_eq, hB_eq, hC_eq, hA_int', hB_int', hC_int', smul_add, smul_smul, - mul_comm, mul_left_comm, mul_assoc] using hscale' + have hscale'' : + t • ((u ^ (s - 1) : ℝ) : ℂ) • + matrixFunction (fun x => ((1 - u * (x + u)⁻¹ : ℝ) : ℂ)) A hA.1 + + (1 - t) • ((u ^ (s - 1) : ℝ) : ℂ) • + matrixFunction (fun x => ((1 - u * (x + u)⁻¹ : ℝ) : ℂ)) B hB.1 ≤ + ((u ^ (s - 1) : ℝ) : ℂ) • + matrixFunction (fun x => ((1 - u * (x + u)⁻¹ : ℝ) : ℂ)) C hCpsd.1 := by + rw [smul_comm t ((u ^ (s - 1) : ℝ) : ℂ), + smul_comm (1 - t) ((u ^ (s - 1) : ℝ) : ℂ), ← smul_add] + exact hscale' + simpa [hA_eq, hB_eq, hC_eq, hA_int', hB_int', hC_int'] using hscale'' have hle_integral : t • (∫ u in Ioi 0, cfcₙ (rpowIntegrand₀₁ q u) A ∂μ) + (1 - t) • (∫ u in Ioi 0, cfcₙ (rpowIntegrand₀₁ q u) B ∂μ) ≤ ∫ u in Ioi 0, cfcₙ (rpowIntegrand₀₁ q u) C ∂μ := by + have hAi : Integrable (fun u => cfcₙ (rpowIntegrand₀₁ q u) A) (μ.restrict (Ioi 0)) := + hA_int.integrable + have hBi : Integrable (fun u => cfcₙ (rpowIntegrand₀₁ q u) B) (μ.restrict (Ioi 0)) := + hB_int.integrable + have hA_smul : Integrable (fun u => t • cfcₙ (rpowIntegrand₀₁ q u) A) + (μ.restrict (Ioi 0)) := hAi.smul (𝕜 := ℝ) t + have hB_smul : Integrable (fun u => (1 - t) • cfcₙ (rpowIntegrand₀₁ q u) B) + (μ.restrict (Ioi 0)) := hBi.smul (𝕜 := ℝ) (1 - t) have hleft_int : Integrable (fun u => t • cfcₙ (rpowIntegrand₀₁ q u) A + - (1 - t) • cfcₙ (rpowIntegrand₀₁ q u) B) (μ.restrict (Ioi 0)) := by - exact (hA_int.smul t).add (hB_int.smul (1 - t)) + (1 - t) • cfcₙ (rpowIntegrand₀₁ q u) B) (μ.restrict (Ioi 0)) := + hA_smul.add hB_smul have hright_int : Integrable (fun u => cfcₙ (rpowIntegrand₀₁ q u) C) (μ.restrict (Ioi 0)) := hC_int @@ -818,28 +924,35 @@ private lemma rpow_operator_concave_le {m : Type*} [Fintype m] [DecidableEq m] [ · exact hB_int.smul (1 - t) _ = t • (∫ u in Ioi 0, cfcₙ (rpowIntegrand₀₁ q u) A ∂μ) + (1 - t) • (∫ u in Ioi 0, cfcₙ (rpowIntegrand₀₁ q u) B ∂μ) := by - simp [integral_smul] + congr 1 + · exact hAi.integral_smul (R := ℝ) t + · exact hBi.integral_smul (R := ℝ) (1 - t) have hmono' : t • (∫ u in Ioi 0, cfcₙ (rpowIntegrand₀₁ q u) A ∂μ) + (1 - t) • (∫ u in Ioi 0, cfcₙ (rpowIntegrand₀₁ q u) B ∂μ) ≤ ∫ u in Ioi 0, cfcₙ (rpowIntegrand₀₁ q u) C ∂μ := by simpa [hleft_eq] using hmono exact hmono' + have hq_pos : 0 < (q : ℝ) := by exact_mod_cast hs0 + have hqs : (q : ℝ) = s := rfl have hA_eq_int : A ^ s = ∫ u in Ioi 0, cfcₙ (rpowIntegrand₀₁ q u) A ∂μ := by - have hq_pos : 0 < (q : ℝ) := by exact_mod_cast hs0 - simpa [CFC.nnrpow_eq_rpow (A := Matrix m m ℂ) (a := A) (x := q) hq_pos] using - (hμ A hA0).2 + have h1 : A ^ q = A ^ (q : ℝ) := + CFC.nnrpow_eq_rpow (A := Matrix m m ℂ) (a := A) (x := q) hq_pos + have h2 : A ^ q = ∫ u in Ioi 0, cfcₙ (rpowIntegrand₀₁ q u) A ∂μ := (hμ A hA0).2 + rw [← hqs, ← h1]; exact h2 have hB_eq_int : B ^ s = ∫ u in Ioi 0, cfcₙ (rpowIntegrand₀₁ q u) B ∂μ := by - have hq_pos : 0 < (q : ℝ) := by exact_mod_cast hs0 - simpa [CFC.nnrpow_eq_rpow (A := Matrix m m ℂ) (a := B) (x := q) hq_pos] using - (hμ B hB0).2 + have h1 : B ^ q = B ^ (q : ℝ) := + CFC.nnrpow_eq_rpow (A := Matrix m m ℂ) (a := B) (x := q) hq_pos + have h2 : B ^ q = ∫ u in Ioi 0, cfcₙ (rpowIntegrand₀₁ q u) B ∂μ := (hμ B hB0).2 + rw [← hqs, ← h1]; exact h2 have hC_eq_int : C ^ s = ∫ u in Ioi 0, cfcₙ (rpowIntegrand₀₁ q u) C ∂μ := by - have hq_pos : 0 < (q : ℝ) := by exact_mod_cast hs0 - simpa [CFC.nnrpow_eq_rpow (A := Matrix m m ℂ) (a := C) (x := q) hq_pos] using - (hμ C hC0).2 + have h1 : C ^ q = C ^ (q : ℝ) := + CFC.nnrpow_eq_rpow (A := Matrix m m ℂ) (a := C) (x := q) hq_pos + have h2 : C ^ q = ∫ u in Ioi 0, cfcₙ (rpowIntegrand₀₁ q u) C ∂μ := (hμ C hC0).2 + rw [← hqs, ← h1]; exact h2 have hC_eq_mf : matrixFunction (fun x => ((x ^ s : ℝ) : ℂ)) C hC = C ^ s := by have hC' : @@ -863,6 +976,8 @@ private lemma rpow_operator_concave_le {m : Type*} [Fintype m] [DecidableEq m] [ simpa [hA_eq_int, hB_eq_int, hC_eq_int] using hle_integral simpa [hA_eq_mf, hB_eq_mf, hC_eq_mf, C] using hfinal +end RpowOperatorConcaveAux + /-- Helper: The difference in quadratic forms for operator concavity. -/ private lemma rpow_concavity_quadform_nonneg {m : Type*} [Fintype m] [DecidableEq m] {s : ℝ} (hs0 : 0 < s) (hs1 : s ≤ 1) diff --git a/QuantumSystem/Analysis/Matrix/PosDef.lean b/QuantumSystem/Analysis/Matrix/PosDef.lean index 452631e..69bd421 100644 --- a/QuantumSystem/Analysis/Matrix/PosDef.lean +++ b/QuantumSystem/Analysis/Matrix/PosDef.lean @@ -23,11 +23,12 @@ namespace Matrix open scoped ComplexOrder /-- A strictly positive convex combination of positive definite matrices is positive definite. -/ -lemma PosDef.convex_comb {m : Type*} [Fintype m] +lemma PosDef.convex_comb {m : Type*} [Finite m] {A B : Matrix m m ℂ} (hA : A.PosDef) (hB : B.PosDef) {t : ℝ} (ht0 : 0 < t) (ht1 : 0 < 1 - t) : (t • A + (1 - t) • B).PosDef := by classical + letI := Fintype.ofFinite m refine Matrix.PosDef.of_dotProduct_mulVec_pos ?_ ?_ · exact (hA.1.smul_real t).add (hB.1.smul_real (1 - t)) · intro x hx @@ -40,21 +41,26 @@ lemma PosDef.convex_comb {m : Type*} [Fintype m] have hC_re : (star x ⬝ᵥ ((t • A + (1 - t) • B) *ᵥ x)).re = t * (star x ⬝ᵥ (A *ᵥ x)).re + (1 - t) * (star x ⬝ᵥ (B *ᵥ x)).re := by - simp [add_mulVec, smul_mulVec, dotProduct_add, dotProduct_smul, - Complex.add_re, Complex.real_smul] + have htA : (t • A) *ᵥ x = t • (A *ᵥ x) := smul_mulVec _ _ _ + have htB : ((1 - t) • B) *ᵥ x = (1 - t) • (B *ᵥ x) := smul_mulVec _ _ _ + have hsmA : star x ⬝ᵥ (t • (A *ᵥ x)) = t • (star x ⬝ᵥ (A *ᵥ x)) := + dotProduct_smul (R := ℝ) t (star x) (A *ᵥ x) + have hsmB : star x ⬝ᵥ ((1 - t) • (B *ᵥ x)) = (1 - t) • (star x ⬝ᵥ (B *ᵥ x)) := + dotProduct_smul (R := ℝ) (1 - t) (star x) (B *ᵥ x) + rw [add_mulVec, dotProduct_add, htA, htB, hsmA, hsmB, Complex.add_re, + Complex.smul_re, Complex.smul_re] + simp [smul_eq_mul] refine (RCLike.pos_iff).2 ?_ constructor - · have hA' : 0 < t * (star x ⬝ᵥ (A *ᵥ x)).re := by - exact mul_pos ht0 hA_re - have hB' : 0 < (1 - t) * (star x ⬝ᵥ (B *ᵥ x)).re := by - exact mul_pos ht1 hB_re + · have hA' : 0 < t * (star x ⬝ᵥ (A *ᵥ x)).re := mul_pos ht0 hA_re + have hB' : 0 < (1 - t) * (star x ⬝ᵥ (B *ᵥ x)).re := mul_pos ht1 hB_re have hsum : 0 < t * (star x ⬝ᵥ (A *ᵥ x)).re + (1 - t) * (star x ⬝ᵥ (B *ᵥ x)).re := add_pos hA' hB' simpa [hC_re] using hsum · exact hC_im /-- Convex combination of PD matrices with nonnegative weights is PD. -/ -lemma PosDef.convex_comb_nonneg {m : Type*} [Fintype m] +lemma PosDef.convex_comb_nonneg {m : Type*} [Finite m] {A B : Matrix m m ℂ} (hA : A.PosDef) (hB : B.PosDef) {w₁ w₂ : ℝ} (hw₁ : 0 ≤ w₁) (hw₂ : 0 ≤ w₂) (hw : w₁ + w₂ = 1) : (w₁ • A + w₂ • B).PosDef := by @@ -62,12 +68,14 @@ lemma PosDef.convex_comb_nonneg {m : Type*} [Fintype m] · have h₂ : w₂ = 1 := by linarith [hw, h₁] subst h₁ subst h₂ - simpa using hB + convert hB using 1 + module by_cases h₂ : w₂ = 0 · have h₁' : w₁ = 1 := by linarith [hw, h₂] subst h₂ subst h₁' - simpa using hA + convert hA using 1 + module have hw₁pos : 0 < w₁ := lt_of_le_of_ne hw₁ (Ne.symm h₁) have hw₂pos : 0 < w₂ := lt_of_le_of_ne hw₂ (Ne.symm h₂) have hw₂' : w₂ = 1 - w₁ := by linarith [hw] diff --git a/QuantumSystem/Channel.lean b/QuantumSystem/Channel.lean index adb771c..a9a9a07 100644 --- a/QuantumSystem/Channel.lean +++ b/QuantumSystem/Channel.lean @@ -191,6 +191,9 @@ lemma stinespringIsometry_conjTranspose_mul {r : ℕ} [DecidableEq n] Matrix.of_apply, Matrix.one_apply, Fintype.sum_prod_type] have heq : ∀ i, ∑ j : m, star (K i j a) * K i j b = ((K i)ᴴ * K i) a b := fun i => by simp only [Matrix.mul_apply, Matrix.conjTranspose_apply] - simp only [heq, ← Finset.sum_apply, hK, Matrix.one_apply] + simp only [heq, ← Finset.sum_apply] + calc (∑ c, (K c)ᴴ * K c) a b + = (1 : Matrix n n ℂ) a b := by rw [hK] + _ = if a = b then 1 else 0 := Matrix.one_apply end Matrix diff --git a/QuantumSystem/ForMathlib/Analysis/CStarAlgebra/Ideal.lean b/QuantumSystem/ForMathlib/Analysis/CStarAlgebra/Ideal.lean index 2f15847..ff64566 100644 --- a/QuantumSystem/ForMathlib/Analysis/CStarAlgebra/Ideal.lean +++ b/QuantumSystem/ForMathlib/Analysis/CStarAlgebra/Ideal.lean @@ -19,8 +19,8 @@ def leftRel (I : CStarAlgebraIdeal A) : Setoid A := QuotientAddGroup.leftRel I.toAddSubgroup /-- The quotient of a C*-algebra by an ideal. -/ -instance instHasQuotient : HasQuotient A (CStarAlgebraIdeal A) where - quotient' I := Quotient (leftRel I) +instance instHasQuotient : HasQuotient A (CStarAlgebraIdeal A) := + ⟨fun I => Quotient (leftRel I)⟩ instance : SetLike (CStarAlgebraIdeal A) A where coe I := I.carrier diff --git a/QuantumSystem/ForMathlib/Analysis/CStarAlgebra/WeakDual.lean b/QuantumSystem/ForMathlib/Analysis/CStarAlgebra/WeakDual.lean index 8ab1879..6a5a713 100644 --- a/QuantumSystem/ForMathlib/Analysis/CStarAlgebra/WeakDual.lean +++ b/QuantumSystem/ForMathlib/Analysis/CStarAlgebra/WeakDual.lean @@ -3,7 +3,7 @@ module public import Mathlib.Analysis.CStarAlgebra.Classes public import Mathlib.Analysis.Normed.Order.Lattice public import Mathlib.GroupTheory.MonoidLocalization.Basic -public import Mathlib.Topology.Algebra.Module.WeakDual +public import Mathlib.Topology.Algebra.Module.Spaces.WeakDual @[expose] public section @@ -32,22 +32,24 @@ lemma add {φ ψ : WeakDual ℂ A} (hφ : IsPositive A φ) (hψ : IsPositive A intro a obtain ⟨r, hr⟩ := hφ a obtain ⟨s, hs⟩ := hψ a - use r + s - change (φ + ψ : A →L[ℂ] ℂ) (star a * a) = _ - erw [ContinuousLinearMap.add_apply] - rw [hr, hs] - simp only [RCLike.ofReal_add, NNReal.coe_add] + refine ⟨r + s, ?_⟩ + have hsum : (φ + ψ) (star a * a) = φ (star a * a) + ψ (star a * a) := rfl + rw [hsum, hr, hs] + push_cast + rfl lemma smul {φ : WeakDual ℂ A} (hφ : IsPositive A φ) {c : ℝ≥0} : IsPositive A (c • φ) := by intro a obtain ⟨r, hr⟩ := hφ a - use c * r - change (c • φ : A →L[ℂ] ℂ) (star a * a) = _ - erw [ContinuousLinearMap.smul_apply] - rw [hr] - simp only [RCLike.ofReal_mul, NNReal.coe_mul] - rw [Algebra.smul_def] + refine ⟨c * r, ?_⟩ + -- `c • φ` for `c : ℝ≥0` acts on the underlying CLM via the `ℝ`-cast (NNReal.smul_def). + have hsmul : (c • φ) (star a * a) = ((c : ℝ) : ℂ) * φ (star a * a) := by + have : (c • φ) (star a * a) = ((c : ℝ) : ℂ) • φ (star a * a) := by + rw [NNReal.smul_def]; rfl + rw [this, smul_eq_mul] + rw [hsmul, hr] + push_cast rfl lemma isClosed : IsClosed { φ : WeakDual ℂ A | IsPositive A φ } := by diff --git a/QuantumSystem/ForMathlib/Analysis/Calculus/Deriv/Sign.lean b/QuantumSystem/ForMathlib/Analysis/Calculus/Deriv/Sign.lean index 94534ba..c4fadf5 100644 --- a/QuantumSystem/ForMathlib/Analysis/Calculus/Deriv/Sign.lean +++ b/QuantumSystem/ForMathlib/Analysis/Calculus/Deriv/Sign.lean @@ -21,7 +21,7 @@ lemma deriv_nonpos_of_forall_lt_min (g : ℝ → ℝ) (d : ℝ) (x₀ ε : ℝ) (hd : HasDerivAt g d x₀) (hmin : ∀ y ∈ Set.Ioo (x₀ - ε) x₀, g x₀ ≤ g y) : d ≤ 0 := by rw [hasDerivAt_iff_tendsto_slope] at hd haveI : (nhdsWithin x₀ (Set.Iio x₀)).NeBot := - nhdsWithin_Iio_self_neBot' ⟨x₀ - 1, by simp [Set.mem_Iio]⟩ + nhdsLT_neBot_of_exists_lt ⟨x₀ - 1, by linarith⟩ have hiio_sub : Set.Iio x₀ ⊆ {x₀}ᶜ := fun y hy => by simp [(Set.mem_Iio.mp hy).ne] have hslope2 := hd.mono_left (nhdsWithin_mono x₀ hiio_sub) diff --git a/QuantumSystem/ForMathlib/Analysis/Matrix/Basic.lean b/QuantumSystem/ForMathlib/Analysis/Matrix/Basic.lean index b239a0b..68e06ee 100644 --- a/QuantumSystem/ForMathlib/Analysis/Matrix/Basic.lean +++ b/QuantumSystem/ForMathlib/Analysis/Matrix/Basic.lean @@ -1,9 +1,12 @@ module public import Mathlib.Analysis.CStarAlgebra.CStarMatrix +public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi public import Mathlib.Analysis.Matrix.Order public import Mathlib.Analysis.CStarAlgebra.Classes +public import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic public import Mathlib.Data.Matrix.ColumnRowPartitioned +public import Mathlib.LinearAlgebra.Complex.FiniteDimensional /-! # Block-Matrix Lemmas @@ -35,6 +38,8 @@ This file collects block-matrix identities used in the HPJ and related inequalit semidefinite. - `Matrix.PosSemidef.one_sub_fromRows`: if AᴴA + BᴴB ≤ I, then I − VᴴV is PSD for V = [A; B]. +- `Matrix.PosSemidef.real_smul`: scaling a PSD matrix by a nonnegative real scalar gives a PSD + matrix. - `Matrix.PosSemidef.smul_nonpos`: scaling a PSD matrix by a nonpositive real scalar gives a matrix ≤ 0. - `Matrix.PosSemidef.add_smul_one_posDef`: A + rI is positive definite for A ≥ 0, r > 0. @@ -73,7 +78,7 @@ lemma fromBlocks_mulVec_inr {m n : Type*} [Fintype m] [Fintype n] `(fromRows A B)ᴴ * fromBlocks T₁ 0 0 T₂ * fromRows A B = Aᴴ * T₁ * A + Bᴴ * T₂ * B`. This is useful for reducing block-matrix inequalities to separate inequalities for each block. -/ lemma fromRows_compress_blockDiag - {m₁ m₂ n : Type*} [Fintype m₁] [Fintype m₂] [Fintype n] + {m₁ m₂ n : Type*} [Fintype m₁] [Fintype m₂] (A : Matrix m₁ n ℂ) (B : Matrix m₂ n ℂ) (T₁ : Matrix m₁ m₁ ℂ) (T₂ : Matrix m₂ m₂ ℂ) : (Matrix.fromRows A B)ᴴ * (Matrix.fromBlocks T₁ 0 0 T₂) * Matrix.fromRows A B = @@ -143,6 +148,9 @@ lemma rpow_unitary_conj {n : Type*} [Fintype n] [DecidableEq n] letI : NormedRing (Matrix n n ℂ) := Matrix.linftyOpNormedRing letI : NormedAlgebra ℝ (Matrix n n ℂ) := Matrix.linftyOpNormedAlgebra letI : NormedAlgebra ℂ (Matrix n n ℂ) := Matrix.linftyOpNormedAlgebra + letI : NormedSpace ℝ (Matrix n n ℂ) := NormedAlgebra.toNormedSpace _ + letI : IsBoundedSMul ℝ (Matrix n n ℂ) := NormedSpace.toIsBoundedSMul (𝕜 := ℝ) + letI : ContinuousSMul ℝ (Matrix n n ℂ) := IsBoundedSMul.continuousSMul letI : CStarAlgebra (Matrix n n ℂ) := by simpa [CStarMatrix] using CStarMatrix.instCStarAlgebra (n := n) (A := ℂ) -- Convert to unitary element @@ -159,9 +167,14 @@ lemma rpow_unitary_conj {n : Type*} [Fintype n] [DecidableEq n] rw [CFC.rpow_eq_cfc_real (a := φ M) (ha := by rw [hφ_apply]; exact hM')] have hcont : ContinuousOn (· ^ p) (spectrum ℝ M) := (Real.continuous_rpow_const hp).continuousOn - -- Continuity of φ follows from finite-dimensionality - have hφ_cont : Continuous φ := - φ.toAlgEquiv.toLinearMap.continuous_of_finiteDimensional + -- Continuity of φ follows from finite-dimensionality. Build the FiniteDimensional + -- instance locally inside the `have`-block so the instance database stays focused. + -- φ is x ↦ U * x * Uᴴ, which is continuous as a composition of multiplications. + have hφ_cont : Continuous φ := by + have hfun : (φ : Matrix n n ℂ → Matrix n n ℂ) = fun x => U * x * Uᴴ := + funext hφ_apply + rw [show ⇑φ = fun x => U * x * Uᴴ from hfun] + exact (continuous_const.mul continuous_id).mul continuous_const -- IsSelfAdjoint φ M follows from M being self-adjoint and φ preserving star have hM_sa : IsSelfAdjoint M := by have : M.PosSemidef := by simpa [Matrix.le_iff] using hM @@ -191,8 +204,33 @@ lemma diagonal_rpow {n : Type*} [Fintype n] [DecidableEq n] letI : NormedRing (Matrix n n ℂ) := Matrix.linftyOpNormedRing letI : NormedAlgebra ℝ (Matrix n n ℂ) := Matrix.linftyOpNormedAlgebra letI : NormedAlgebra ℂ (Matrix n n ℂ) := Matrix.linftyOpNormedAlgebra + letI : NormedSpace ℝ (Matrix n n ℂ) := NormedAlgebra.toNormedSpace _ + letI : IsBoundedSMul ℝ (Matrix n n ℂ) := NormedSpace.toIsBoundedSMul (𝕜 := ℝ) + letI : ContinuousSMul ℝ (Matrix n n ℂ) := IsBoundedSMul.continuousSMul + haveI : Module.Free ℝ ℂ := Module.Free.of_divisionRing _ _ + haveI : Module.Finite ℝ ℂ := inferInstance + haveI : Module.Finite ℝ (Matrix n n ℂ) := Module.Finite.matrix letI : CStarAlgebra (Matrix n n ℂ) := by simpa [CStarMatrix] using CStarMatrix.instCStarAlgebra (n := n) (A := ℂ) + letI : NormedSpace ℝ (n → ℂ) := inferInstance + letI : IsBoundedSMul ℝ (n → ℂ) := NormedSpace.toIsBoundedSMul (𝕜 := ℝ) + letI : ContinuousSMul ℝ (n → ℂ) := IsBoundedSMul.continuousSMul + haveI : Module.Free ℝ ℂ := Module.Free.of_divisionRing _ _ + haveI : Module.Finite ℝ ℂ := inferInstance + haveI : Module.Finite ℝ (n → ℂ) := Module.Finite.pi + -- Provide CFC instances for the Pi C*-algebra `n → ℂ` and the fiber `ℂ`. These are not + -- registered globally in Mathlib (`IsStarNormal.instContinuousFunctionalCalculus` is a + -- `theorem` with `attribute [local instance]` only), but follow once the appropriate + -- normed/CStar structure is in scope. + letI : ContinuousFunctionalCalculus ℂ ℂ IsStarNormal := + IsStarNormal.instContinuousFunctionalCalculus + letI : ContinuousFunctionalCalculus ℝ ℂ IsSelfAdjoint := + IsSelfAdjoint.instContinuousFunctionalCalculus + letI : CStarAlgebra (n → ℂ) := inferInstance + letI : ContinuousFunctionalCalculus ℂ (n → ℂ) IsStarNormal := + IsStarNormal.instContinuousFunctionalCalculus + letI : ContinuousFunctionalCalculus ℝ (n → ℂ) IsSelfAdjoint := + IsSelfAdjoint.instContinuousFunctionalCalculus let dc : n → ℂ := fun i => (d i : ℂ) have hD_psd : (diagonal dc).PosSemidef := by rw [posSemidef_diagonal_iff] @@ -206,8 +244,10 @@ lemma diagonal_rpow {n : Type*} [Fintype n] [DecidableEq n] map_star' := fun v => by change diagonal (star v) = (diagonal v)ᴴ rw [diagonal_conjTranspose] } - have hφ_cont : Continuous φ := - φ.toAlgHom.toLinearMap.continuous_of_finiteDimensional + have hφ_cont : Continuous φ := by + have : (φ : (n → ℂ) → Matrix n n ℂ) = fun v => diagonal v := rfl + rw [show ⇑φ = fun v => diagonal v from this] + exact Continuous.matrix_diagonal continuous_id -- `dc` is self-adjoint: all entries are real, hence equal to their conjugate. have hdc_sa : IsSelfAdjoint dc := by rw [IsSelfAdjoint, Pi.star_def]; ext i; simp [dc, Complex.conj_ofReal] @@ -311,14 +351,15 @@ lemma inv_transpose_rpow_mul_transpose_eq {m : Type*} [Fintype m] [DecidableEq m congr 1 have hB_nonneg : (0 : Matrix m m ℂ) ≤ B := by simpa [Matrix.le_iff] using hB.posSemidef + have hB_sp : IsStrictlyPositive B := hB.isStrictlyPositive have hBinv_cfc : B⁻¹ = B ^ (-1 : ℝ) := by have h1 : B ^ (-1 : ℝ) * B = 1 := by - have := CFC.rpow_neg_mul_rpow (1 : ℝ) hB_unit hB_nonneg + have := CFC.rpow_neg_mul_rpow (a := B) (1 : ℝ) hB_sp rwa [CFC.rpow_one B hB_nonneg] at this have h2 : B⁻¹ * B = 1 := Matrix.nonsing_inv_mul B hB_det exact hB_unit.mul_right_cancel (h2.trans h1.symm) have hBinv_rpow : (B⁻¹) ^ p = B ^ (-p) := by - rw [hBinv_cfc, CFC.rpow_rpow B (-1 : ℝ) p hB_unit (by norm_num)] + rw [hBinv_cfc, CFC.rpow_rpow B (-1 : ℝ) p (by norm_num) hB_sp] congr 1 ring rw [hBinv_rpow] @@ -330,9 +371,10 @@ lemma inv_transpose_rpow_mul_transpose_eq {m : Type*} [Fintype m] [DecidableEq m /-! ### Positive Definite and Positive Semidefinite Matrices -/ /-- The identity matrix is positive definite. -/ -lemma posDef_one {m : Type*} [Fintype m] [DecidableEq m] : +lemma posDef_one {m : Type*} [Finite m] [DecidableEq m] : (1 : Matrix m m ℂ).PosDef := by classical + letI := Fintype.ofFinite m refine Matrix.PosDef.of_dotProduct_mulVec_pos ?_ ?_ · simp [IsHermitian] · intro x hx @@ -340,7 +382,7 @@ lemma posDef_one {m : Type*} [Fintype m] [DecidableEq m] : simpa using hpos /-- The identity matrix is positive semidefinite. -/ -lemma posSemidef_one {m : Type*} [Fintype m] [DecidableEq m] : +lemma posSemidef_one {m : Type*} [Finite m] [DecidableEq m] : (1 : Matrix m m ℂ).PosSemidef := posDef_one.posSemidef @@ -357,7 +399,7 @@ lemma fromBlocks_inv_posSemidef {m : Type*} [Fintype m] [DecidableEq m] /-- The product `(fromRows A B)ᴴ * (fromRows A B)` equals `Aᴴ * A + Bᴴ * B`. -/ lemma fromRows_conjTranspose_mul_self - {m₁ m₂ n : Type*} [Fintype m₁] [Fintype m₂] [Fintype n] + {m₁ m₂ n : Type*} [Fintype m₁] [Fintype m₂] (A : Matrix m₁ n ℂ) (B : Matrix m₂ n ℂ) : (Matrix.fromRows A B)ᴴ * Matrix.fromRows A B = Aᴴ * A + Bᴴ * B := by classical @@ -367,7 +409,7 @@ lemma fromRows_conjTranspose_mul_self namespace PosSemidef /-- Diagonal matrix with nonnegative real entries is positive semidefinite. -/ -lemma diagonal_ofReal {m : Type*} [Fintype m] [DecidableEq m] +lemma diagonal_ofReal {m : Type*} [DecidableEq m] {f : m → ℝ} (hf : ∀ i, 0 ≤ f i) : (diagonal (fun i => (f i : ℂ))).PosSemidef := by rw [posSemidef_diagonal_iff] @@ -383,33 +425,50 @@ lemma one_sub_fromRows {m : Type*} [Fintype m] [DecidableEq m] simpa [fromRows_conjTranspose_mul_self] using hAB simpa [Matrix.le_iff] using hV +/-- Scaling a PSD matrix by a nonnegative real scalar yields a PSD matrix. The real-scalar +form is convenient because `PosSMulMono ℝ ℂ` is unavailable; we route the action through +the complex coercion. -/ +lemma real_smul {m : Type*} [Finite m] + {c : ℝ} (hc : 0 ≤ c) {M : Matrix m m ℂ} (hM : M.PosSemidef) : + (c • M : Matrix m m ℂ).PosSemidef := by + letI := Fintype.ofFinite m + have hnonneg_C : (0 : ℂ) ≤ ((c : ℝ) : ℂ) := Complex.zero_le_real.mpr hc + have hsmul : (((c : ℝ) : ℂ) • M).PosSemidef := hM.smul hnonneg_C + have hreal : ((c : ℝ) : ℂ) • M = (c : ℝ) • M := by + ext i j + change ((c : ℝ) : ℂ) * M i j = (c : ℝ) • M i j + simp [Complex.real_smul] + rwa [hreal] at hsmul + /-- Scaling a PSD matrix by a nonpositive real scalar gives a matrix `≤ 0`. -/ -lemma smul_nonpos {m : Type*} [Fintype m] +lemma smul_nonpos {m : Type*} [Finite m] {c : ℝ} (hc : c ≤ 0) {M : Matrix m m ℂ} (hM : M.PosSemidef) : c • M ≤ (0 : Matrix m m ℂ) := by - have hnonneg : 0 ≤ -c := by linarith - have hsmul : ((-c) • M).PosSemidef := hM.smul hnonneg + letI := Fintype.ofFinite m + -- Work via the ℂ-action: `((-c : ℝ) : ℂ) • M` is PSD when `0 ≤ ((-c : ℝ) : ℂ)`. + have hnonneg_C : (0 : ℂ) ≤ ((-c : ℝ) : ℂ) := + Complex.zero_le_real.mpr (by linarith) + have hsmul : (((-c : ℝ) : ℂ) • M).PosSemidef := hM.smul hnonneg_C + -- ℂ-cast scalar action equals ℝ-action: pointwise on each entry. + have hreal : ((-c : ℝ) : ℂ) • M = (-c : ℝ) • M := by + ext i j + change ((-c : ℝ) : ℂ) * M i j = (-c : ℝ) • M i j + simp [Complex.real_smul] rw [Matrix.le_iff] - simpa [sub_eq_add_neg, add_comm, add_left_comm, add_assoc] using hsmul + rw [hreal] at hsmul + rw [show ((-c : ℝ) • M : Matrix m m ℂ) = -(c • M) from neg_smul c M] at hsmul + simpa [sub_eq_add_neg] using hsmul /-- Adding a positive scalar multiple of the identity to a PSD matrix gives a PD matrix. -/ -lemma add_smul_one_posDef {m : Type*} [Fintype m] [DecidableEq m] +lemma add_smul_one_posDef {m : Type*} [Finite m] [DecidableEq m] {A : Matrix m m ℂ} (hA : A.PosSemidef) {r : ℝ} (hr : 0 < r) : (A + (r : ℂ) • (1 : Matrix m m ℂ)).PosDef := by classical + letI := Fintype.ofFinite m have h1 : ((r : ℂ) • (1 : Matrix m m ℂ)).IsHermitian := by - change ((r : ℂ) • (1 : Matrix m m ℂ))ᴴ = (r : ℂ) • (1 : Matrix m m ℂ) - ext i j - by_cases h : i = j - · subst h - simp - · have h1 : (1 : Matrix m m ℂ) i j = 0 := by - simp [h] - have hji : ¬ j = i := by - simpa [eq_comm] using h - have h2 : (1 : Matrix m m ℂ) j i = 0 := by - simp [hji] - simp [Matrix.conjTranspose_apply, h1, h2] + rw [Matrix.IsHermitian, Matrix.conjTranspose_smul, Complex.star_def, + Complex.conj_ofReal] + rw [Matrix.IsHermitian.eq (Matrix.isHermitian_one : (1 : Matrix m m ℂ).IsHermitian)] refine Matrix.PosDef.of_dotProduct_mulVec_pos ?_ ?_ · exact hA.1.add h1 · intro x hx @@ -420,8 +479,8 @@ lemma add_smul_one_posDef {m : Type*} [Fintype m] [DecidableEq m] have hsum_re : (star x ⬝ᵥ ((A + (r : ℂ) • (1 : Matrix m m ℂ)) *ᵥ x)).re = (star x ⬝ᵥ (A *ᵥ x)).re + r * (star x ⬝ᵥ x).re := by - simp [add_mulVec, smul_mulVec, dotProduct_add, dotProduct_smul, - Complex.add_re, Complex.real_smul] + simp only [add_mulVec, smul_mulVec, dotProduct_add, dotProduct_smul, + Complex.add_re, Matrix.one_mulVec, smul_eq_mul, Complex.re_ofReal_mul] have hsum_im : (star x ⬝ᵥ ((A + (r : ℂ) • (1 : Matrix m m ℂ)) *ᵥ x)).im = 0 := by set M := A + (r : ℂ) • (1 : Matrix m m ℂ) @@ -454,10 +513,12 @@ end PosSemidef /-- Block diagonal `fromBlocks A 0 0 D` is PSD when both `A` and `D` are PSD. -/ lemma fromBlocks_diag_posSemidef {n₁ n₂ : Type*} - [Fintype n₁] [Fintype n₂] + [Finite n₁] [Finite n₂] {A : Matrix n₁ n₁ ℂ} (hA : A.PosSemidef) {D : Matrix n₂ n₂ ℂ} (hD : D.PosSemidef) : (Matrix.fromBlocks A 0 0 D).PosSemidef := by + letI := Fintype.ofFinite n₁ + letI := Fintype.ofFinite n₂ refine PosSemidef.of_dotProduct_mulVec_nonneg (Matrix.IsHermitian.fromBlocks hA.1 (by simp) hD.1) ?_ intro v diff --git a/QuantumSystem/ForMathlib/Analysis/Matrix/Hermitian.lean b/QuantumSystem/ForMathlib/Analysis/Matrix/Hermitian.lean index d8c3c37..36ec8c9 100644 --- a/QuantumSystem/ForMathlib/Analysis/Matrix/Hermitian.lean +++ b/QuantumSystem/ForMathlib/Analysis/Matrix/Hermitian.lean @@ -48,13 +48,13 @@ lemma IsHermitian.quadForm_im_eq_zero {m : Type*} [Fintype m] linarith /-- Sum of Hermitian matrices is Hermitian. -/ -lemma IsHermitian.add_isHermitian {m : Type*} [Fintype m] +lemma IsHermitian.add_isHermitian {m : Type*} {A B : Matrix m m ℂ} (hA : A.IsHermitian) (hB : B.IsHermitian) : (A + B).IsHermitian := hA.add hB /-- Real scalar multiple of a Hermitian matrix is Hermitian. -/ -lemma IsHermitian.smul_real {m : Type*} [Fintype m] +lemma IsHermitian.smul_real {m : Type*} {A : Matrix m m ℂ} (hA : A.IsHermitian) (r : ℝ) : (r • A).IsHermitian := by unfold IsHermitian at * @@ -62,13 +62,13 @@ lemma IsHermitian.smul_real {m : Type*} [Fintype m] simp only [RCLike.star_def, RCLike.conj_to_real] /-- Convex combination of Hermitian matrices is Hermitian. -/ -lemma IsHermitian.convex_combination {m : Type*} [Fintype m] +lemma IsHermitian.convex_combination {m : Type*} {A B : Matrix m m ℂ} (hA : A.IsHermitian) (hB : B.IsHermitian) (t : ℝ) : (t • A + (1 - t) • B).IsHermitian := (hA.smul_real t).add (hB.smul_real (1 - t)) /-- Diagonal matrix with real entries is Hermitian. -/ -lemma IsHermitian.diagonal_real {m : Type*} [Fintype m] [DecidableEq m] +lemma IsHermitian.diagonal_real {m : Type*} [DecidableEq m] (f : m → ℝ) : (diagonal (fun i => (f i : ℂ))).IsHermitian := by rw [IsHermitian, diagonal_conjTranspose] ext i j @@ -78,7 +78,7 @@ lemma IsHermitian.diagonal_real {m : Type*} [Fintype m] [DecidableEq m] · rfl /-- Complex scalar multiple of a Hermitian matrix is Hermitian when the scalar is real. -/ -lemma IsHermitian.smul_complex_real {m : Type*} [Fintype m] +lemma IsHermitian.smul_complex_real {m : Type*} {A : Matrix m m ℂ} (hA : A.IsHermitian) (r : ℝ) : ((r : ℂ) • A).IsHermitian := by unfold IsHermitian at * diff --git a/QuantumSystem/ForMathlib/Analysis/Matrix/Order.lean b/QuantumSystem/ForMathlib/Analysis/Matrix/Order.lean index 24bb2f4..387a7fd 100644 --- a/QuantumSystem/ForMathlib/Analysis/Matrix/Order.lean +++ b/QuantumSystem/ForMathlib/Analysis/Matrix/Order.lean @@ -45,7 +45,7 @@ lemma loewnerLE_trans {m : Type*} [Fintype m] [DecidableEq m] exact hbc.add hab /-- Compression preserves the Löwner order: M ≤ N ⇒ V†MV ≤ V†NV. -/ -lemma compression_le {n m : Type*} [Fintype n] [Fintype m] +lemma compression_le {n m : Type*} [Fintype n] [Finite m] {M N : Matrix n n ℂ} (h : M ≤ N) (V : Matrix n m ℂ) : Vᴴ * M * V ≤ Vᴴ * N * V := by rw [Matrix.le_iff] at h ⊢ diff --git a/QuantumSystem/ForMathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Abs.lean b/QuantumSystem/ForMathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Abs.lean index 61116bc..95f98ae 100644 --- a/QuantumSystem/ForMathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Abs.lean +++ b/QuantumSystem/ForMathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Abs.lean @@ -66,6 +66,14 @@ lemma absoluteValue_of_nonneg {T : H →L[ℂ] H} (hT : 0 ≤ T) : absoluteValue lemma absoluteValue_smul (c : ℂ) (T : H →L[ℂ] H) : absoluteValue (c • T) = ‖c‖ • absoluteValue T := by + letI : IsScalarTower ℝ ℂ H := ⟨fun r z x => by + rw [show (r • z : ℂ) = (r : ℂ) * z from rfl, mul_smul] + rfl⟩ + letI : IsScalarTower ℝ ℂ (H →L[ℂ] H) := ⟨fun r z S => by + apply ContinuousLinearMap.ext + intro x + change (r • z) • S x = r • z • S x + exact smul_assoc r z (S x)⟩ rw [absoluteValue_eq_cfc_abs, absoluteValue_eq_cfc_abs] exact CFC.abs_smul c T diff --git a/QuantumSystem/ForMathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/PartialIsometry.lean b/QuantumSystem/ForMathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/PartialIsometry.lean index 5db657a..e4d4ef7 100644 --- a/QuantumSystem/ForMathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/PartialIsometry.lean +++ b/QuantumSystem/ForMathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/PartialIsometry.lean @@ -174,7 +174,7 @@ lemma IsPartialIsometry.norm_of_mem_initialSpace {U : H →L[ℂ] H} have hP_symm : (P : H →ₗ[ℂ] H).IsSymmetric := (ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric).1 h_sa have h_orth : (LinearMap.range P.toLinearMap)ᗮ = LinearMap.ker P.toLinearMap := - (ContinuousLinearMap.IsIdempotentElem.isSymmetric_iff_orthogonal_range hP_idem).1 hP_symm + (LinearMap.IsIdempotentElem.isSymmetric_iff_orthogonal_range hP_idem.toLinearMap).1 hP_symm have h_range_closed : IsClosed (LinearMap.range P.toLinearMap : Set H) := (IsIdempotentElem.isClosed_range (p := P) hP_idem) -- Hence (ker P)ᗮ = range P @@ -242,7 +242,7 @@ lemma IsPartialIsometry.adjoint_mul_self_apply_of_mem_ker_orthogonal {U : H →L have hP_symm : (P : H →ₗ[ℂ] H).IsSymmetric := ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric.1 h_sa have h_orth : (LinearMap.range P.toLinearMap)ᗮ = LinearMap.ker P.toLinearMap := - (ContinuousLinearMap.IsIdempotentElem.isSymmetric_iff_orthogonal_range hP_idem).1 hP_symm + (LinearMap.IsIdempotentElem.isSymmetric_iff_orthogonal_range hP_idem.toLinearMap).1 hP_symm have h_range_closed : IsClosed (LinearMap.range P.toLinearMap : Set H) := IsIdempotentElem.isClosed_range hP_idem have h_eq_range : (LinearMap.ker P.toLinearMap)ᗮ = LinearMap.range P.toLinearMap := by diff --git a/QuantumSystem/ForMathlib/LinearAlgebra/Matrix/StarAlgEquiv.lean b/QuantumSystem/ForMathlib/LinearAlgebra/Matrix/StarAlgEquiv.lean index 7b1d54d..d7efa2e 100644 --- a/QuantumSystem/ForMathlib/LinearAlgebra/Matrix/StarAlgEquiv.lean +++ b/QuantumSystem/ForMathlib/LinearAlgebra/Matrix/StarAlgEquiv.lean @@ -1,6 +1,10 @@ module +public import Mathlib.Analysis.CStarAlgebra.CStarMatrix +public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital +public import Mathlib.Analysis.Matrix.HermitianFunctionalCalculus public import Mathlib.Analysis.Matrix.Order +public import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic /-! # `StarAlgEquiv` instances for matrix algebras @@ -115,19 +119,24 @@ theorem IsHermitian.map_starAlgEquiv {M : Matrix m m ℂ} (hM : M.IsHermitian) omit [DecidableEq m] [DecidableEq n] in /-- `*-`algebra equivalences preserve positive-semidefiniteness on matrix algebras over `ℂ`. -The proof goes via the existence of a positive-semidefinite square root: for PSD `M` we -have `M = (sqrt M)ᴴ * sqrt M`, applying `φ` gives `φ M = (φ (sqrt M))ᴴ * φ (sqrt M)`, -which is PSD by `posSemidef_conjTranspose_mul_self`. -/ +The proof goes via the eigenvalue characterisation of `PosSemidef`: any `*`-algebra equivalence +preserves the spectrum, and on Hermitian matrices the eigenvalues are exactly the real spectrum, +so non-negativity is preserved. -/ theorem PosSemidef.map_starAlgEquiv {M : Matrix m m ℂ} (hM : M.PosSemidef) (φ : Matrix m m ℂ ≃⋆ₐ[ℂ] Matrix n n ℂ) : (φ M).PosSemidef := by classical - have hM_nonneg : (0 : Matrix m m ℂ) ≤ M := hM.nonneg - have hsqrt_sa : IsSelfAdjoint (CFC.sqrt M) := IsSelfAdjoint.of_nonneg (CFC.sqrt_nonneg M) - have hM_eq : M = star (CFC.sqrt M) * CFC.sqrt M := by - rw [hsqrt_sa.star_eq, CFC.sqrt_mul_sqrt_self M hM_nonneg] - rw [hM_eq, map_mul, map_star, star_eq_conjTranspose] - exact posSemidef_conjTranspose_mul_self _ + -- Image is hermitian. + have hφM_herm : (φ M).IsHermitian := IsHermitian.map_starAlgEquiv hM.isHermitian φ + -- Reduce to spectrum-non-negativity using `posSemidef_iff_isHermitian_and_spectrum_nonneg`. + rw [posSemidef_iff_isHermitian_and_spectrum_nonneg] + refine ⟨hφM_herm, ?_⟩ + rw [posSemidef_iff_isHermitian_and_spectrum_nonneg] at hM + -- `*-`-algebra equivalences preserve the spectrum. + have hspec : spectrum ℂ (φ M) = spectrum ℂ M := + AlgEquiv.spectrum_eq φ.toAlgEquiv M + rw [hspec] + exact hM.2 omit [DecidableEq m] [DecidableEq n] in /-- `*-`algebra equivalences preserve positive-definiteness: PSD + invertibility, both of @@ -145,21 +154,25 @@ theorem PosDef.map_starAlgEquiv {M : Matrix m m ℂ} (hM : M.PosDef) `PosDef.map_starAlgEquiv`, useful when an index-set bijection `e : n ≃ m` is naturally available (e.g. from `LocalNet` region equivalences). -/ -omit [DecidableEq m] [DecidableEq n] in +omit [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] in /-- `Matrix.PosSemidef` is preserved by reindexing the index set via a bijection. Specialisation of `PosSemidef.map_starAlgEquiv` to `reindexStarAlgEquiv`. -/ -theorem PosSemidef.mapEquiv {M : Matrix m m ℂ} (hM : M.PosSemidef) (e : n ≃ m) : +theorem PosSemidef.mapEquiv [Finite m] {M : Matrix m m ℂ} (hM : M.PosSemidef) (e : n ≃ m) : (M.submatrix e e).PosSemidef := by classical + letI := Fintype.ofFinite m + letI : Fintype n := Fintype.ofEquiv m e.symm exact Matrix.PosSemidef.map_starAlgEquiv hM (Matrix.reindexStarAlgEquiv (R := ℂ) e.symm) -omit [DecidableEq m] [DecidableEq n] in +omit [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] in /-- `Matrix.PosDef` is preserved by reindexing the index set via a bijection. Specialisation of `PosDef.map_starAlgEquiv` to `reindexStarAlgEquiv`. -/ -theorem PosDef.mapEquiv {M : Matrix m m ℂ} (hM : M.PosDef) (e : n ≃ m) : +theorem PosDef.mapEquiv [Finite m] {M : Matrix m m ℂ} (hM : M.PosDef) (e : n ≃ m) : (M.submatrix e e).PosDef := by classical + letI := Fintype.ofFinite m + letI : Fintype n := Fintype.ofEquiv m e.symm exact Matrix.PosDef.map_starAlgEquiv hM (Matrix.reindexStarAlgEquiv (R := ℂ) e.symm) diff --git a/QuantumSystem/State.lean b/QuantumSystem/State.lean index cddf08e..5a34182 100644 --- a/QuantumSystem/State.lean +++ b/QuantumSystem/State.lean @@ -130,11 +130,24 @@ noncomputable def mix (ρ₁ ρ₂ : DensityMatrix n) (p : ℝ) (hp : 0 ≤ p) (hp1 : p ≤ 1) : DensityMatrix n where toMatrix := p • ↑ρ₁ + (1 - p) • ↑ρ₂ posSemidef := by - apply Matrix.PosSemidef.add - · exact ρ₁.posSemidef.smul (by exact_mod_cast hp) - · exact ρ₂.posSemidef.smul (by exact_mod_cast (sub_nonneg.mpr hp1)) + have hρ₁_smul : + p • (ρ₁.toMatrix : Matrix n n ℂ) = ((p : ℂ)) • (ρ₁.toMatrix : Matrix n n ℂ) := by + ext i j; simp [Matrix.smul_apply, Complex.real_smul] + have hρ₂_smul : + (1 - p) • (ρ₂.toMatrix : Matrix n n ℂ) = + ((1 - p : ℝ) : ℂ) • (ρ₂.toMatrix : Matrix n n ℂ) := by + ext i j; simp [Matrix.smul_apply, Complex.real_smul] + rw [hρ₁_smul, hρ₂_smul] + refine (Matrix.PosSemidef.smul ρ₁.posSemidef ?_).add + (Matrix.PosSemidef.smul ρ₂.posSemidef ?_) + · exact_mod_cast hp + · exact_mod_cast (sub_nonneg.mpr hp1) trace_eq_one := by - rw [Matrix.trace_add, Matrix.trace_smul, Matrix.trace_smul, + rw [Matrix.trace_add, + show (p • (ρ₁.toMatrix : Matrix n n ℂ)).trace = p • ρ₁.toMatrix.trace + from Matrix.trace_smul p ρ₁.toMatrix, + show ((1 - p) • (ρ₂.toMatrix : Matrix n n ℂ)).trace = (1 - p) • ρ₂.toMatrix.trace + from Matrix.trace_smul (1 - p) ρ₂.toMatrix, ρ₁.trace_eq_one, ρ₂.trace_eq_one, Algebra.smul_def, Algebra.smul_def, mul_one, mul_one] push_cast ring @@ -300,13 +313,12 @@ theorem regularize_eq_cfc (ρ : DensityMatrix n) {ε : ℝ} Algebra.algebraMap_eq_smul_one] rw [regularize_toMatrix, maximallyMixed_toMatrix, smul_smul] have h1 : (1 - (ε : ℂ)) • ρ.toMatrix = (1 - ε : ℝ) • ρ.toMatrix := by - rw [show (1 - (ε : ℂ)) = ((1 - ε : ℝ) : ℂ) from by push_cast; ring] - exact algebraMap_smul ℂ (1 - ε : ℝ) ρ.toMatrix + ext i j + simp [Matrix.smul_apply, Complex.real_smul] have h2 : ((ε : ℂ) * (Fintype.card n : ℂ)⁻¹) • (1 : Matrix n n ℂ) = (ε / (Fintype.card n : ℝ) : ℝ) • (1 : Matrix n n ℂ) := by - rw [show ((ε : ℂ) * (Fintype.card n : ℂ)⁻¹) = ((ε / (Fintype.card n : ℝ) : ℝ) : ℂ) from by - push_cast; rw [div_eq_mul_inv]] - exact algebraMap_smul ℂ (ε / Fintype.card n : ℝ) 1 + ext i j + simp [Matrix.smul_apply, Complex.real_smul, div_eq_mul_inv] rw [h1, h2] /-! ### Reindex compatibility