English
For χ, φ multiplicative characters and ψ additive with the same ψ, gaussSum χ ψ · gaussSum φ ψ equals ∑_{t∈R} ∑_{x∈R} χ(x) φ(t−x) ψ(t).
Русский
Для χ, φ мультипликативных символов и ψ аддитивного с тем же ψ гауссовы суммы удовлетворяют: gaussSum χ ψ · gaussSum φ ψ = ∑_{t∈R} ∑_{x∈R} χ(x) φ(t−x) ψ(t).
LaTeX
$$$\mathrm{gaussSum}(\chi, \psi) \cdot \mathrm{gaussSum}(\phi, \psi) = \displaystyle \sum_{t\in R} \sum_{x\in R} \chi(x) \phi(t-x) \psi(t)$$$
Lean4
/-- A formula for the product of two Gauss sums with the same additive character. -/
theorem gaussSum_mul {R : Type u} [CommRing R] [Fintype R] {R' : Type v} [CommRing R'] (χ φ : MulChar R R')
(ψ : AddChar R R') : gaussSum χ ψ * gaussSum φ ψ = ∑ t : R, ∑ x : R, χ x * φ (t - x) * ψ t :=
by
rw [gaussSum, gaussSum, sum_mul_sum]
conv => enter [1, 2, x, 2, x_1]; rw [mul_mul_mul_comm]
simp only [← ψ.map_add_eq_mul]
have sum_eq x : ∑ y : R, χ x * φ y * ψ (x + y) = ∑ y : R, χ x * φ (y - x) * ψ y :=
by
rw [sum_bij (fun a _ ↦ a + x)]
· simp only [mem_univ, forall_const]
· simp only [mem_univ, add_left_inj, imp_self, forall_const]
· exact fun b _ ↦ ⟨b - x, mem_univ _, by rw [sub_add_cancel]⟩
· exact fun a _ ↦ by rw [add_sub_cancel_right, add_comm]
rw [sum_congr rfl fun x _ ↦ sum_eq x, sum_comm]
-- In the following, we need `R` to be a finite field.
