Commit 2024-10-11 13:11 8839a89f

feat: L2 inner product of finite sequences (#16447) Define the weighted L2 inner product of functions f g : ∀ i, E i where ι is a fintype and the E i are 𝕜-inner product spaces where 𝕜 is RCLike as ∑ i, w i • inner (f i) (g i). This "duplicates" inner but is necessary because there are two useful (to discrete analysis) inner products on G → R given inner products on R and Fintype G, namely

• the usual "discrete" inner product ∑ i, conj (f i) * g i
• the less usual but nevertheless crucial "compact" inner product 𝔼 i, conj (f i) * g i From LeanAPAP