Symmetry on L², as a real subspace

Pointwise symmetry cannot be carried into L² unchanged: elements of Lp are equivalence classes, so the property must be stated almost everywhere. Doing so needs one genuinely new ingredient — an a.e. statement has to be transportable through u ↦ -u, which holds because negation preserves Lebesgue measure and Ioo (-lam) lam is reflection-invariant.

Once that is available the symmetric elements form an ℝ-subspace. Not a ℂ-one: multiplying by i sends conj (f u) = f (-u) to conj (i · f u) = -i · conj (f u), which fails. That is exactly the structure the Gram–Schmidt argument needs, since its coefficients are real by inner_symmetric_im_eq_zero and so it never leaves the subspace.

theorem ZetaZeros.ae_restrict_Ioo_neg {lam : ℝ} {P : ℝ → Prop} (h : ∀ᵐ (u : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-lam) lam), P u) : ∀ᵐ (u : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-lam) lam), P (-u)

An almost-everywhere statement on the symmetric interval survives reflection. Negation preserves Lebesgue measure and Ioo (-lam) lam is reflection-invariant, so a null set is carried to a null set.

def ZetaZeros.IsSymmetricL2 {lam : ℝ} (f : ↥(L2Interval lam)) : Prop

Almost-everywhere symmetry for an element of L².

Equations

• ZetaZeros.IsSymmetricL2 f = ∀ᵐ (u : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-lam) lam), (starRingEnd ℂ) (↑↑f u) = ↑↑f (-u)

noncomputable def ZetaZeros.symmetricSubspace (lam : ℝ) : Submodule ℝ ↥(L2Interval lam)

The symmetric elements form an ℝ-subspace of L².

Equations

• ZetaZeros.symmetricSubspace lam = { carrier := {f : ↥(ZetaZeros.L2Interval lam) | ZetaZeros.IsSymmetricL2 f}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }