cLpNorm_dft_indicator_one_pow

lemma cLpNorm_dft_indicator_one_pow [MeasurableSpace G] [DiscreteMeasurableSpace G] (n : ℕ)    (s : Finset G) : ‖dft 𝟭_[(s : Set G)]‖ₙ_[↑(2 * n)] ^ (2 * n) = boringEnergy n s := by  obtain rfl | hn := n.eq_zero_or_pos  · simp  refine Complex.ofReal_injective ?_  calc    _ = ⟪dft (𝟭_[(s : Set G)] ∗ᵈ^ n), dft (𝟭_[s] ∗ᵈ^ n)⟫ₙ_[ℂ] := ?_    _ = ⟪𝟭_[(s : Set G), ℂ] ∗ᵈ^ n, 𝟭_[s] ∗ᵈ^ n⟫_[ℂ] := wInner_cWeight_dft _ _    _ = _ := ?_  · rw [cLpNorm_pow_eq_expect_norm (by positivity)]    simp_rw [pow_mul', ← norm_pow _ n, Complex.ofReal_expect, Complex.ofReal_pow,      ← Complex.conj_mul', wInner_cWeight_eq_expect, inner_apply', dft_iterConv_apply]  · simp only [wInner_one_eq_sum, RCLike.inner_apply, boringEnergy_eq, Complex.ofReal_mul,      Complex.ofReal_sum, sq, Complex.ofReal_iterConv,      (((isSelfAdjoint_indicator_one _).iterConv _).apply _).conj_eq,      Complex.ofReal_comp_indicator_one]