Exact finite Selberg optimization for Liu's source modulus

Liu's lemma lm-selberg states the existence of coefficients with main term [8 + O(ε)] 𝔖(N) / log N; it does not prove the finite minimization in the form needed by this development. This file performs that minimization exactly. After it, the genuinely analytic missing statement is precisely the eventual, uniform weighted Mertens--Selberg lower bound for ∑_{l ∣ Q, l ≤ R} ∏_{p ∣ l} 1 / (p - 2).

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuSelbergTerm (l : ℕ) : ℝ

The positive local Selberg factor attached to a source divisor.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuSelbergTerm l = ∏ p ∈ l.primeFactors, (↑p - 2)⁻¹

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuSelbergDenominator (N : ℕ) (epsilon : ℝ) : ℝ

Liu's truncated Selberg denominator. It has no proof argument.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuSelbergDenominator N epsilon = ∑ l ∈ MathlibNt.SieveTheory.LiuWeight.liuSelbergLambdaSourceCarrier N epsilon, MathlibNt.SieveTheory.LiuWeight.liuSelbergTerm l

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergTerm_eq_selbergTerms {N l : ℕ} {epsilon : ℝ} (hNeven : Even N) (hl : l ∣ liuPaperQModulus N epsilon) : liuSelbergTerm l = BoundingSieve.selbergTerms l

On the even source modulus, the explicit local factor is Mathlib's BoundingSieve.selbergTerms.

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergTerm_pos {N l : ℕ} {epsilon : ℝ} (hNeven : Even N) (hl : l ∈ liuSelbergLambdaSourceCarrier N epsilon) : 0 < liuSelbergTerm l

Every explicit Selberg term on the source carrier is positive.

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergDenominator_pos {N : ℕ} {epsilon : ℝ} (hNeven : Even N) (hR : 1 ≤ paperQSourceCutoff N epsilon) : 0 < liuSelbergDenominator N epsilon

The denominator is positive once the truncation contains 1.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuSelbergOptimalX (N : ℕ) (epsilon : ℝ) (l : ℕ) : ℝ

The prescribed diagonal coordinate, extended by zero off the truncation.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuSelbergOptimalX N epsilon l = if l ∈ MathlibNt.SieveTheory.LiuWeight.liuSelbergLambdaSourceCarrier N epsilon then ↑(ArithmeticFunction.moebius l) * MathlibNt.SieveTheory.LiuWeight.liuSelbergTerm l / MathlibNt.SieveTheory.LiuWeight.liuSelbergDenominator N epsilon else 0

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuSelbergOptimalLambda (N : ℕ) (epsilon : ℝ) (d : ℕ) : ℝ

Reverse-divisor Möbius inversion of the optimal diagonal coordinates.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuSelbergOptimalLambda N epsilon d = if d ∈ MathlibNt.SieveTheory.LiuWeight.liuSelbergLambdaSourceCarrier N epsilon then (∑ e ∈ MathlibNt.SieveTheory.LiuWeight.liuSelbergLambdaSourceCarrier N epsilon, if d ∣ e then ↑(ArithmeticFunction.moebius (e / d)) * MathlibNt.SieveTheory.LiuWeight.liuSelbergOptimalX N epsilon e else 0) / MathlibNt.SieveTheory.LiuWeight.liuSelbergReciprocalTotient d else 0

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergOptimalLambda_eq_zero_of_not_mem {N d : ℕ} {epsilon : ℝ} (hd : d ∉ liuSelbergLambdaSourceCarrier N epsilon) : liuSelbergOptimalLambda N epsilon d = 0

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergOptimalLambda_support {N d : ℕ} {epsilon : ℝ} (hd : liuSelbergOptimalLambda N epsilon d ≠ 0) : d ∣ liuPaperQModulus N epsilon ∧ d ≤ paperQSourceCutoff N epsilon

The explicit optimizer is supported on divisors of the source modulus below the source cutoff.

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergOptimalX_eq_sum_nu_mul_lambda {N l : ℕ} {epsilon : ℝ} (hNeven : Even N) (hl : l ∈ liuSelbergLambdaSourceCarrier N epsilon) : liuSelbergOptimalX N epsilon l = ∑ d ∈ (liuPaperQModulus N epsilon).divisors, if l ∣ d then (liuSelbergBoundingSieve N epsilon hNeven).nu d * liuSelbergOptimalLambda N epsilon d else 0

Reverse-divisor inversion recovers every diagonal coordinate on the truncated carrier.

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergOptimalLambda_one {N : ℕ} {epsilon : ℝ} (hNeven : Even N) (hR : 1 ≤ paperQSourceCutoff N epsilon) : liuSelbergOptimalLambda N epsilon 1 = 1

