Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

LiebBridge

Abstract

Consumed Hilbert-Schmidt perspective-to-Lieb trace bridge.

This module is a consumed supporting source transplant for the strictly positive, interior-exponent Lieb joint trace concavity endpoint. Its definitions and proof steps come from Kei Tsukamoto, Kento Mori and Hayata Yamasaki’s Apache-2.0 Physlib source at immutable revision b9043cc548ef6d63a28454cf3a57fb12a0c2e142. The Lean file records the exact original module and retained supplier license. No mathematical originality is claimed.

The consumed endpoint and its precise positive-definite and interior-exponent scope are described in the LiebConcavity blueprint. Retirement is triggered by an equivalent consumed declaration in this repository’s pinned Mathlib. This supporting module does not assert the singular PSD extension, closed exponent endpoints or trace-exponential consequence.

References