Strong subadditivity of von Neumann entropy

.devcontainer/Dockerfile

@@ -9,7 +9,7 @@ RUN SNIPPET="export PROMPT_COMMAND='history -a' && export HISTFILE=/commandhisto
     && echo "$SNIPPET" >> "/home/$USERNAME/.bashrc"
 
 RUN apt-get update && \
-    apt install -y ripgrep
+    apt install -y ripgrep libgl1 libglib2.0-0
 
 USER vscode
 WORKDIR /home/vscode

QuantumSystem.lean

@@ -9,19 +9,49 @@ public import QuantumSystem.Algebra.CStarAlgebra.PureState
 public import QuantumSystem.Algebra.CStarAlgebra.QuasiState
 public import QuantumSystem.Algebra.CStarAlgebra.State
 public import QuantumSystem.Algebra.CStarAlgebra.State.Continuity
+public import QuantumSystem.Algebra.CStarAlgebra.State.Faithful
+public import QuantumSystem.Algebra.LocalNet
 public import QuantumSystem.Algebra.Star.DoubleCommutant.SOTClosedSubAlgebra
 public import QuantumSystem.Algebra.Star.DoubleCommutant.WOTClosedSubAlgebra
-public import QuantumSystem.Algebra.VonNeumannAlgebra.Basic
+public import QuantumSystem.Analysis.CFC.Diagonal
+public import QuantumSystem.Analysis.Entropy.KroneckerProduct
+public import QuantumSystem.Analysis.Entropy.Regularize
+public import QuantumSystem.Analysis.Entropy.RelativeEntropy
+public import QuantumSystem.Analysis.Entropy.SSA
+public import QuantumSystem.Analysis.Entropy.VonNeumannEntropy
+public import QuantumSystem.Analysis.Matrix.Effros
+public import QuantumSystem.Analysis.Matrix.HermitianFunctionalCalculus
+public import QuantumSystem.Analysis.Matrix.LiebConcavity
+public import QuantumSystem.Analysis.Matrix.Order
+public import QuantumSystem.Analysis.Matrix.PartialTrace
+public import QuantumSystem.Analysis.Matrix.Pinching
+public import QuantumSystem.Analysis.Matrix.PosDef
+public import QuantumSystem.Channel
+public import QuantumSystem.ForMathlib.Analysis.Calculus.Deriv.Sign
 public import QuantumSystem.ForMathlib.Analysis.Complex.Basic
 public import QuantumSystem.ForMathlib.Analysis.CStarAlgebra.HilbertSpace
 public import QuantumSystem.ForMathlib.Analysis.CStarAlgebra.Ideal
 public import QuantumSystem.ForMathlib.Analysis.CStarAlgebra.NonUnital
 public import QuantumSystem.ForMathlib.Analysis.CStarAlgebra.Unital
 public import QuantumSystem.ForMathlib.Analysis.CStarAlgebra.WeakDual
+public import QuantumSystem.ForMathlib.Analysis.InnerProductSpace.Adjoint
 public import QuantumSystem.ForMathlib.Analysis.InnerProductSpace.DiagonalAmplification
 public import QuantumSystem.ForMathlib.Analysis.InnerProductSpace.InvariantSubspace
+public import QuantumSystem.ForMathlib.Analysis.InnerProductSpace.l2Space
+public import QuantumSystem.ForMathlib.Analysis.InnerProductSpace.TensorProduct
 public import QuantumSystem.ForMathlib.Analysis.LocallyConvex.StrongOperatorTopology
 public import QuantumSystem.ForMathlib.Analysis.LocallyConvex.WeakOperatorTopology
+public import QuantumSystem.ForMathlib.Analysis.Matrix.Basic
+public import QuantumSystem.ForMathlib.Analysis.Matrix.Hermitian
+public import QuantumSystem.ForMathlib.Analysis.Matrix.Order
+public import QuantumSystem.ForMathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
+public import QuantumSystem.ForMathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PartialIsometry
+public import QuantumSystem.ForMathlib.Analysis.SpecialFunctions.Pow.Real
+public import QuantumSystem.ForMathlib.InformationTheory.KullbackLeibler.KLFun
+public import QuantumSystem.ForMathlib.LinearAlgebra.Matrix.StarAlgEquiv
 public import QuantumSystem.ForMathlib.LinearAlgebra.Span.Def
