Real.marcinkiewicz_zygmund'

theorem marcinkiewicz_zygmund' (m : ℕ) (f : ι → ℝ) (hf : ∀ i, ∑ a ∈ A ^^ n, f (a i) = 0) :    ∑ a ∈ A ^^ n, (∑ i, f (a i)) ^ (2 * m) ≤      (4 * m) ^ m * ∑ a ∈ A ^^ n, (∑ i, f (a i) ^ 2) ^ m := by  obtain rfl | hm := m.eq_zero_or_pos  · simp  have hm' : 1 ≤ m := by rwa [Nat.succ_le_iff]  obtain rfl | hA := A.eq_empty_or_nonempty  · cases n <;> cases m <;> simp  let B := A ^^ n  calc    ∑ a ∈ B, (∑ i, f (a i)) ^ (2 * m)      ≤ ∑ a ∈ A ^^ n, (∑ b ∈ B, |∑ i, (f (a i) - f (b i))| ^ (2 * m)) / #A ^ n := by      gcongr; simpa [pow_mul, sq_abs] using step_one' hA f hf (2 * m) _    _ = (∑ a ∈ A ^^ n, ∑ b ∈ A ^^ n, ∑ k ∈ piAntidiag univ (2 * m) with ∀ i, 2 ∣ k i,        multinomial univ (fun i ↦ k i) * ∏ t, (f (a t) - f (b t)) ^ k t) / #A ^ n := by      rw [← sum_div]      simp only [pow_mul, sq_abs]      simp only [← pow_mul]      rw [step_two, step_three, mul_comm, inv_pow, ← div_eq_mul_inv, div_div]      simp only [step_four, mul_ite, mul_zero, mul_one, ← sum_filter, ← sum_mul, even_iff_two_dvd]      rw [mul_comm, mul_div_mul_left]      positivity    _ = (∑ a ∈ A ^^ n, ∑ b ∈ A ^^ n, ∑ k ∈ (piAntidiag univ m).map          ⟨(2 • ·), fun _ _ h ↦ funext fun i ↦ mul_right_injective₀ two_ne_zero (congr_fun h i)⟩,        multinomial univ (fun i ↦ k i) * ∏ t, (f (a t) - f (b t)) ^ k t) / #A ^ n := by      rw [map_nsmul_piAntidiag_univ m (ι := Fin n) (n := 2) two_ne_zero]    _ = (∑ 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 := by      simp    _ ≤ _ := end_step hm' hA