The reverse-divisor construction is normalized at 1.

theorem MathlibNt.SieveTheory.LiuWeight.sum_nu_mul_liuSelbergOptimalLambda_eq_optimalX {N l : ℕ} {epsilon : ℝ} (hNeven : Even N) (hlQ : l ∣ liuPaperQModulus N epsilon) : (∑ d ∈ (liuPaperQModulus N epsilon).divisors, if l ∣ d then (liuSelbergBoundingSieve N epsilon hNeven).nu d * liuSelbergOptimalLambda N epsilon d else 0) = liuSelbergOptimalX N epsilon l

The diagonal coordinate identity also holds off the truncation: both sides vanish there.

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergCoefficientFactor_optimalLambda {N : ℕ} {epsilon : ℝ} (hNeven : Even N) (hR : 1 ≤ paperQSourceCutoff N epsilon) : liuSelbergCoefficientFactor N epsilon (liuSelbergOptimalLambda N epsilon) = 1 / liuSelbergDenominator N epsilon

Exact finite Selberg minimization: the source quadratic coefficient of the explicit optimizer is the reciprocal truncated denominator.

theorem MathlibNt.SieveTheory.LiuWeight.abs_liuSelbergOptimalLambda_le_one {N d : ℕ} {epsilon : ℝ} (hNeven : Even N) (hR : 1 ≤ paperQSourceCutoff N epsilon) : |liuSelbergOptimalLambda N epsilon d| ≤ 1

Every finite optimal coefficient has the classical Selberg bound.

def MathlibNt.SieveTheory.LiuWeight.truncatedSelbergCarrier (S : BoundingSieve) (R : ℕ) : Finset ℕ

Divisors of the sieve product retained by a finite Selberg cutoff.

Equations

• MathlibNt.SieveTheory.LiuWeight.truncatedSelbergCarrier S R = {d ∈ S.prodPrimes.divisors | d ≤ R}

noncomputable def MathlibNt.SieveTheory.LiuWeight.truncatedSelbergDenominator (S : BoundingSieve) (R : ℕ) : ℝ

The finite Selberg denominator for an arbitrary bounding sieve and cutoff.

Equations

• MathlibNt.SieveTheory.LiuWeight.truncatedSelbergDenominator S R = ∑ d ∈ MathlibNt.SieveTheory.LiuWeight.truncatedSelbergCarrier S R, BoundingSieve.selbergTerms d

noncomputable def MathlibNt.SieveTheory.LiuWeight.truncatedSelbergOptimalX (S : BoundingSieve) (R l : ℕ) : ℝ

The diagonal coordinates of the finite truncated Selberg optimizer.

Equations

• MathlibNt.SieveTheory.LiuWeight.truncatedSelbergOptimalX S R l = if l ∈ MathlibNt.SieveTheory.LiuWeight.truncatedSelbergCarrier S R then ↑(ArithmeticFunction.moebius l) * BoundingSieve.selbergTerms l / MathlibNt.SieveTheory.LiuWeight.truncatedSelbergDenominator S R else 0

noncomputable def MathlibNt.SieveTheory.LiuWeight.truncatedSelbergOptimalLambda (S : BoundingSieve) (R d : ℕ) : ℝ

Reverse-divisor Möbius inversion of the truncated optimal diagonal coordinates.

Equations

• MathlibNt.SieveTheory.LiuWeight.truncatedSelbergOptimalLambda S R d = if d ∈ MathlibNt.SieveTheory.LiuWeight.truncatedSelbergCarrier S R then (∑ e ∈ MathlibNt.SieveTheory.LiuWeight.truncatedSelbergCarrier S R, if d ∣ e then ↑(ArithmeticFunction.moebius (e / d)) * MathlibNt.SieveTheory.LiuWeight.truncatedSelbergOptimalX S R e else 0) / S.nu d else 0

theorem MathlibNt.SieveTheory.LiuWeight.truncatedSelbergDenominator_pos (S : BoundingSieve) {R : ℕ} (hR : 1 ≤ R) : 0 < truncatedSelbergDenominator S R

theorem MathlibNt.SieveTheory.LiuWeight.truncatedSelbergOptimalLambda_eq_zero_of_not_mem {S : BoundingSieve} {R d : ℕ} (hd : d ∉ truncatedSelbergCarrier S R) : truncatedSelbergOptimalLambda S R d = 0

theorem MathlibNt.SieveTheory.LiuWeight.truncatedSelbergOptimalLambda_support {S : BoundingSieve} {R d : ℕ} (hd : truncatedSelbergOptimalLambda S R d ≠ 0) : d ∣ S.prodPrimes ∧ d ≤ R

