The two-variable kernel in terms of even and odd parts

The algebraic heart of alphaCoeff_eq: rewriting F so that the non-real points contribute g_z(u) g_z(v) - h_z(u) h_z(v) rather than f_z(u) f_z(v).

The rewrite is not termwise — f_z(u) f_z(v) exceeds g_z(u)g_z(v) - h_z(u)h_z(v) by the cross term i(g_z(u)h_z(v) + h_z(u)g_z(v)). What makes it true is that conjugation is a fixed-point-free involution of the non-real part under which the cross term is odd, since gz is conjugation-invariant and hz anti-invariant. So the cross terms cancel in pairs and Finset.sum_involution kills the whole sum at once.

This is the step that lets the source's factor of two over conjugate pairs disappear entirely.

theorem ZetaZeros.union_realPart_nonRealPart {Z : Finset ℂ} {m : ℂ → ℕ} (hZ : IsConjInvariant Z m) : simpleRealPart Z m ∪ multipleRealPart Z m ∪ nonRealPart Z = Z

The support splits into its real and non-real parts.

theorem ZetaZeros.disjoint_realPart_nonRealPart {Z : Finset ℂ} {m : ℂ → ℕ} : Disjoint (simpleRealPart Z m ∪ multipleRealPart Z m) (nonRealPart Z)

The real and non-real parts are disjoint.

theorem ZetaZeros.sum_cross_eq_zero {eta : ℝ → ℝ} {Z : Finset ℂ} {m : ℂ → ℕ} (hZ : IsConjInvariant Z m) (u v : ℝ) : ∑ z ∈ nonRealPart Z, ↑(m z) * (Complex.I * (gz eta z u * hz eta z v + hz eta z u * gz eta z v)) = 0

The cross terms cancel over the non-real part: conjugation is a fixed-point-free involution there, and the cross term is odd under it.

theorem ZetaZeros.bigF_eq {eta : ℝ → ℝ} {Z : Finset ℂ} {m : ℂ → ℕ} (hZ : IsConjInvariant Z m) (u v : ℝ) : bigF eta Z m u v = ∑ x ∈ simpleRealPart Z m ∪ multipleRealPart Z m, ↑(m x) * fz eta x u * fz eta x v + ∑ z ∈ nonRealPart Z, ↑(m z) * (gz eta z u * gz eta z v - hz eta z u * hz eta z v)

The two-variable kernel in terms of even and odd parts.