Source indexedlemma · leanprover/lean4:v4.32.0

step_three

APAP.Prereqs.MarcinkiewiczZygmund · APAP/Prereqs/MarcinkiewiczZygmund.lean:113 to 124

Mathematical statement

Exact Lean statement

lemma step_three (f : ι → ℝ) :
    ∑ ε ∈ ({-1, 1} : Finset ℝ)^^n,
      ∑ a ∈ A ^^ n, ∑ b ∈ A ^^ n, (∑ i, ε i * (f (a i) - f (b i))) ^ (2 * m) =
      ∑ a ∈ A ^^ n, ∑ b ∈ A ^^ n, ∑ k ∈ piAntidiag univ (2 * m),
          (multinomial univ k * ∏ t, (f (a t) - f (b t)) ^ k t) *
            ∑ ε ∈ ({-1, 1} : Finset ℝ)^^n, ∏ t, ε t ^ k t

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma step_three (f : ι → ℝ) :    ∑ ε ∈ ({-1, 1} : Finset ℝ)^^n,      ∑ a ∈ A ^^ n, ∑ b ∈ A ^^ n, (∑ i, ε i * (f (a i) - f (b i))) ^ (2 * m) =      ∑ a ∈ A ^^ n, ∑ b ∈ A ^^ n, ∑ k ∈ piAntidiag univ (2 * m),          (multinomial univ k * ∏ t, (f (a t) - f (b t)) ^ k t) *            ∑ ε ∈ ({-1, 1} : Finset ℝ)^^n, ∏ t, ε t ^ k t := by  simp only [@sum_comm _ _ (Fin n → ℝ) _ _ (A ^^ n), sum_pow_eq_sum_piAntidiag]  refine sum_congr rfl fun a _ ↦ ?_  refine sum_congr rfl fun b _ ↦ ?_  simp only [mul_pow, prod_mul_distrib, @sum_comm _ _ (Fin n → ℝ), ← mul_sum, ← sum_mul]  refine sum_congr rfl fun k _ ↦ ?_  rw [← mul_assoc, mul_right_comm]