The finite optimizer is supported on divisors of the sieve product below its cutoff.

theorem MathlibNt.SieveTheory.LiuWeight.truncatedSelbergOptimalLambda_one (S : BoundingSieve) {R : ℕ} (hR : 1 ≤ R) : truncatedSelbergOptimalLambda S R 1 = 1

The reverse-divisor construction is normalized at one.

theorem MathlibNt.SieveTheory.LiuWeight.mainSum_truncatedSelbergOptimalLambda (S : BoundingSieve) {R : ℕ} (hR : 1 ≤ R) : BoundingSieve.mainSum (BoundingSieve.lambdaSquared (truncatedSelbergOptimalLambda S R)) = 1 / truncatedSelbergDenominator S R

Exact finite Selberg minimization for a cutoff-supported optimizer.

theorem MathlibNt.SieveTheory.LiuWeight.one_div_truncatedSelbergDenominator_le_mainSum (S : BoundingSieve) {R : ℕ} (w : ℕ → ℝ) (hw_one : w 1 = 1) (hw_support : ∀ {d : ℕ}, w d ≠ 0 → d ∈ truncatedSelbergCarrier S R) : 1 / truncatedSelbergDenominator S R ≤ BoundingSieve.mainSum (BoundingSieve.lambdaSquared w)

The reciprocal truncated Selberg denominator is a lower bound for every normalized weight supported on the truncated carrier.

theorem MathlibNt.SieveTheory.LiuWeight.mainSum_truncatedSelbergOptimalLambda_le_mainSum (S : BoundingSieve) {R : ℕ} (hR : 1 ≤ R) (w : ℕ → ℝ) (hw_one : w 1 = 1) (hw_support : ∀ {d : ℕ}, w d ≠ 0 → d ∈ truncatedSelbergCarrier S R) : BoundingSieve.mainSum (BoundingSieve.lambdaSquared (truncatedSelbergOptimalLambda S R)) ≤ BoundingSieve.mainSum (BoundingSieve.lambdaSquared w)

The truncated Selberg optimizer minimizes the main sum among all normalized weights supported on the same carrier.

theorem MathlibNt.SieveTheory.LiuWeight.abs_truncatedSelbergOptimalLambda_le_one (S : BoundingSieve) {R d : ℕ} (hR : 1 ≤ R) : |truncatedSelbergOptimalLambda S R d| ≤ 1

Every cutoff-supported finite optimal coefficient has the Selberg bound.

def MathlibNt.SieveTheory.LiuWeight.LiuSelbergDenominatorLowerBound (delta epsilon : ℝ) : Prop

The sole analytic statement left by the finite minimization: uniformly for large N, the truncated weighted divisor sum dominates the sharp reciprocal scale. This is a lower bound on G, not the desired coefficient conclusion.

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuSelbergDenominatorLowerBound delta epsilon = ∀ᶠ (N : ℕ) in Filter.atTop, 2 ≤ N → Even N → 1 ≤ MathlibNt.SieveTheory.LiuWeight.paperQSourceCutoff N epsilon → Real.log ↑N / ((8 + delta) * MathlibNt.SieveTheory.SingularSeries.liuSingularSeries N) ≤ MathlibNt.SieveTheory.LiuWeight.liuSelbergDenominator N epsilon

theorem MathlibNt.SieveTheory.LiuWeight.one_div_liuSelbergDenominator_le {delta epsilon : ℝ} {N : ℕ} (hdelta : 0 < 8 + delta) (hN : 2 ≤ N) (hNeven : Even N) (hR : 1 ≤ paperQSourceCutoff N epsilon) (hden : Real.log ↑N / ((8 + delta) * SingularSeries.liuSingularSeries N) ≤ liuSelbergDenominator N epsilon) : 1 / liuSelbergDenominator N epsilon ≤ (8 + delta) * SingularSeries.liuSingularSeries N / Real.log ↑N

theorem MathlibNt.SieveTheory.LiuWeight.LegacySelberg.LiuOptimizedSelbergCoefficientEstimate.of_denominatorLowerBound {delta epsilon : ℝ} (hdelta : 0 < 8 + delta) (hden : LiuSelbergDenominatorLowerBound delta epsilon) : LiuOptimizedSelbergCoefficientEstimate delta epsilon

theorem MathlibNt.SieveTheory.LiuWeight.LegacySelberg.LiuOptimizedSelbergCoefficientInput.of_denominatorLowerBound (hden : ∀ delta > 0, ∃ epsilon0 > 0, ∀ (epsilon : ℝ), 0 < epsilon → epsilon ≤ epsilon0 → LiuSelbergDenominatorLowerBound delta epsilon) : LiuOptimizedSelbergCoefficientInput