RCLike.marcinkiewicz_zygmund

lemma marcinkiewicz_zygmund (hm : m ≠ 0) (f : ι → 𝕜) (hf : ∀ i, ∑ a ∈ A ^^ n, f (a i) = 0) :    ∑ a ∈ A ^^ n, ‖∑ i, f (a i)‖ ^ (2 * m) ≤      (8 * m) ^ m * n ^ (m - 1) * ∑ a ∈ A ^^ n, ∑ i, ‖f (a i)‖ ^ (2 * m) := by  let f₁ x : ℝ := re (f x)  let f₂ x : ℝ := im (f x)  let B := A ^^ n  have hf₁ i : ∑ a ∈ B, f₁ (a i) = 0 := by rw [← map_sum, hf, map_zero]  have hf₂ i : ∑ a ∈ B, f₂ (a i) = 0 := by rw [← map_sum, hf, map_zero]  have h₁ := Real.marcinkiewicz_zygmund hm _ hf₁  have h₂ := Real.marcinkiewicz_zygmund hm _ hf₂  simp only [pow_mul, RCLike.norm_sq_eq_def]  simp only [← sq, map_sum, map_sum]  calc    ∑ a ∈ B, ((∑ i, re (f (a i))) ^ 2 + (∑ i, im (f (a i))) ^ 2) ^ m ≤        ∑ a ∈ B,          2 ^ (m - 1) * (((∑ i, re (f (a i))) ^ 2) ^ m + ((∑ i, im (f (a i))) ^ 2) ^ m) := by      gcongr with a; apply add_pow_le <;> positivity    _ = 2 ^ (m - 1) * (∑ a ∈ B, (∑ i, re (f (a i))) ^ (2 * m) +          ∑ a ∈ B, (∑ i, im (f (a i))) ^ (2 * m)) := by      simp only [← sum_add_distrib, mul_sum, pow_mul]    _ ≤ 2 ^ (m - 1) * ((4 * m) ^ m * n ^ (m - 1) *          ∑ a ∈ B, ∑ i, re (f (a i)) ^ (2 * m) + (4 * m) ^ m * n ^ (m - 1) *          ∑ a ∈ B, ∑ i, im (f (a i)) ^ (2 * m)) := by gcongr    _ = 2 ^ (m - 1) * ((4 * m) ^ m * n ^ (m - 1) *          ∑ a ∈ B, ∑ i, (re (f (a i)) ^ (2 * m) + im (f (a i)) ^ (2 * m))) := by      simp_rw [sum_add_distrib, mul_add]    _ ≤ 2 ^ (m - 1) * ((4 * m) ^ m * n ^ (m - 1) *          ∑ a ∈ B, ∑ i, 2 * (re (f (a i)) ^ 2 + im (f (a i)) ^ 2) ^ m) := by      simp_rw [pow_mul]; gcongr; apply pow_add_pow_le' <;> positivity    _ = (8 * m) ^ m * n ^ (m - 1) * ∑ a ∈ B, ∑ i, (re (f (a i)) ^ 2 + im (f (a i)) ^ 2) ^ m := by      simp_rw [← mul_sum, show (8 : ℝ) = 2 * 4 by norm_num, mul_pow, ← pow_sub_one_mul hm (2 : ℝ)]      ring