OAI/Analysis/Daugavet/Multipliers.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactModuli.KW.scale line 11
2. def OAI.ExactModuli.KW.multiplier line 13
3. lemma OAI.ExactModuli.KW.scale_pos line 15
4. lemma OAI.ExactModuli.KW.scale_lt_one line 18
5. lemma OAI.ExactModuli.KW.multiplier_nonneg line 23
6. lemma OAI.ExactModuli.KW.measurable_multiplier line 26
7. lemma OAI.ExactModuli.KW.integrable_multiplier line 30
8. lemma OAI.ExactModuli.KW.integral_multiplier line 40
9. lemma OAI.ExactModuli.KW.multiplier_tail line 55
10. lemma OAI.ExactModuli.KW.multiplier_tail_le line 84
11. abbrev OAI.ExactModuli.KW.pairedMeasure line 92
12. def OAI.ExactModuli.KW.difference line 95
13. lemma OAI.ExactModuli.KW.measurable_difference line 98
14. lemma OAI.ExactModuli.KW.integrable_difference line 102
15. lemma OAI.ExactModuli.KW.difference_symmetric line 109
16. lemma OAI.ExactModuli.KW.difference_tail_upper line 118
17. lemma OAI.ExactModuli.KW.difference_tail_lower line 141