The truncated Perron sine kernel

This file records only the real-analytic foundation for a truncated Perron kernel. In particular, it makes no step-function or approximation claim.

noncomputable def AnalyticNumberTheory.LargeSieve.truncatedPerronIntegrand (x t : ℝ) : ℝ

The removable-at-zero form of sin (t * x) / t.

Equations

• AnalyticNumberTheory.LargeSieve.truncatedPerronIntegrand x t = if t = 0 then x else Real.sin (t * x) / t

theorem AnalyticNumberTheory.LargeSieve.truncatedPerronIntegrand_eq_mul_sinc (x t : ℝ) : truncatedPerronIntegrand x t = x * Real.sinc (t * x)

The removable definition is exactly x times Mathlib's unnormalised sinc.

@[simp]

theorem AnalyticNumberTheory.LargeSieve.truncatedPerronIntegrand_zero_right (x : ℝ) : truncatedPerronIntegrand x 0 = x

@[simp]

theorem AnalyticNumberTheory.LargeSieve.truncatedPerronIntegrand_zero_left (t : ℝ) : truncatedPerronIntegrand 0 t = 0

@[simp]

theorem AnalyticNumberTheory.LargeSieve.truncatedPerronIntegrand_neg_left (x t : ℝ) : truncatedPerronIntegrand (-x) t = -truncatedPerronIntegrand x t

theorem AnalyticNumberTheory.LargeSieve.continuous_truncatedPerronIntegrand_right (x : ℝ) : Continuous (truncatedPerronIntegrand x)

Continuity in the integration variable, including at the removable point t = 0.

theorem AnalyticNumberTheory.LargeSieve.continuous_truncatedPerronIntegrand_left (t : ℝ) : Continuous fun (x : ℝ) => truncatedPerronIntegrand x t

Continuity in the Perron spatial variable.

theorem AnalyticNumberTheory.LargeSieve.continuous_truncatedPerronIntegrand_uncurry : Continuous (Function.uncurry truncatedPerronIntegrand)

Joint continuity of the removable sine kernel.

theorem AnalyticNumberTheory.LargeSieve.intervalIntegrable_truncatedPerronIntegrand (x a b : ℝ) : IntervalIntegrable (truncatedPerronIntegrand x) MeasureTheory.volume a b

The sine kernel is integrable on every finite interval.

noncomputable def AnalyticNumberTheory.LargeSieve.truncatedPerronKernel (T x : ℝ) : ℝ

The real truncated Perron kernel.

Equations

• AnalyticNumberTheory.LargeSieve.truncatedPerronKernel T x = 1 / 2 + 1 / Real.pi * ∫ (t : ℝ) in 0..T, AnalyticNumberTheory.LargeSieve.truncatedPerronIntegrand x t

@[simp]

theorem AnalyticNumberTheory.LargeSieve.truncatedPerronKernel_zero (T : ℝ) : truncatedPerronKernel T 0 = 1 / 2

theorem AnalyticNumberTheory.LargeSieve.truncatedPerronKernel_neg (T x : ℝ) : truncatedPerronKernel T (-x) = 1 - truncatedPerronKernel T x

Reflection in the spatial variable exchanges the two sides of the kernel.

theorem AnalyticNumberTheory.LargeSieve.continuous_truncatedPerronKernel_left (T : ℝ) : Continuous fun (x : ℝ) => truncatedPerronKernel T x

For fixed truncation height, the kernel is continuous in x.

theorem AnalyticNumberTheory.LargeSieve.continuous_truncatedPerronKernel_right (x : ℝ) : Continuous fun (T : ℝ) => truncatedPerronKernel T x

For fixed x, the kernel is continuous in its truncation height.

theorem AnalyticNumberTheory.LargeSieve.abs_truncatedPerronKernel_sub_half_le_integral_abs {T x : ℝ} (hT : 0 ≤ T) : |truncatedPerronKernel T x - 1 / 2| ≤ 1 / Real.pi * ∫ (t : ℝ) in 0..T, |truncatedPerronIntegrand x t|

Triangle inequality for the defining integral.

theorem AnalyticNumberTheory.LargeSieve.abs_truncatedPerronIntegrand_le (x t : ℝ) : |truncatedPerronIntegrand x t| ≤ |x|

The sinc bound gives a uniform pointwise majorant for the integrand.

theorem AnalyticNumberTheory.LargeSieve.integral_abs_truncatedPerronIntegrand_le {T x : ℝ} (hT : 0 ≤ T) : ∫ (t : ℝ) in 0..T, |truncatedPerronIntegrand x t| ≤ T * |x|

Coarse but robust integral norm bound, sufficient for later L¹ estimates.

theorem AnalyticNumberTheory.LargeSieve.abs_truncatedPerronKernel_sub_half_le {T x : ℝ} (hT : 0 ≤ T) : |truncatedPerronKernel T x - 1 / 2| ≤ T * |x| / Real.pi

Combined triangle and uniform sinc bound.