Loewner order

What 'bigger' means for operators -- and the strange discovery that taking squares breaks it while taking square roots does not.

standard mathematics · standard mathematics, cited outward

In plain terms

Here is the problem. Quantum information runs on inequalities -- this entropy is at most that one, this channel loses at least this much -- but the objects being compared are operators, not numbers. What does A is at most B even mean for matrices?

The Loewner order answers: A is at most B when their difference B minus A is positive semidefinite -- when it never produces a negative number from any state. Some pairs are simply incomparable; it is a partial order, and that is fine.

The genuine surprise is which functions respect it. Send A and B, with A below B, through the square-root function: order preserved. Through the SQUARE: order can flip. Intuition trained on numbers fails at the second example, and half the classic blunders in operator inequalities are exactly this failure.

In CSD

The corpus's entropy and channel results are statements IN this order -- data processing, subadditivity, trace-distance contraction all compare operators. So are the operator-convexity results that support them.

The machinery is imported, not claimed; what the corpus adds is formal verification, which for this topic has unusual value. Because naive number-intuition fails silently here, this is exactly the terrain where an informal proof can be confidently wrong -- and where machine-checking pays for itself.

Mathematically

A at most B iff B minus A is positive semidefinite. Operator monotone functions -- those respecting the order under the functional calculus -- are characterised by Loewner's theorem: precisely the functions analytically continuing to map the upper half-plane to itself. Square root and logarithm qualify; the square does not. The corpus consumes the order throughout its entropy and channel chains.

The name

Charles Loewner (1893-1968), born Karel Lowner near Prague, studied under Georg Pick at the German university there. His 1923 attack on the Bieberbach conjecture introduced an evolution equation that waited eighty years to become spectacularly famous -- as the Loewner in Schramm-Loewner evolution, now central to two-dimensional statistical physics.

The operator-monotone characterisation is from 1934. Five years later the Nazi occupation forced him out of Prague; he restarted in America almost from zero -- Louisville, Syracuse, finally Stanford from 1951, where he taught to the end. Two results, each a half-century ahead of its audience, from a man who had to rebuild his life in the middle.

Background
Overview and history
Referenced
Wikipedia

Source links are pinned to a commit, so they do not drift. The anchors above are checked mechanically against the Lean tree on every build. The mathematics is not, and cannot be: that is a human responsibility and it rests with the author.

Part of Constraint-Surface Dynamics · Formalised in csd-lean4.

Privacy policy