pow_inner_nonneg'

lemma pow_inner_nonneg' {f : G → ℂ} (hf : g ○ᵈ g = f) (hν : h ○ᵈ h = (↑) ∘ ν) (k : ℕ) :    0 ≤ ⟪f ^ k, (↑) ∘ ν⟫_[ℂ] := by  calc    0 ≤ ∑ z : Fin k → G, (‖∑ x, (∏ i, conj (g (x + z i))) * h x‖ : ℂ) ^ 2 := by positivity    _ = ∑ x : G, ∑ yz : G × G with yz.1 - yz.2 = x,          h yz.1 * conj h yz.2 * conj ((g ○ᵈ g) (yz.1 - yz.2)) ^ k := ?_    _ = ∑ x : G, ∑ yz : G × G with yz.1 - yz.2 = x,          h yz.1 * conj h yz.2 * conj ((g ○ᵈ g) x) ^ k := by        congr! with x _ yz hyz        simpa using hyz    _ = _ := by      rw [← hf, ← hν, wInner_one_eq_sum]      simp only [Pi.pow_apply, RCLike.inner_apply, map_pow]      simp_rw [dddconv_apply h, sum_mul]  simp_rw [dddconv_apply_sub, sum_fiberwise, ← univ_product_univ, sum_product]  simp only [sum_pow', sum_mul_sum, map_mul, starRingEnd_self_apply, Fintype.piFinset_univ,    ← Complex.conj_mul', map_sum, map_prod]  simp only [mul_sum, @sum_comm _ _ (Fin k → G), mul_comm (conj _), prod_mul_distrib, Pi.conj_apply]  rw [sum_comm]  congr with x  congr with y  congr with z  group