end_step

lemma end_step {f : ι → ℝ} (hm : 1 ≤ m) (hA : A.Nonempty) :    (∑ a ∈ A ^^ n, ∑ b ∈ A ^^ n, ∑ k ∈ piAntidiag univ m,      ↑(multinomial univ fun i ↦ 2 * k i) * ∏ t, (f (a t) - f (b t)) ^ (2 * k t)) / #A ^ n        ≤ (4 * m) ^ m * ∑ a ∈ A ^^ n, (∑ i, f (a i) ^ 2) ^ m := by  let B := A ^^ n  calc    (∑ a ∈ B, ∑ b ∈ B, ∑ k ∈ piAntidiag univ m,      (multinomial univ fun i ↦ 2 * k i : ℝ) * ∏ t, (f (a t) - f (b t)) ^ (2 * k t)) / #A ^ n    _ ≤ (∑ a ∈ B, ∑ b ∈ B, m ^ m * 2 ^ (m + (m - 1)) *          ((∑ i, f (a i) ^ 2) ^ m + (∑ i, f (b i) ^ 2) ^ m) : ℝ) / #A ^ n := by      gcongr; exact step_six.trans <| step_seven.trans step_eight    _ = _ := by      simp only [mul_add, sum_add_distrib, sum_const, nsmul_eq_mul, ← mul_sum]      rw [← mul_add, ← two_mul, ← mul_assoc 2, ← mul_assoc 2, mul_right_comm 2, ← _root_.pow_succ',        add_assoc, Nat.sub_add_cancel hm, pow_add, ← mul_pow, ← mul_pow, card_piFinset, prod_const,        Finset.card_univ, Fintype.card_fin, Nat.cast_pow, mul_div_cancel_left₀]      · norm_num        dsimp [B]      · positivity