English
For any i ∈ d and z: d → AddCircle(1) we have mFourier (Pi.single i 1) z = fourier 1 (z i).
Русский
Для любого индекса i и функции z: d → AddCircle(1) выполняется равенство mFourier (Pi.single i 1) z = fourier 1 (z i).
LaTeX
$$$ mFourier(\mathrm{Pi}.single i 1)\, z = fourier\,1\,(z(i)) $$$
Lean4
theorem mFourier_single [DecidableEq d] (z : d → AddCircle (1 : ℝ)) (i : d) :
mFourier (Pi.single i 1) z = fourier 1 (z i) :=
by
simp_rw [mFourier, ContinuousMap.coe_mk]
have := Finset.prod_mul_prod_compl { i } (fun j ↦ fourier ((Pi.single i (1 : ℤ) : d → ℤ) j) (z j))
rw [Finset.prod_singleton, Finset.prod_congr rfl (fun j hj ↦ ?_)] at this
· rw [← this, Finset.prod_const_one, mul_one, Pi.single_eq_same]
· rw [Finset.mem_compl, Finset.mem_singleton] at hj
simp only [Pi.single_eq_of_ne hj, fourier_zero]
