Strong subadditivity of von Neumann entropy - #14

Merged

kencyke merged 35 commits into

mainfrom

6-von-neumann-entropy

Apr 30, 2026

Commits on Apr 23, 2026

docs(DoubleCommutant): use unicode ⇒ in WOTClosedSubAlgebra docstring
kencyke
committed
b981f09
feat(ForMathlib): add analysis matrix, inner-product, and calculus helpers
kencyke
committed
c8e904f
feat(ForMathlib): add CFC abs / partial isometry and real-power lemma
kencyke
committed
0cee909
feat(ForMathlib/Complex): add phase-alignment exp/arg helpers
kencyke
committed
cf911f5
feat(ForMathlib): add classical KL function and complex roots of unity
kencyke
committed
ec6d13d
feat: add top-level quantum-info notation and state abbreviation
kencyke
committed
3526f3b
feat(CStarAlgebra): faithful states and GNS separating property
kencyke
committed
b37c657
feat(Linear/Unbounded): add densely-defined maps, adjoint, antilinear, closable
kencyke
committed
e42e4fb
feat(Analysis/Matrix): add Effros, Hermitian CFC, Lieb, pinching utilities
kencyke
committed
5fd77f0
feat(Analysis/CFC): add compact, polar decomposition, trace-class CFC
kencyke
committed
c8737a2
feat(Analysis/Entropy): add von Neumann, relative, trace-class entropies
kencyke
committed
36bd982
feat(Channel): add quantum channels and trace-class conditional expectation
kencyke
committed
0b1b039
feat(VonNeumannAlgebra): add normal state, separating vector, Tomita, Segal entropy
kencyke
committed
14309ac
feat(VonNeumannAlgebra): add variational Araki relative entropy and monotonicity
kencyke
committed
cde2096
chore: re-export new modules from QuantumSystem aggregate
kencyke
committed
e837e32
feat(ForMathlib): operator tensor product for finite-dim Hilbert spaces
kencyke
committed
3a538a2
refactor(ArakiRelativeEntropy): drop unused import and universe var
kencyke
committed
f62ac65

Commits on Apr 29, 2026

chore: remove for now
kencyke
committed
86ea6c2

Commits on Apr 30, 2026

chore: add deps for MinerU
kencyke
committed
cbaa328
refactor(ForMathlib/InnerProductSpace): hide tensor-of-CLM helpers

kencyke
and
claude
committed
d164f48
feat(ForMathlib/Complex): add ComplexOrder lifting helpers for ℝ-valued

kencyke
and
claude
committed
aec0767
feat(ForMathlib/Matrix): reindex StarAlgEquiv with trace and positivity preservation

kencyke
and
claude
committed
30f7058
feat(Matrix): add matrix-log spectral form and StarAlgEquiv compatibility

kencyke
and
claude
committed
34652a6
feat(Matrix/CFC/Diagonal): add cfc Real.log on strictly-positive diagonal matrices

kencyke
and
claude
committed
eebbe1e
feat(State): add density-matrix transport, maximally-mixed state and regularization

kencyke
and
claude
committed
39e920c
feat(Algebra/LocalNet): add local algebras and region-index combinators

kencyke
and
claude
committed
eeadd54
feat(Matrix/PartialTrace): add region restriction (partial trace) and ρ ↾ Λ notation

kencyke
and
claude
committed
3299679
feat(Entropy/VonNeumann): add spectral form, isomorphism invariance and regularization continuity

kencyke
and
claude
committed
1ff13e9
feat(Entropy/Relative): add isomorphism invariance under trace-preserving StarAlgEquiv

kencyke
and
claude
committed
2989e8f
feat(Entropy/Kronecker): add bipartite Kronecker calculus and log-tensor identity

kencyke
and
claude
committed
5ed159a
feat(Entropy/Regularize): make regularization commute with restriction on a LocalNet

kencyke
and
claude
committed
8e2d53c
feat(Entropy/SSA): add strong subadditivity in common-region-explicit form

kencyke
and
claude
committed
23fdfdf
chore: refresh aggregate root and notation table

kencyke
and
claude
committed
01ee118
chore: remove low-quality codes
kencyke
committed
0cea660
docs: update README
kencyke
committed
b13e99c