+public import QuantumSystem.ForMathlib.RingTheory.RootsOfUnity.Complex
 public import QuantumSystem.ForMathlib.Topology.DenseLinear
 public import QuantumSystem.ForMathlib.Topology.MetricSpace.Completion
+public import QuantumSystem.Notation
+public import QuantumSystem.State

QuantumSystem/Algebra/CStarAlgebra/GNS/Construction.lean

@@ -5,6 +5,7 @@ public import Mathlib.Analysis.Normed.Operator.Extend
 public import QuantumSystem.ForMathlib.Analysis.CStarAlgebra.HilbertSpace
 public import QuantumSystem.ForMathlib.Analysis.CStarAlgebra.Ideal
 public import QuantumSystem.Algebra.CStarAlgebra.State.Continuity
+public import QuantumSystem.Algebra.CStarAlgebra.State.Faithful
 
 @[expose] public section
 
@@ -765,6 +766,84 @@ lemma approxUnit_eval_tendsto_one :
   rw [inner_self_eq_norm_sq_to_K (𝕜 := ℂ), h_norm]
   norm_num
 
+/-- If ω is faithful, then the GNS kernel Nω is trivial. -/
+lemma IsFaithful.kernel_eq_bot (hω : ω.IsFaithful) : (Nω).carrier = {0} := by
+  ext a
+  simp only [Set.mem_singleton_iff]
+  constructor
+  · intro ha
+    exact hω a ha
+  · intro ha
+    simp [ha]
+
+/-- The GNS cyclic vector ξω is nonzero (has norm 1).
+
+Note: This is a basic property of the GNS construction, not the main theorem about
+faithful states and separating vectors. -/
+lemma ξω_ne_zero : ξω ω ≠ 0 := by
+  have h := ξω_norm (ω := ω)
+  intro h0
+  rw [h0, norm_zero] at h
+  exact one_ne_zero h.symm
+
+/-- If ω is faithful, then πω(a) ξω = 0 implies a = 0 (and hence πω(a) = 0).
+
+This is the key separating property: the cyclic vector ξω separates elements of A
+via the GNS representation when ω is faithful. -/
+lemma IsFaithful.ξω_separating (hω : ω.IsFaithful) (a : A) (h : πω ω a (ξω ω) = 0) : a = 0 := by
+  rw [πω_cyclic_identity] at h
+  -- h : ↑(Quotient.mk'' a : A ⧸ Nω ω) = 0 in Hω
+  have h_inj := UniformSpace.Completion.coe_injective (α := A ⧸ Nω)
+  have h0 : (↑(Quotient.mk'' 0 : A ⧸ Nω) : Hω) = 0 :=
+    UniformSpace.Completion.coe_zero (α := A ⧸ Nω)
+  have h_quot_zero : (Quotient.mk'' a : A ⧸ Nω) = Quotient.mk'' 0 := h_inj (h.trans h0.symm)
+  -- From quotient being zero, a ∈ Nω
+  have h_eq := Quotient.exact' h_quot_zero
+  rw [CStarAlgebraIdeal.leftRel, QuotientAddGroup.leftRel_apply] at h_eq
+  have h_neg_in : -a ∈ (Nω).toAddSubgroup := by simpa using h_eq
+  have h_neg_neg : - -a ∈ (Nω).carrier := (Nω).neg_mem' h_neg_in
+  have h_in_kernel : a ∈ (Nω).carrier := by simp only [neg_neg] at h_neg_neg; exact h_neg_neg
+  -- Apply faithfulness: Nω = {0}
+  rw [IsFaithful.kernel_eq_bot (ω := ω) hω, Set.mem_singleton_iff] at h_in_kernel
+  exact h_in_kernel
+
+/-- The fundamental equivalence: ω is faithful if and only if the map a ↦ πω(a) ξω
+is injective from A to Hω.
+
+This connects faithfulness (an algebraic property of the state) with the separating
+property (a geometric property of the cyclic vector). -/
+theorem isFaithful_iff_separating :
+    ω.IsFaithful ↔ Function.Injective (fun a : A => πω ω a (ξω ω)) := by
+  constructor
+  · intro hω a b hab
+    have h : πω ω (a - b) (ξω ω) = 0 := by
+      simp only [πω_sub, ContinuousLinearMap.sub_apply, hab, sub_self]
+    exact sub_eq_zero.mp (IsFaithful.ξω_separating (ω := ω) hω (a - b) h)
+  · intro h_inj a ha
+    -- ha : ω(a*a) = 0, i.e., a ∈ Nω
+    -- Need to show a = 0
+    have h_cyclic : πω ω a (ξω ω) = 0 := by
+      rw [πω_cyclic_identity]
+      have h_quot : (Quotient.mk'' a : A ⧸ Nω) = Quotient.mk'' 0 := by
+        apply Quotient.sound'
+        rw [CStarAlgebraIdeal.leftRel, QuotientAddGroup.leftRel_apply]
+        simpa using (Nω).neg_mem' ha
+      rw [h_quot]
+      exact UniformSpace.Completion.coe_zero (α := A ⧸ Nω)
+    have h0 : πω ω 0 (ξω ω) = 0 := by rw [πω_zero]; simp
+    exact h_inj (h_cyclic.trans h0.symm)
+
+/-- The GNS representation πω is injective when ω is faithful.
+
+This is a corollary of the fundamental equivalence `isFaithful_iff_separating`:
+the cyclic vector ξω separates elements via the representation, which implies
+that the representation itself is injective. -/
+lemma IsFaithful.injective_πω (hω : ω.IsFaithful) : Function.Injective (πω ω) := by
+  intro a b hab
+  have h_sep := (isFaithful_iff_separating (ω := ω)).mp hω
+  apply h_sep
+  simp only [hab]
+
 end Construction
 
 end GNS

