OAI/Analysis/KadisonKastler/CommutantPolarSupport.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A support inequality for positive commutant contractions

This is the operator-order part of the bounded modular Radon--Nikodym argument. The sign of a self-adjoint test operator dominates its pairing with a positive contraction from the commutant.

  1. theorem OAI.KadisonKastler.commutant_positive_polar_support line 24