Integrability and factorisation for the Bessel coefficients #
The analytic ingredients alphaCoeff_eq needs on top of the algebraic identity bigF_eq.
Integrability is Hölder with p = q = 2: each factor is a twisted function, square-integrable by
memLp_fz, against a conjugated L² element, so the product is L¹. That is what licenses
splitting the finite sum under the integral.
The factorisation of the double integral needs no integrability: pulling a constant out of a Bochner integral is unconditional, so a separable integrand factors by two such pulls rather than by Fubini.
A conjugated L² element is still in L².
A twisted function against a conjugated L² element is integrable: Hölder with p = q = 2.
The even part against a conjugated L² element is integrable.
The odd part against a conjugated L² element is integrable.
The double integral of a finite sum of separable terms. Splitting the sum under the integral is what needs the integrability hypothesis; each term then factors as a square with none.
This is the reusable core of alphaCoeff_eq, applied once per family (fz, gz, hz).
The Bessel coefficient in terms of one-variable integrals.
Stated for an arbitrary family psi: the identity is linearity together with bigF_eq, so the
source's adapted-orthonormal-basis hypothesis plays no role and is dropped.
The set-integral form of inner_symmetric_im_eq_zero. The pairing of two symmetric
functions over the symmetric interval is real.
The Bessel coefficients are real.
Orthogonality to a spanning set extends to the span.
fzL2 agrees a.e. with fz.
gzL2 agrees a.e. with gz.
hzL2 agrees a.e. with hz.
Pointwise symmetry of a representing function gives a.e. symmetry of the L² element.
At a real point the twisted function is a symmetric L² element.
The even part is a symmetric L² element.
The odd part is a symmetric L² element.
Inner products of symmetric L² elements are real.
The integral of Φ * conj ψ, for a function Φ agreeing a.e. with an L² element, is the
inner product ⟪ψ, Φ⟫.
alphaCoeff_eq, restated for a single vector. Definitionally the same statement.
A Bessel coefficient against a symmetric L² element is real.
Past dim V the Bessel coefficient is non-positive.
The conjugate of a twisted function is still square-integrable.
The even and odd parts differ by exactly one in squared L² norm (lem_g_h_norm_diff).
The kernel at 0 is 1, and by the Gram identity it is the pairing of f_z against
f_{conj z}. Pointwise the real part of that pairing is already ‖g_z‖² - ‖h_z‖², because the
cross term is g conj h + h conj g = 2 re (g conj h), which is real, so I times it contributes
nothing. Taking real parts once — rather than expanding the product into four integrals and
discharging integrability for each — is what keeps this short.
Conjugating the index leaves the even part unchanged as an L² element.
Conjugation is injective on the complex numbers.
Conjugation maps the non-real support to itself.
The lower half of the non-real support is exactly the conjugate image of the upper half. Conjugation has no fixed point there, since every point has non-zero imaginary part.
The non-real support has exactly twice as many points as its upper half.
The dimension of U (lem_dim_U). It is spanned by one vector per multiple real point
together with the even parts at the non-real points, and conjugation identifies those in pairs, so
they contribute only half of |S|. The half is exact rather than a floor, because |S| is even.
Alternating series, and the three external inputs #
Alternating series bracketing (lem_alt_bracket). The partial sums of an alternating
series with antitone terms bracket its limit: even-length sums from below, odd-length from above.
Generalised off the source, which also assumes the terms non-negative and null: neither is needed once the limit is a hypothesis, and Mathlib's two one-sided bounds ask only for antitonicity.
Bessel input for the second-range estimate #
Orthogonality to an initial segment's span. If the first d members of an orthonormal
family span K, then every later member is orthogonal to all of K.
Factored out because both range estimates need it — for U and for V — with only d changing.
R₁ and R₂ are disjoint: multiplicity exactly one versus at least two.
The second-range estimate (lem_alpha_second_upper). Summed over dim U < j ≤ dim V, the
Bessel coefficients are bounded by the number of simple real points.
Past dim U the basis vector is orthogonal to U, so the R₂ and S pairings drop out and only
R₁ survives — with weight one, since that is what R₁ means. Discarding the subtracted h_z sum
(non-negative) and applying Bessel to each f_x, which is a unit vector at a real point, gives one
per point of R₁.
The cutoff normalising constant #
The extremal test function is non-negative everywhere: positive on [-1/2, 1/2] and zero
off it.
The normalising constant is positive.
The integrand ψ²f₀ is non-negative, and on |x| ≤ 1/2 - δ it equals f₀ > 0, a set of positive
measure. Note it is NOT positive throughout (-1/2, 1/2): a cutoff may vanish between 1/2 - δ
and 1/2, so the argument has to go through the support rather than through positivity on the
whole interval.
0 < δ is genuinely needed, not decoration: with δ negative the shrunken interval |x| ≤ 1/2 - δ
would be LARGER than [-1/2, 1/2], and f₀ is only positive on the latter.
Parseval at elements of the span, for an arbitrary finite index type.
Mathlib has Bessel for an arbitrary element (Orthonormal.sum_inner_products_le) and the equality
only through OrthonormalBasis, which wants the family to span the WHOLE space. Here the family
spans a proper submodule, so the statement is proved from the expansion directly: the inner product
against a basis vector picks out that coefficient, and the squared norm is the sum of the squared
coefficients.
The Fin N specialization of sum_sq_norm_inner_eq_norm_sq_of_span.
The tensor squares pair as the square of the inner product, hence are orthonormal in
L²(I²).
This needs no Fubini: the double integral factors by pulling a constant out of each integral, the
same route integral_double_finsetSum takes.
The total Bessel sum #
The real part of a natural multiple of the square of a real complex number.
Not private: a private name is mangled, so the axiom probe reports Unknown constant for it and
then cannot gate the file at all.
The total Bessel sum (lem_alpha_sum_total). Over the whole basis the coefficients sum to
the total multiplicity.
Parseval, not Bessel: the pairings are summed over the FULL basis, so each spanning vector
contributes exactly its squared norm — one for each f_x at a real point, and one for each
non-real z by the norm defect between g_z and h_z.
The adapted orthonormal basis #
The new ingredient over standard Gram--Schmidt is that every vector stays in the prescribed real subspace, which is what carries the paper's symmetry.
Scoped in a section: it opens Set and Submodule, which the rest of this file does not.
(Crux, uses hreal.) Every Gram-Schmidt vector of a family lying in the real subspace S
stays in S.
Argument: strong induction on i using the recursion
gramSchmidt ℂ v i = v i - ∑_{k<i} (ℂ ∙ gramSchmidt ℂ v k).starProjection (v i)
(InnerProductSpace.gramSchmidt_def). Each summand is
(ℂ ∙ g k).starProjection (v i); for a unit vector u, (ℂ ∙ u).starProjection w = ⟪u,w⟫ • u,
and in general the projection onto the line ℂ ∙ (g k) is (⟪g k, v i⟫ / ‖g k‖²) • g k. By the
induction hypothesis g k ∈ S, and v i ∈ S, so by hreal the coefficient ⟪g k, v i⟫ is real;
dividing by the real ‖g k‖² keeps it real. Since S is an ℝ-submodule it is closed under real
scalar multiplication, so each summand lies in S, and thus v i - (sum) = g i ∈ S.
The normalized Gram-Schmidt vectors also stay in S: gn i = ‖g i‖⁻¹ • g i is a real scalar
multiple of g i ∈ S.
Existence of an adapted orthonormal basis inside a real subspace.
v is a finite ordered family spanning W; its initial segments of lengths dU and dV span two
nested subspaces. There is an orthonormal family spanning the same W, lying in S, whose own
initial segments (of the appropriate dimensions) span those same two subspaces.
A symmetric adapted basis for the three Hilbert subspaces #
A symmetric adapted basis exists.
Order the natural spanning vectors in three blocks: the generators of U, the further
generators of V, and the further generators of W. The real Gram–Schmidt construction above
then preserves symmetry and its initial segments span exactly U and V.
Multiplicity of a non-trivial zero #
Every non-trivial zero has multiplicity at least one (lem_mult_pos).
Two things have to be ruled out, and only one of them is the obvious one. The order is not 0
because zeta is analytic at the point and vanishes there. It is also not ⊤: zeta is not
identically zero near the point, and the only route to that is the identity theorem on the
punctured plane, where zeta 2 ≠ 0 supplies the contradiction.
The rescaled zeros carry the three counts #
The rescaling is injective: it is affine with non-zero linear coefficient.
The transported multiplicity agrees with the original at a rescaled point.
The rescaled zeros carry the counted total (part of lem_Z_T_counts).
The rescaled zeros carry the distinct count (part of lem_Z_T_counts).
The rescaled zeros carry the simple-on-line count (part of lem_Z_T_counts).
The third of the entity's three conjuncts. Under the bijection a rescaled point is real exactly
when the zero is on the critical line (rescale_im_eq_zero_iff) and has multiplicity one exactly
when the zero does.
Parseval over a sub-family, at elements of that sub-family's span.
The normalised test function has total mass one #
Bessel for a kernel against tensor squares #
The abstract statement: it mentions no admissible eta, no bigF and no alphaCoeff. What the
instantiation still needs is that bigF and the tensor squares are MemLp 2 for the product
measure; the orthonormality hypothesis is discharged by integral_tensor_square_pairing.
Bessel for a kernel paired against tensor squares.
phi is a finite family whose tensor squares are orthonormal in the iterated-integral pairing
(horth). Then the squared pairings of the kernel K against them are dominated by the squared
L² norm of K.
The tensor product of two L² functions is L² for the product measure.
The normalised cutoff test function is 1/2-admissible.
Three of the four fields are the smoothness, support and integral facts for cutoffTest read off
directly. Only square-integrability is new, and it is immediate once the function is known to be
continuous with compact support -- which is why HasCompactSupport was worth stating there rather
than leaving the support condition purely pointwise.
The kernel sums agree #
The double sum over the rescaled zeros and the double sum over the actual
zeros are the same sum, reindexed along the rescaling. Two facts carry it: the rescaling is
injective, so Finset.sum_image applies at both levels; and it turns a difference of zeros into
exactly the rescaled difference the pair-correlation formula is stated with.
Stated without an admissibility hypothesis on eta: nothing in a reindexing can use it.
The rescaling turns a difference of zeros into the rescaled difference.
The kernel sums agree (lem_kernel_sum_identity).
The Fourier transform of the self-convolution #
The convolution theorem, at a complex frequency. The move worth keeping is to abstract the
character: the statement holds for any continuous E : ℝ → ℂ with
E (a + b) = E a * E b, and the complex frequency then stops being special -- no
analytic-continuation argument is needed, only Fubini on the compactly supported integrand.
The bookkeeping behind the second moment #
A double integral whose integrand is a finite double sum with factored terms equals the double sum of the products of the single integrals. Also stated abstractly.
Abstract version: for any continuous multiplicative character E, the "transform" of a
self-convolution factors.
A double integral of a factored double sum.
The two instantiations #
A twisted function against another twisted function's conjugate is integrable.
Distinct from the existing integrable_fz_mul_conj, which pairs against an L² ELEMENT. That
one is not syntactically usable here: (fzL2 h s : ℝ → ℂ) is only a.e. equal to fz eta s, so
applying it would need an Integrable.congr where memLp_fz directly needs nothing.
The second moment is the L²(I²) norm of the two-variable kernel (lem_second_moment).
Bessel's inequality for the two-variable kernel #
The abstract inequality is sum_sq_pairing_le_integral_norm_sq, and the orthonormality of the
tensor squares is integral_tensor_square_pairing. What is left is the integrability, which is
proved here rather than assumed as a hypothesis.
bigF is a finite sum of tensor products, so memLp_tensor_two on each summand and
memLp_finsetSum over Z does it; the basis members give their tensor squares the same way.
Realness of the coefficients is not needed. The usual argument invokes alphaCoeff_im_eq_zero to
turn |alpha_j|^2 into alpha_j^2; but the norm form is the stronger inequality and
(re a)^2 ≤ ‖a‖^2 holds for every complex a, so the real-coefficient form follows with no appeal
to realness, no conjugation-invariance and no symmetry hypothesis. That matters practically:
alphaCoeff_im_eq_zero wants pointwise IsSymmetric, whereas a Gram--Schmidt basis is only
symmetric almost everywhere.
The two-variable kernel is L² on the square: it is a finite sum of tensor products.
The tensor square of an L² element is L² on the square.
Bessel's inequality for the kernel, in norm form. Stronger than the real-coefficient form, and what actually gets proved.
Bessel's inequality for the kernel (lem_bessel_F).
Stated without conjugation-invariance of (Z, m) and without symmetry of the basis members: the
norm form above needs neither, and (re a)^2 <= ‖a‖^2 delivers this from it.
The rescaled multiset is conjugation-invariant #
The composite symmetry rho ↦ 1 - conj rho is what makes the rescaled zeros conjugation-invariant.
Both halves are available: zeroMultiplicity_conj for conjugation and zeroMultiplicity_one_sub
for the reflection.
The computation is that conjugating a rescaled zero rescales the REFLECTED CONJUGATE:
conj (rescale T rho) = rescale T (1 - conj rho). Everything else follows, and the vanishing of
zeta at 1 - conj rho comes straight from the functional equation rather than through the
multiplicity -- zeta (conj rho) = conj (zeta rho) = 0, so the product form vanishes.
Conjugating a rescaled point rescales the reflected conjugate.
The reflected conjugate of a non-trivial zero is a non-trivial zero at the same height.
The rescaled multiset is conjugation-invariant (lem_Z_T_conj).
The tensor square of an L² function belongs to L² for the product measure.
The kernel second moment #
The unconjugated finite kernel sum is the product-space second moment of bigF.
The Gram identity initially conjugates the second support point; conjugation invariance permits
the change of variables back to the difference z - s.
Real-valued form of the second-moment identity, matching the right side of Bessel's inequality.
The first-range coefficient estimate #
The real part of one coefficient expressed entirely in squared Hilbert-space pairings.
This is the common pointwise form used by the Parseval/Bessel arguments for the three basis ranges. Symmetry makes all the pairings real, so the real part of their complex squares is their squared norm.
First range: lower bound for the coefficient sum (lem_alpha_first_lower).
Parseval on the initial segment spanning U is exact for the f_x at multiple real points and
the g_z at non-real points. Bessel bounds the subtracted h_z terms, leaving the unit norm
defect. Finally multiplicities are at least two on R₂ and at least one on the support.
Three-range algebra #
The numerical three-range estimate used for the simple-real-point bound.
The first range uses a² + 4 ≥ 4a, the middle range uses a² + 1 ≥ 2a, and the
last range uses a ≤ 0.
Lower bound for the simple real elements (prop_simple_real_lower).
The numerical three-range estimate used for the distinct-point bound.
Compared with three_range_simple, all three ranges retain a factor four. On the middle range,
the upper bound on its coefficient sum supplies the extra factor two.
Lower bound for the distinct elements (prop_distinct_lower).