Properties of the extremal test function

f_0 is even, vanishes off [-1/2, 1/2], has total mass one, and is measurable, bounded and continuous on its support. Every later step rests on these, and none mentions the functional.

theorem ZetaZeros.extremalTest_even (x : ℝ) : extremalTest (-x) = extremalTest x

f₀ is even. Immediate from cos being even and |-x| = |x|.

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

f₀ is supported in [-1/2, 1/2]: it vanishes outside.

theorem ZetaZeros.extremalTest_eqOn_uIcc : Set.EqOn extremalTest (fun (x : ℝ) => Real.cos (√2 * x) / (√2 * Real.sin (1 / √2))) (Set.uIcc (-1 / 2) (1 / 2))

On the closed interval [-1/2,1/2], extremalTest agrees with the continuous cos(√2 ·)/(√2 sin(1/√2)) (the jump of the indicator is strictly outside).

theorem ZetaZeros.extremalTest_continuousOn : ContinuousOn extremalTest (Set.uIcc (-1 / 2) (1 / 2))

extremalTest is continuous on [-1/2,1/2].

theorem ZetaZeros.extremalTest_intervalIntegrable : IntervalIntegrable extremalTest MeasureTheory.volume (-1 / 2) (1 / 2)

extremalTest is interval-integrable on [-1/2,1/2].

theorem ZetaZeros.extremalTest_measurable : Measurable extremalTest

extremalTest is measurable.

theorem ZetaZeros.extremalTest_abs_le (x : ℝ) : |extremalTest x| ≤ (√2 * Real.sin (1 / √2))⁻¹

extremalTest is bounded: |extremalTest x| ≤ C with C = (√2 sin(1/√2))⁻¹.

theorem ZetaZeros.extremalTest_integrableOn {s : Set ℝ} (hs : MeasureTheory.volume s < ⊤) : MeasureTheory.IntegrableOn extremalTest s MeasureTheory.volume

extremalTest is IntegrableOn any measurable set of finite measure.