English
If χ and φ are multiplicative characters with χφ ≠ 1, then gaussSum(χφ)ψ · jacobiSum(χ, φ) = gaussSum(χ)ψ · gaussSum(φ)ψ for any additive ψ.
Русский
Если χ и φ — мультипликативные символы с χφ ≠ 1, то gaussSum(χφ)ψ · jacobiSum(χ, φ) = gaussSum(χ)ψ · gaussSum(φ)ψ для любого аддитивного ψ.
LaTeX
$$$$ \gaussSum(χ φ) ψ \cdot J(χ, φ) = \gaussSum(χ) ψ \cdot \gaussSum(φ) ψ, \quad χ φ \neq 1. $$$$
Lean4
/-- If `χ` and `φ` are multiplicative characters on a finite field `F` such that
`χφ` is nontrivial, then `g(χφ) * J(χ,φ) = g(χ) * g(φ)`. -/
theorem jacobiSum_mul_nontrivial {χ φ : MulChar F R} (h : χ * φ ≠ 1) (ψ : AddChar F R) :
gaussSum (χ * φ) ψ * jacobiSum χ φ = gaussSum χ ψ * gaussSum φ ψ := by
classical
rw [gaussSum_mul _ _ ψ, sum_eq_sum_diff_singleton_add (mem_univ (0 : F))]
conv =>
enter [2, 2, 2, x]
rw [zero_sub, neg_eq_neg_one_mul x, map_mul, mul_left_comm (χ x) (φ (-1)), ← MulChar.mul_apply, ψ.map_zero_eq_one,
mul_one]
rw [← mul_sum _ _ (φ (-1)), MulChar.sum_eq_zero_of_ne_one h, mul_zero, add_zero]
have sum_eq : ∀ t ∈ univ \ {0}, (∑ x : F, χ x * φ (t - x)) * ψ t = (∑ y : F, χ (t * y) * φ (t - (t * y))) * ψ t :=
by
intro t ht
simp only [mem_sdiff, mem_univ, mem_singleton, true_and] at ht
exact congrArg (· * ψ t) (Equiv.sum_comp (Equiv.mulLeft₀ t ht) _).symm
simp_rw [← sum_mul, sum_congr rfl sum_eq, ← mul_one_sub, map_mul, mul_assoc]
conv => enter [2, 2, t, 1, 2, x, 2]; rw [← mul_assoc, mul_comm (χ x) (φ t)]
simp_rw [← mul_assoc, ← MulChar.mul_apply, mul_assoc, ← mul_sum, mul_right_comm]
rw [← jacobiSum, ← sum_mul, gaussSum, sum_eq_sum_diff_singleton_add (mem_univ (0 : F)), (χ * φ).map_zero, zero_mul,
add_zero]
