OAI/Analysis/Daugavet/SignAverages.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactModuli.KW.signSum line 16
2. def OAI.ExactModuli.KW.signAverage line 19
3. lemma OAI.ExactModuli.KW.norm_le_signAverage line 23
4. lemma OAI.ExactModuli.KW.signSum_identDistrib line 64
5. lemma OAI.ExactModuli.KW.expected_max_le_expected_abs_sum line 80
6. lemma OAI.ExactModuli.KW.one_sub_exp_neg_ge_half line 105
7. lemma OAI.ExactModuli.KW.independent_max_tail_lower line 116
8. lemma OAI.ExactModuli.KW.integrable_real_tail line 159
9. lemma OAI.ExactModuli.KW.expectation_lower_from_power_tail line 171