OAI/Analysis/Commutator/PartialWordContinuity.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Kadison.FinitePatching.PartialUnitary.support_norm_sub line 24
2. lemma OAI.Kadison.FinitePatching.PartialUnitary.power_norm_sub line 35
3. def OAI.Kadison.FinitePatching.Words.slotCost line 59
4. def OAI.Kadison.FinitePatching.Words.wordCost line 64
5. lemma OAI.Kadison.FinitePatching.Words.slotPower_norm_sub line 67
6. lemma OAI.Kadison.FinitePatching.Words.letter_norm_sub line 79
7. lemma OAI.Kadison.FinitePatching.Words.word_norm_sub line 88
8. lemma OAI.Kadison.FinitePatching.Words.trace_word_norm_sub line 105
9. lemma OAI.Kadison.FinitePatching.Words.momentBound_limit line 113