Symmetry of the twisted functions

Conjugation acts on the twisted functions as reflection in the origin. This is the property that survives Gram–Schmidt and makes every Bessel coefficient real, which is what lets the source treat them with real inequalities rather than complex ones.

Everything here follows from one computation, conj_fz: conjugating fz eta z reflects the argument and conjugates the twist.

theorem ZetaZeros.conj_fz {eta : ℝ → ℝ} (he : ∀ (x : ℝ), eta (-x) = eta x) (z : ℂ) (u : ℝ) : (starRingEnd ℂ) (fz eta z u) = fz eta ((starRingEnd ℂ) z) (-u)

Conjugation reflects the argument and conjugates the twist. The single computation the three symmetry lemmas below rest on.

theorem ZetaZeros.isSymmetric_fz {lam : ℝ} {eta : ℝ → ℝ} (h : IsAdmissible lam eta) {x : ℂ} (hx : x.im = 0) : IsSymmetric (fz eta x)

At a real point the twisted function is symmetric.

theorem ZetaZeros.isSymmetric_gz {lam : ℝ} {eta : ℝ → ℝ} (h : IsAdmissible lam eta) (z : ℂ) : IsSymmetric (gz eta z)

The even part is symmetric.

theorem ZetaZeros.isSymmetric_hz {lam : ℝ} {eta : ℝ → ℝ} (h : IsAdmissible lam eta) (z : ℂ) : IsSymmetric (hz eta z)

The odd part is symmetric.