Documentation

MathlibNt.AnalyticNumberTheory.LargeSieve.TruncatedPerronKernel

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.

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

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

Equations
Instances For
    source
    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.

    source
    @[simp]
    theorem AnalyticNumberTheory.LargeSieve.truncatedPerronIntegrand_zero_right (x : ℝ) :
    truncatedPerronIntegrand x 0 = x
    source
    @[simp]
    theorem AnalyticNumberTheory.LargeSieve.truncatedPerronIntegrand_zero_left (t : ℝ) :
    truncatedPerronIntegrand 0 t = 0
    source
    @[simp]
    theorem AnalyticNumberTheory.LargeSieve.truncatedPerronIntegrand_neg_left (x t : ℝ) :
    truncatedPerronIntegrand (-x) t = -truncatedPerronIntegrand x t
    source
    theorem AnalyticNumberTheory.LargeSieve.continuous_truncatedPerronIntegrand_right (x : ℝ) :
    Continuous (truncatedPerronIntegrand x)

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

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

    Continuity in the Perron spatial variable.

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

    Joint continuity of the removable sine kernel.

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

    The sine kernel is integrable on every finite interval.

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

    The real truncated Perron kernel.

    Equations
    Instances For
      source
      @[simp]
      theorem AnalyticNumberTheory.LargeSieve.truncatedPerronKernel_zero (T : ℝ) :
      truncatedPerronKernel T 0 = 1 / 2
      source
      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.

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

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

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

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

      source
      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.

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

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

      source
      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.

      source
      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.