big_shifts_step2

lemma big_shifts_step2 (L : Finset (Fin k → G)) (hk : k ≠ 0) :    (∑ x ∈ L + S.piDiag (Fin k), ∑ l ∈ L, ∑ s ∈ S.piDiag (Fin k), ite (l + s = x) (1 : ℝ) 0) ^ 2      ≤ #(L + S.piDiag (Fin k)) * #S *        ∑ l₁ ∈ L, ∑ l₂ ∈ L, ite (l₁ - l₂ ∈ univ.piDiag (Fin k)) 1 0 := by  refine sq_sum_le_card_mul_sum_sq.trans ?_  simp_rw [sq, sum_mul, @sum_comm _ _ _ _ (L + S.piDiag (Fin k)), boole_mul, sum_ite_eq, mul_assoc]  refine mul_le_mul_of_nonneg_left ?_ (Nat.cast_nonneg _)  have : ∀ f : (Fin k → G) → (Fin k → G) → ℝ,    ∑ x ∈ L, ∑ y ∈ S.piDiag (Fin k), (if x + y ∈ L + S.piDiag (Fin k) then f x y else 0) =      ∑ x ∈ L, ∑ y ∈ S.piDiag (Fin k), f x y := by    refine fun f ↦ sum_congr rfl fun x hx ↦ ?_    exact sum_congr rfl fun y hy ↦ if_pos <| add_mem_add hx hy  rw [this]  have (x y : Fin k → G) :      ∑ s₁ ∈ S.piDiag (Fin k), ∑ s₂ ∈ S.piDiag (Fin k), ite (y + s₂ = x + s₁) (1 : ℝ) 0 =        ite (x - y ∈ univ.piDiag (Fin k)) 1 0 *          ∑ s₁ ∈ S.piDiag (Fin k), ∑ s₂ ∈ S.piDiag (Fin k), ite (s₂ = x + s₁ - y) 1 0 := by    simp_rw [mul_sum, boole_mul, ← ite_and]    refine sum_congr rfl fun s₁ hs₁ ↦ ?_    refine sum_congr rfl fun s₂ hs₂ ↦ ?_    refine if_congr ?_ rfl rfl    rw [eq_sub_iff_add_eq', and_iff_right_of_imp]    intro h    simp only [mem_piDiag] at hs₁ hs₂    have : x - y = s₂ - s₁ := by rw [sub_eq_sub_iff_add_eq_add, ← h, add_comm]    rw [this]    obtain ⟨i, -, rfl⟩ := hs₁    obtain ⟨j, -, rfl⟩ := hs₂    exact mem_image.2 ⟨j - i, mem_univ _, rfl⟩  simp_rw [@sum_comm _ _ _ _ (S.piDiag (Fin k)) L, this, sum_ite_eq']  have : ∑ x ∈ L, ∑ y ∈ L,        ite (x - y ∈ univ.piDiag (Fin k)) (1 : ℝ) 0 *          ∑ z ∈ S.piDiag (Fin k), ite (x + z - y ∈ S.piDiag (Fin k)) 1 0 ≤      ∑ x ∈ L, ∑ y ∈ L, ite (x - y ∈ univ.piDiag (Fin k)) 1 0 * (#S : ℝ) := by    refine sum_le_sum fun l₁ _ ↦ sum_le_sum fun l₂ _ ↦ ?_    refine mul_le_mul_of_nonneg_left ?_ (by split_ifs <;> norm_num)    refine (sum_le_card_nsmul _ _ 1 ?_).trans_eq ?_    · intro x _; split_ifs <;> norm_num    have := Fin.pos_iff_nonempty.1 (pos_iff_ne_zero.2 hk)    rw [card_piDiag]    simp only [nsmul_one]  refine this.trans ?_  simp_rw [← sum_mul, mul_comm]  rfl