OAI/Analysis/KadisonKastler/ExtremeHermitianSplit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A norm-budgeted splitting of an extreme Hermitian annihilator

The compression argument splits an extreme functional into two Hermitian annihilators with complementary norm bounds. Extremality determines each summand from that norm budget.

  1. theorem OAI.KadisonKastler.scaled_hermitian_mem_annihilator_ball line 18
  2. theorem OAI.KadisonKastler.extreme_hermitian_split line 36