step_one

lemma step_one (hA : A.Nonempty) (f : ι → ℝ) (a : Fin n → ι)    (hf : ∀ i, ∑ a ∈ A ^^ n, f (a i) = 0) :    |∑ i, f (a i)| ^ (m + 1) ≤      (∑ b ∈ A ^^ n, |∑ i, (f (a i) - f (b i))| ^ (m + 1)) / #A ^ n := by  let B := A ^^ n  calc    |∑ i, f (a i)| ^ (m + 1)      = |∑ i, (f (a i) - (∑ b ∈ B, f (b i)) / #B)| ^ (m + 1) := by      simp only [B, hf, sub_zero, zero_div]    _ = |(∑ b ∈ B, ∑ i, (f (a i) - f (b i))) / #B| ^ (m + 1) := by      simp only [sum_sub_distrib]      rw [sum_const, sub_div, sum_comm, sum_div, nsmul_eq_mul, card_piFinset, prod_const,        Finset.card_univ, Fintype.card_fin, Nat.cast_pow, mul_div_cancel_left₀]      positivity    _ = |∑ b ∈ B, ∑ i, (f (a i) - f (b i))| ^ (m + 1) / #B ^ (m + 1) := by      rw [abs_div, div_pow, Nat.abs_cast]    _ ≤ (∑ b ∈ B, |∑ i, (f (a i) - f (b i))|) ^ (m + 1) / #B ^ (m + 1) := by      gcongr; exact IsAbsoluteValue.abv_sum _ _ _    _ = (∑ b ∈ B, |∑ i, (f (a i) - f (b i))|) ^ (m + 1) / #B ^ m / #B := by      rw [div_div, ← _root_.pow_succ]    _ ≤ (∑ b ∈ B, |∑ i, (f (a i) - f (b i))| ^ (m + 1)) / #B := by      gcongr; exact pow_sum_div_card_le_sum_pow (fun _ _ ↦ abs_nonneg _) _    _ = _ := by simp [B]