Source indexedlemma · leanprover/lean4:v4.32.0

step_two

APAP.Prereqs.MarcinkiewiczZygmund · APAP/Prereqs/MarcinkiewiczZygmund.lean:99 to 111

Mathematical statement

Exact Lean statement

lemma step_two (f : ι → ℝ) :
    ∑ a ∈ A ^^ n, ∑ b ∈ A ^^ n, (∑ i, (f (a i) - f (b i))) ^ (2 * m) =
      2⁻¹ ^ n * ∑ ε ∈ ({-1, 1} : Finset ℝ)^^n,
        ∑ a ∈ A ^^ n, ∑ b ∈ A ^^ n, (∑ i, ε i * (f (a i) - f (b i))) ^ (2 * m)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma step_two (f : ι → ℝ) :    ∑ a ∈ A ^^ n, ∑ b ∈ A ^^ n, (∑ i, (f (a i) - f (b i))) ^ (2 * m) =      2⁻¹ ^ n * ∑ ε ∈ ({-1, 1} : Finset ℝ)^^n,        ∑ a ∈ A ^^ n, ∑ b ∈ A ^^ n, (∑ i, ε i * (f (a i) - f (b i))) ^ (2 * m) := by  let B := A ^^ n  have : ∀ ε ∈ ({-1, 1} : Finset ℝ)^^n,    ∑ a ∈ B, ∑ b ∈ B, (∑ i, ε i * (f (a i) - f (b i))) ^ (2 * m) =      ∑ a ∈ B, ∑ b ∈ B, (∑ i, (f (a i) - f (b i))) ^ (2 * m) :=    fun ε hε ↦ step_two_aux A f _ hε fun z : Fin n → ℝ ↦ univ.sum z ^ (2 * m)  rw [Finset.sum_congr rfl this, sum_const, card_piFinset_const, card_pair, nsmul_eq_mul,    Nat.cast_pow, Nat.cast_two, inv_pow, inv_mul_cancel_left₀]  · positivity  · norm_num