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.

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

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

Equations

• AnalyticNumberTheory.LargeSieve.standardBVCanonicalBaseBump = { rIn := 1 / 4, rOut := 3 / 4, rIn_pos := AnalyticNumberTheory.LargeSieve.standardBVCanonicalBaseBump._proof_4, rIn_lt_rOut := AnalyticNumberTheory.LargeSieve.standardBVCanonicalBaseBump._proof_5 }

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

• AnalyticNumberTheory.LargeSieve.standardBVCanonicalWeight x = ↑AnalyticNumberTheory.LargeSieve.standardBVCanonicalBaseBump x / max x (1 / 2)

noncomputable def AnalyticNumberTheory.LargeSieve.standardBVCanonicalWeightMass : ℝ

The finite, strictly positive normalizing denominator.

Equations

• AnalyticNumberTheory.LargeSieve.standardBVCanonicalWeightMass = ∫ (x : ℝ), AnalyticNumberTheory.LargeSieve.standardBVCanonicalWeight x

theorem AnalyticNumberTheory.LargeSieve.standardBVCanonicalWeight_continuous : Continuous standardBVCanonicalWeight

theorem AnalyticNumberTheory.LargeSieve.standardBVCanonicalWeight_hasCompactSupport : HasCompactSupport standardBVCanonicalWeight

theorem AnalyticNumberTheory.LargeSieve.standardBVCanonicalWeight_integrable : MeasureTheory.Integrable standardBVCanonicalWeight MeasureTheory.volume

theorem AnalyticNumberTheory.LargeSieve.standardBVCanonicalWeight_nonneg : 0 ≤ standardBVCanonicalWeight

theorem AnalyticNumberTheory.LargeSieve.standardBVCanonicalWeightMass_pos : 0 < standardBVCanonicalWeightMass

The normalization denominator is positive (and hence nonzero).

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

The canonical smoothing function, normalized for dx/x.

Equations

• AnalyticNumberTheory.LargeSieve.standardBVCanonicalSmoothing x = ↑AnalyticNumberTheory.LargeSieve.standardBVCanonicalBaseBump x / AnalyticNumberTheory.LargeSieve.standardBVCanonicalWeightMass

theorem AnalyticNumberTheory.LargeSieve.standardBVCanonicalSmoothing_contDiff : ContDiff ℝ 1 standardBVCanonicalSmoothing

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

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

The canonical smoothing function is globally nonnegative.

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

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

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

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

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

The canonical smoothing function has multiplicative mass one.

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.