Documentation

MathlibNt.AnalyticNumberTheory.LargeSieve.LandauSiegelToStandardBVCanonicalSmoothing

Canonical smoothing data for the raw Landau--Siegel Standard-BV endpoint #

This module constructs a fixed nonnegative smooth bump supported in [1/2, 2], normalizes it for the multiplicative measure dx/x, and removes all smoothing data from the final raw-Landau--Siegel-to-Standard-BV headline.

source
noncomputable def AnalyticNumberTheory.LargeSieve.standardBVCanonicalBaseBump :
ContDiffBump (5 / 4)

A concrete smooth bump centered at 5/4, with outer radius 3/4.

Equations
Instances For
    source
    noncomputable def AnalyticNumberTheory.LargeSieve.standardBVCanonicalWeight (x : ℝ) :
    ℝ

    The base bump multiplied by a globally continuous version of 1/x. On the support of the bump this is exactly standardBVCanonicalBaseBump x / x.

    Equations
    Instances For
      source
      noncomputable def AnalyticNumberTheory.LargeSieve.standardBVCanonicalWeightMass :
      ℝ

      The finite, strictly positive normalizing denominator.

      Equations
      Instances For
        source
        theorem AnalyticNumberTheory.LargeSieve.standardBVCanonicalWeight_continuous :
        Continuous standardBVCanonicalWeight
        source
        theorem AnalyticNumberTheory.LargeSieve.standardBVCanonicalWeight_hasCompactSupport :
        HasCompactSupport standardBVCanonicalWeight
        source
        theorem AnalyticNumberTheory.LargeSieve.standardBVCanonicalWeight_integrable :
        MeasureTheory.Integrable standardBVCanonicalWeight MeasureTheory.volume
        source
        theorem AnalyticNumberTheory.LargeSieve.standardBVCanonicalWeight_nonneg :
        0 ≤ standardBVCanonicalWeight
        source
        theorem AnalyticNumberTheory.LargeSieve.standardBVCanonicalWeightMass_pos :
        0 < standardBVCanonicalWeightMass

        The normalization denominator is positive (and hence nonzero).

        source
        noncomputable def AnalyticNumberTheory.LargeSieve.standardBVCanonicalSmoothing (x : ℝ) :
        ℝ

        The canonical smoothing function, normalized for dx/x.

        Equations
        Instances For
          source
          theorem AnalyticNumberTheory.LargeSieve.standardBVCanonicalSmoothing_contDiff :
          ContDiff ℝ 1 standardBVCanonicalSmoothing

          The canonical smoothing function is (in fact infinitely) smooth, hence C¹.

          source
          theorem AnalyticNumberTheory.LargeSieve.standardBVCanonicalSmoothing_nonneg_all (x : ℝ) :
          0 ≤ standardBVCanonicalSmoothing x

          The canonical smoothing function is globally nonnegative.

          source
          theorem AnalyticNumberTheory.LargeSieve.standardBVCanonicalSmoothing_nonneg (x : ℝ) (_hx : 0 < x) :
          0 ≤ standardBVCanonicalSmoothing x

          The positive-axis form consumed by the existing low Siegel--Walfisz source.

          source
          theorem AnalyticNumberTheory.LargeSieve.standardBVCanonicalSmoothing_support :
          Function.support standardBVCanonicalSmoothing ⊆ Set.Icc (1 / 2) 2

          The canonical smoothing function is supported in [1/2, 2].

          source
          theorem AnalyticNumberTheory.LargeSieve.standardBVCanonicalSmoothing_mass_one :
          ∫ (x : ℝ) in Set.Ioi 0, standardBVCanonicalSmoothing x / x = 1

          The canonical smoothing function has multiplicative mass one.

          source
          theorem AnalyticNumberTheory.LargeSieve.standardBombieriVinogradov_of_rawLandauSiegelLowerBound_canonicalSmoothing (hLandauSiegel : RawLandauSiegelLowerBound) :
          MathlibNt.SieveTheory.BombieriVinogradov.StandardBombieriVinogradov

          A raw Landau--Siegel lower bound supplies Standard Bombieri--Vinogradov with no smoothing function, regularity, support, or mass parameters in the headline.