feat: finish part 1 of Lemma 3.23

[fpvandoorn]

• There are some preliminary lemmas about independent variables in ForMathlib/Independence. Maybe these lemmas already exist, but I couldn't find them
• It was incredibly painful to instantiate lemma independent_copies' to the case with 3 explicit random variables. I did this only if the variables have the same codomain, otherwise it would be even more painful.
• I only proved condDist_diff_le for Ω and Ω' in the same universe level. We could remove this constraint, but I don't think it will cause many problems (except that we maybe have to write some universe levels explicitly)
• For condDist_diff_le' I needed H[Y + Z; μ'] = H[Y - Z; μ'], so I assumed ElementaryAddCommGroup G 2. We should probably mention in the blueprint that this lemma only holds for elementary 2-groups? Maybe by choosing signs more carefully we get the result also without that condition.
• Also rename/reformulate some lemmas in f2_vec