Commit 2024-02-13 21:51 d13557bc
View on Github →feat: (a + b) ^ n ≤ 2 ^ (n - 1) * (a ^ n + b ^ n) (#9484)
Note that this inequality is trivial if the constant is 2 ^ n instead.
Due to the current import situation, I've had to downgrade the proof to not use gcongr, positivity, ring. This is currently hard to fix.
From LeanAPAP