Inner products of symmetric functions are real

The reason the source may apply real inequalities such as a² + 1 ≥ 2a to the Bessel coefficients: every inner product formed from symmetric functions is real, because conjugating it is the same as reflecting the interval, and the interval (-lam, lam) is reflection-invariant.

theorem ZetaZeros.conj_inner_symmetric {Φ₁ Φ₂ : ℝ → ℂ} (h1 : IsSymmetric Φ₁) (h2 : IsSymmetric Φ₂) (lam : ℝ) : (starRingEnd ℂ) (∫ (u : ℝ) in -lam..lam, Φ₁ u * (starRingEnd ℂ) (Φ₂ u)) = ∫ (u : ℝ) in -lam..lam, Φ₁ u * (starRingEnd ℂ) (Φ₂ u)

Inner products of symmetric functions are self-conjugate.

theorem ZetaZeros.inner_symmetric_im_eq_zero {Φ₁ Φ₂ : ℝ → ℂ} (h1 : IsSymmetric Φ₁) (h2 : IsSymmetric Φ₂) (lam : ℝ) : (∫ (u : ℝ) in -lam..lam, Φ₁ u * (starRingEnd ℂ) (Φ₂ u)).im = 0

Inner products of symmetric functions are real.