The dimension gap between the first two subspaces #
dim V - dim U ≤ |R₁|: passing from U to V adds only the twisted functions at the simple real
points, one per point, so the dimension can grow by at most their number.
This is the bound that turns the source's second-range estimate into a statement about the count of simple real elements — the quantity the whole proposition is about.
theorem
ZetaZeros.finrank_sup_le
{M : Type u_1}
[AddCommGroup M]
[Module ℂ M]
(p q : Submodule ℂ M)
[FiniteDimensional ℂ ↥p]
[FiniteDimensional ℂ ↥q]
:
finrank (p ⊔ q) ≤ finrank p + finrank q for finitely-generated submodules of an arbitrary
module. Mathlib's finrank_sup_add_finrank_inf_eq needs the ambient module finite-dimensional,
which L² is not, so the bound is built here from the surjection p × q → p ⊔ q.
theorem
ZetaZeros.finrank_subspaceV_le
{lam : ℝ}
{eta : ℝ → ℝ}
(h : IsAdmissible lam eta)
(Z : Finset ℂ)
(m : ℂ → ℕ)
:
Module.finrank ℂ ↥(subspaceV h Z m) ≤ Module.finrank ℂ ↥(subspaceU h Z m) + (simpleRealPart Z m).card
The dimension gap. Passing from U to V costs at most one dimension per simple real
point.