Source indexedlemma · leanprover/lean4:v4.32.0

wInner_one_cft

APAP.Prereqs.FourierTransform.Compact · APAP/Prereqs/FourierTransform/Compact.lean:50 to 57

Source documentation

Parseval-Plancherel identity for the discrete Fourier transform.

Exact Lean statement

@[simp] lemma wInner_one_cft (f g : G → ℂ) : ⟪cft f, cft g⟫_[ℂ] = ⟪f, g⟫ₙ_[ℂ]

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[simp] lemma wInner_one_cft (f g : G → ℂ) : ⟪cft f, cft g⟫_[ℂ] = ⟪f, g⟫ₙ_[ℂ] := by  classical  unfold cft  simp_rw [wInner_one_eq_sum, wInner_cWeight_eq_expect, inner_apply', map_expect, map_mul,    starRingEnd_self_apply, expect_mul, mul_expect, ← expect_sum_comm,    mul_mul_mul_comm _ (conj <| f _), ← sum_mul, ← AddChar.inv_apply_eq_conj, ← map_neg_eq_inv,    ← map_add_eq_mul, AddChar.sum_apply_eq_ite]  simp [add_neg_eq_zero, card_univ, Fintype.card_ne_zero, NNRat.smul_def]