OAI/Analysis/Kaplansky/Regular/PowersOperators.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KaplanskyConsequences.Regular.mask_compl line 19
2. lemma OAI.KaplanskyConsequences.Regular.mask_left_conjugate line 25
3. lemma OAI.KaplanskyConsequences.Regular.sum_mask_norm_le line 32
4. lemma OAI.KaplanskyConsequences.Regular.norm_sum_mul_mask_le line 49
5. lemma OAI.KaplanskyConsequences.Regular.left_norm_le line 72
6. lemma OAI.KaplanskyConsequences.Regular.conjugate_norm_le line 77
7. lemma OAI.KaplanskyConsequences.Regular.powers_operator_estimate line 86