OAI/Analysis/Commutator/ScalarIndicator.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Kadison.Decomposable.indicator_measurable line 21
2. lemma OAI.Kadison.Decomposable.indicator_bound line 28
3. def OAI.Kadison.Decomposable.indicatorOperator line 38
4. lemma OAI.Kadison.Decomposable.indicatorOperator_ae line 42
5. lemma OAI.Kadison.Decomposable.indicatorOperator_norm_sq line 50
6. lemma OAI.Kadison.Decomposable.indicatorOperator_const line 61
7. theorem OAI.Kadison.Decomposable.local_constant_ae_bound line 73