The L² inner product of symmetric elements is real

inner_symmetric_im_eq_zero says this for functions; Gram–Schmidt runs on L², so the same fact is needed for the inner product of Lp elements. The upgrade needs genuine measure-preservation of u ↦ -u on the restricted measure, rather than an a.e. transport, because a change of variables inside an integral is involved rather than a null-set argument.

With this, "the Gram–Schmidt coefficients are real" becomes a fact about the ambient space, which is what lets the process stay inside symmetricSubspace.

theorem ZetaZeros.measurePreserving_neg_Ioo (lam : ℝ) : MeasureTheory.MeasurePreserving (fun (u : ℝ) => -u) (MeasureTheory.volume.restrict (Set.Ioo (-lam) lam)) (MeasureTheory.volume.restrict (Set.Ioo (-lam) lam))

Negation preserves Lebesgue measure restricted to the symmetric interval.

theorem ZetaZeros.integral_comp_neg_Ioo {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (g : ℝ → E) (lam : ℝ) : ∫ (u : ℝ) in Set.Ioo (-lam) lam, g (-u) = ∫ (u : ℝ) in Set.Ioo (-lam) lam, g u

A reflection-invariant integral over the symmetric interval.