First properties of the extremal test function and the rescaling

The extremal test function is strictly positive on its support — which is what makes its square root smooth, and hence the whole kernel construction possible — and the rescaling sends a zero to a real point exactly when that zero lies on the critical line.

From those, the normalised cutoff test function η_ψ and its square f_ψ are shown to be smooth, compactly supported in (-1/2, 1/2) and even — and then so is the self-convolution Q_ψ, on (-1, 1), together with its second derivative.

theorem ZetaZeros.extremalTest_pos {x : ℝ} (hx : |x| ≤ 1 / 2) : 0 < extremalTest x

The extremal test function is strictly positive on [-1/2, 1/2].

theorem ZetaZeros.rescale_im_eq_zero_iff {T : ℝ} (hT : 1 < T) (ρ : ℂ) : (rescale T ρ).im = 0 ↔ ρ.re = 1 / 2

The rescaling sends a zero to a real point exactly when the zero is on the critical line.

The normalised cutoff test function is smooth, compactly supported and even

The delicate point is ±1/2: there √f₀ is not smooth, because f₀ jumps from a positive value down to 0. What saves it is that a δ-cutoff VANISHES on a neighbourhood of every such point, so the product is locally constant there.

Stated without 0 < δ < 1/4 and without positivity of A_ψ: neither is needed. When A_ψ = 0 the division gives η_ψ = 0, which is smooth, supported anywhere and even.

theorem ZetaZeros.sqrt_two_mul_sin_pos : 0 < √2 * Real.sin (1 / √2)

Positivity of the normalising denominator of f₀, read off from extremalTest_pos at 0 rather than re-proved, so the library holds only one proof of it.

theorem ZetaZeros.cutoffTest_eq_unfolded {delta : ℝ} {psi : ℝ → ℝ} (h : IsCutoff delta psi) : cutoffTest psi = fun (x : ℝ) => psi x * √(Real.cos (√2 * x) / (√2 * Real.sin (1 / √2))) / √(cutoffNormaliser psi)

Off [-1/2, 1/2] the cutoff kills the product, so on ALL of ℝ the test function agrees with the expression that has f₀'s if removed. That representative is smooth wherever cos (√2 x) > 0, and the cutoff handles everywhere else.

theorem ZetaZeros.cutoffTest_contDiff {delta : ℝ} {psi : ℝ → ℝ} (h : IsCutoff delta psi) : ContDiff ℝ (↑⊤) (cutoffTest psi)

η_ψ is smooth.

theorem ZetaZeros.cutoffTest_eq_zero_of_half_le_abs {delta : ℝ} {psi : ℝ → ℝ} (h : IsCutoff delta psi) {x : ℝ} (hx : 1 / 2 ≤ |x|) : cutoffTest psi x = 0

η_ψ vanishes off (-1/2, 1/2).

theorem ZetaZeros.cutoffTest_hasCompactSupport {delta : ℝ} {psi : ℝ → ℝ} (h : IsCutoff delta psi) : HasCompactSupport (cutoffTest psi)

η_ψ has compact support -- the C_c half of C_c^∞.

theorem ZetaZeros.cutoffTest_neg {delta : ℝ} {psi : ℝ → ℝ} (h : IsCutoff delta psi) (x : ℝ) : cutoffTest psi (-x) = cutoffTest psi x

η_ψ is even.

theorem ZetaZeros.cutoffTestSq_contDiff {delta : ℝ} {psi : ℝ → ℝ} (h : IsCutoff delta psi) : ContDiff ℝ (↑⊤) (cutoffTestSq psi)

f_ψ is smooth.

theorem ZetaZeros.cutoffTestSq_eq_zero_of_half_le_abs {delta : ℝ} {psi : ℝ → ℝ} (h : IsCutoff delta psi) {x : ℝ} (hx : 1 / 2 ≤ |x|) : cutoffTestSq psi x = 0

f_ψ vanishes off (-1/2, 1/2).

theorem ZetaZeros.cutoffTestSq_hasCompactSupport {delta : ℝ} {psi : ℝ → ℝ} (h : IsCutoff delta psi) : HasCompactSupport (cutoffTestSq psi)

f_ψ has compact support.

theorem ZetaZeros.cutoffTestSq_neg {delta : ℝ} {psi : ℝ → ℝ} (h : IsCutoff delta psi) (x : ℝ) : cutoffTestSq psi (-x) = cutoffTestSq psi x

f_ψ is even.

The self-convolution Q_psi: smoothness, support, parity

