OAI/Analysis/Commutator/AtomicShift.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.AtomicFactor.Decomposition.finiteShift line 22
2. lemma OAI.Kadison.AtomicFactor.Decomposition.finiteShift_star_mul line 25
3. lemma OAI.Kadison.AtomicFactor.Decomposition.finiteShift_norm_le line 42
4. lemma OAI.Kadison.AtomicFactor.Decomposition.finiteShift_mul_val line 48
5. theorem OAI.Kadison.AtomicFactor.Decomposition.exists_shift line 55
6. lemma OAI.Kadison.AtomicFactor.Decomposition.shift_isometry line 75
7. lemma OAI.Kadison.AtomicFactor.Decomposition.shifts_orthogonal line 89