Interval-integrability of the integrands

Side conditions only: f_0 against the linear, max and shifted-max kernels must be interval-integrable, and the outer integral needs a continuous integrand.

theorem ZetaZeros.extremalTest_intervalIntegrable_gen (p q : ℝ) : IntervalIntegrable extremalTest MeasureTheory.volume p q

extremalTest is interval-integrable on any interval.

theorem ZetaZeros.linTest_intervalIntegrable (t p q : ℝ) : IntervalIntegrable (fun (β : ℝ) => (β + t) * extremalTest β) MeasureTheory.volume p q

(β + t) · f₀ β and max(β+t, 0) · f₀ β are interval-integrable on any interval.

theorem ZetaZeros.maxTest_intervalIntegrable (t p q : ℝ) : IntervalIntegrable (fun (β : ℝ) => max (β + t) 0 * extremalTest β) MeasureTheory.volume p q

theorem ZetaZeros.maxSubTest_intervalIntegrable (c p q : ℝ) : IntervalIntegrable (fun (v : ℝ) => max (c - v) 0 * extremalTest v) MeasureTheory.volume p q

max(c - v, 0) · f₀ v is interval-integrable in v on any interval.

theorem ZetaZeros.outer_intervalIntegrable (K : ℝ → ℝ → ℝ) (hK : Continuous (Function.uncurry K)) : IntervalIntegrable (fun (t : ℝ) => extremalTest t * ∫ (v : ℝ) in -1 / 2..1 / 2, K t v * extremalTest v) MeasureTheory.volume (-1 / 2) (1 / 2)

For a jointly continuous kernel K, the outer integrand t ↦ f₀ t · ∫ v in -1/2..1/2, K t v · f₀ v is interval-integrable on [-1/2,1/2].