OAI/Analysis/Daugavet/ProductOperators.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactModuli.KW.arrayMultiplier line 16
2. lemma OAI.ExactModuli.KW.array_coordinate_mp line 18
3. lemma OAI.ExactModuli.KW.integrable_arrayMultiplier line 23
4. lemma OAI.ExactModuli.KW.integral_arrayMultiplier line 28
5. lemma OAI.ExactModuli.KW.measurable_arrayMultiplier line 34
6. lemma OAI.ExactModuli.KW.arrayMultiplier_tail line 38
7. def OAI.ExactModuli.KW.atomL1 line 44
8. lemma OAI.ExactModuli.KW.atomL1_ae line 50
9. lemma OAI.ExactModuli.KW.norm_atomL1 line 55
10. lemma OAI.ExactModuli.KW.atomL1_near_additive line 64
11. def OAI.ExactModuli.KW.matrixCombination line 87
12. def OAI.ExactModuli.KW.productOperator line 98
13. lemma OAI.ExactModuli.KW.productOperator_ae line 102
14. lemma OAI.ExactModuli.KW.productOperator_zero_coeff line 128