OAI/Analysis/Commutator/InfiniteBoundTransfer.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.InfiniteAmplification.single0 line 27
2. lemma OAI.Kadison.InfiniteAmplification.single0_adjoint line 34
3. lemma OAI.Kadison.InfiniteAmplification.single0_intertwines line 42
4. lemma OAI.Kadison.InfiniteAmplification.pullback_map line 48
5. lemma OAI.Kadison.InfiniteAmplification.seminorm_map_le line 55
6. theorem OAI.Kadison.InfiniteAmplification.bound_of_stable_bound line 68