partialFourierSumL2_norm

lemma partialFourierSumL2_norm {T : ℝ} [hT : Fact (0 < T)] [h2 : Fact (1 ≤ (2 : ENNReal))] {f : ↥(Lp ℂ 2 haarAddCircle)} {N : ℕ} :    ‖partialFourierSumLp 2 N f‖ ^ 2 = ∑ n ∈ Finset.Icc (-Int.ofNat N) N, ‖@fourierCoeff T hT _ _ _ f n‖ ^ 2 := by  calc ‖partialFourierSumLp 2 N f‖ ^ 2    _ = ‖partialFourierSumLp 2 N f‖ ^ (2 : ℝ) := by      rw [← Real.rpow_natCast]; rfl    _ = ‖fourierBasis.repr (partialFourierSumLp 2 N f)‖ ^ (2 : ℝ) := by      rw [fourierBasis.repr.norm_map (partialFourierSumLp 2 N f)]    _ = ‖∑ n ∈ Finset.Icc (-Int.ofNat N) N, fourierCoeff f n • (fourierBasis.repr (@fourierLp T hT 2 h2 n))‖ ^ (2 : ℝ) := by      rw [partialFourierSumLp, map_sum]      simp_rw [LinearMapClass.map_smul]    _ = ∑ n ∈ Finset.Icc (-Int.ofNat N) N, ‖fourierCoeff f n‖ ^ (2 : ℝ) := by      rw [← coe_fourierBasis]      simp_rw [← fourierBasis.repr_symm_single, LinearIsometryEquiv.apply_symm_apply, ← lp.single_smul]      have : 2 = (2 : ENNReal).toReal := by simp      rw [this, ← lp.norm_sum_single (by simp), ← this]      congr 2      refine Finset.sum_congr (by simp) fun n ↦ ?_      simp only [Int.ofNat_eq_natCast, Finset.mem_Icc, smul_eq_mul, mul_one, implies_true]    _ = ∑ n ∈ Finset.Icc (-Int.ofNat N) N, ‖fourierCoeff f n‖ ^ 2 := by      simp_rw [← Real.rpow_natCast]; rfl