Commit 2020-10-12 14:57 38e9ed32

feat(archive/imo): IMO 2020 Q2 (#4565) Add a proof of IMO 2020 Q2 (directly following one of the official solutions; there are many very similar approaches possible). In support of this solution, add geom_mean_le_arith_mean4_weighted to analysis.mean_inequalities, for both real and nnreal, analogous to the versions for two and three numbers (and also add geom_mean_le_arith_mean3_weighted for real as it was only present for nnreal).