QuantumSystem/Algebra/CStarAlgebra/State/Faithful.lean

@@ -0,0 +1,45 @@
+module
+
+public import QuantumSystem.Algebra.CStarAlgebra.State
+
+@[expose] public section
+
+namespace State
+
+variable {𝕜 : Type*} [RCLike 𝕜]
+variable {A : Type*} [NonUnitalCStarAlgebra A] [Module 𝕜 A]
+
+/-- A state ω on a C*-algebra A is faithful if ω(a*a) = 0 implies a = 0.
+
+This is equivalent to saying the GNS kernel Nω is trivial, i.e., the GNS representation
+is injective. -/
+def IsFaithful (ω : State 𝕜 A) : Prop :=
+  ∀ a : A, ω (star a * a) = 0 → a = 0
+
+/-- Alternative characterization: a state is faithful iff a*a is not in the kernel
+unless a = 0. -/
+lemma isFaithful_iff (ω : State 𝕜 A) :
+    ω.IsFaithful ↔ ∀ a : A, a ≠ 0 → ω (star a * a) ≠ 0 := by
+  constructor
+  · intro hf a ha h0
+    exact ha (hf a h0)
+  · intro h a h0
+    by_contra ha
+    exact h a ha h0
+
+/-- Faithful states are positive definite on positive elements. -/
+lemma IsFaithful.pos_of_nonzero {ω : State ℂ A} (hω : ω.IsFaithful) {a : A} (ha : a ≠ 0) :
+    0 < (ω (star a * a)).re := by
+  obtain ⟨r, hr⟩ := ω.positive a
+  have hr' : ω (star a * a) = (r : ℂ) := by
+    simpa [State.toLinearMap_apply] using hr
+  rw [hr']
+  simp only [Complex.ofReal_re]
+  by_contra h_not_pos
+  push_neg 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
+  exact ha (hω a h0)
+
+end State