Q_psi is f_psi convolved with itself, so Mathlib's convolution theory applies once f_psi is known smooth with compact support, which is cutoffTestSq_contDiff and cutoffTestSq_hasCompactSupport.

The support claim doubles: f_psi lives in (-1/2, 1/2), so the convolution lives in (-1, 1). The elementary reason is that the integrand f_psi t * f_psi (x - t) is identically zero when 1 <= |x|: either |t| >= 1/2, killing the first factor, or |t| < 1/2 and then |x - t| >= |x| - |t| > 1/2, killing the second.

For Q_psi'' the support and parity are inherited rather than recomputed: derivatives cannot enlarge the support (tsupport_deriv_subset), and iteratedDeriv_comp_neg turns evenness of Q_psi into evenness of an even-order derivative.

theorem ZetaZeros.le_abs_of_notMem_Icc {c x : ℝ} (hx : x ∉ Set.Icc (-c) c) : c ≤ |x|

Outside [-c, c] the absolute value is at least c. Used repeatedly to turn a HasCompactSupport.intro obligation into the pointwise vanishing statement.

theorem ZetaZeros.cutoffSelfConv_eq_convolution (psi : ℝ → ℝ) : cutoffSelfConv psi = MeasureTheory.convolution (cutoffTestSq psi) (cutoffTestSq psi) (ContinuousLinearMap.mul ℝ ℝ) MeasureTheory.volume

Q_psi is Mathlib's convolution of f_psi with itself. Definitional, but it is what makes the convolution smoothness theorem applicable.

theorem ZetaZeros.contDiff_cutoffSelfConv {delta : ℝ} {psi : ℝ → ℝ} (h : IsCutoff delta psi) : ContDiff ℝ (↑⊤) (cutoffSelfConv psi)

Q_psi is smooth.

theorem ZetaZeros.cutoffSelfConv_eq_zero_of_one_le_abs {delta : ℝ} {psi : ℝ → ℝ} (h : IsCutoff delta psi) {x : ℝ} (hx : 1 ≤ |x|) : cutoffSelfConv psi x = 0

Q_psi vanishes off (-1, 1).

theorem ZetaZeros.hasCompactSupport_cutoffSelfConv {delta : ℝ} {psi : ℝ → ℝ} (h : IsCutoff delta psi) : HasCompactSupport (cutoffSelfConv psi)

Q_psi has compact support.

theorem ZetaZeros.cutoffSelfConv_neg {delta : ℝ} {psi : ℝ → ℝ} (h : IsCutoff delta psi) (x : ℝ) : cutoffSelfConv psi (-x) = cutoffSelfConv psi x

Q_psi is even.

theorem ZetaZeros.exists_lipschitzOnWith_cutoffSelfConv {delta : ℝ} {psi : ℝ → ℝ} (h : IsCutoff delta psi) : ∃ (K : NNReal), ∃ t ∈ nhds 0, LipschitzOnWith K (cutoffSelfConv psi) t

Q_psi is Lipschitz continuous at 0 -- Lipschitz with some constant on some neighbourhood of 0, which is what "Lipschitz continuous at 0" means here.

theorem ZetaZeros.contDiff_iteratedDeriv_two_cutoffSelfConv {delta : ℝ} {psi : ℝ → ℝ} (h : IsCutoff delta psi) : ContDiff ℝ (↑⊤) (iteratedDeriv 2 (cutoffSelfConv psi))

Q_psi'' is smooth.

theorem ZetaZeros.iteratedDeriv_two_cutoffSelfConv_eq_zero {delta : ℝ} {psi : ℝ → ℝ} (h : IsCutoff delta psi) {x : ℝ} (hx : 1 < |x|) : iteratedDeriv 2 (cutoffSelfConv psi) x = 0

Q_psi'' vanishes off [-1, 1]. A derivative cannot enlarge the support.

theorem ZetaZeros.iteratedDeriv_two_cutoffSelfConv_neg {delta : ℝ} {psi : ℝ → ℝ} (h : IsCutoff delta psi) (x : ℝ) : iteratedDeriv 2 (cutoffSelfConv psi) (-x) = iteratedDeriv 2 (cutoffSelfConv psi) x

Q_psi'' is even, being an even-order derivative of an even function.

theorem ZetaZeros.exists_lipschitzOnWith_iteratedDeriv_two_cutoffSelfConv {delta : ℝ} {psi : ℝ → ℝ} (h : IsCutoff delta psi) : ∃ (K : NNReal), ∃ t ∈ nhds 0, LipschitzOnWith K (iteratedDeriv 2 (cutoffSelfConv psi)) t

Q_psi'' is Lipschitz continuous at 0.