Skip to main content
therefore
Sign inSign up
Open navigation
YaelDillies/APAP
Source indexedlemma Β· leanprover/lean4:v4.32.0

wInner_one_dddconv

APAP.Prereqs.Convolution.Norm Β· APAP/Prereqs/Convolution/Norm.lean:37 to 49

Mathematical statement

Exact Lean statement

lemma wInner_one_dddconv (f g h : G β†’ π•œ) : βŸͺf, g β—‹α΅ˆ h⟫_[π•œ] = βŸͺconj g, conj f βˆ—α΅ˆ conj h⟫_[π•œ]

Complete declaration

Lean source

Canonical source
Full Lean sourceLean 4
lemma wInner_one_dddconv (f g h : G β†’ π•œ) : βŸͺf, g β—‹α΅ˆ h⟫_[π•œ] = βŸͺconj g, conj f βˆ—α΅ˆ conj h⟫_[π•œ] := by  calc    _ = βˆ‘ b, βˆ‘ a, g a * conj (h b) * conj (f (a - b)) := by      simp_rw [wInner_one_eq_sum, RCLike.inner_apply, sum_dddconv_mul]      exact sum_comm    _ = βˆ‘ b, βˆ‘ a, conj (f a) * conj (h b) * g (a + b) := by      simp_rw [← Fintype.sum_prod_type']      exact Fintype.sum_equiv ((Equiv.refl _).prodShear Equiv.subRight) _ _        (by simp [mul_rotate, mul_right_comm])    _ = _ := by      simp_rw [wInner_one_eq_sum, RCLike.inner_apply, sum_ddconv_mul, Pi.conj_apply,        RCLike.conj_conj]      exact sum_comm