expect_iInf_ker_eq_expect_ite

lemma expect_iInf_ker_eq_expect_ite {Δ : Set (AddChar G ℂ)}    [DecidablePred (· ∈ AddSubgroup.closure Δ)] {V : AddSubgroup G} [Fintype V]    (hV : V = ⨅ γ ∈ Δ, γ.toAddMonoidHom.ker) (f : G → ℂ) :    𝔼 x ∈ Set.toFinset V, f x = 𝔼 ψ, if ψ ∈ AddSubgroup.closure Δ then dft f ψ else 0 := by  rw [show (𝔼 x ∈ Set.toFinset V, f x) = 𝔼 x ∈ Set.toFinset V, 𝔼 ψ, dft f ψ * ψ x by    congr! with x    exact (dft_inversion f x).symm]  rw [expect_comm]  congr! with ψ  split_ifs with hψ  · rw [← mul_expect, AddChar.expect_iInf_ker_eq_one_of_mem_closure hV hψ, mul_one]  · rw [← mul_expect, AddChar.expect_iInf_ker_eq_zero_of_not_mem_closure hV hψ, mul_zero]