Unconditional chosen Standard-BV high-conductor source

This checker constructs the genuine chosen high-conductor source with explicit parameters.

def AnalyticNumberTheory.LargeSieve.standardBVHighChosenUnconditionalTypeIIExponent (A : ℕ) : ℕ

Explicit Pan exponent for the chosen all-aspect Type-II payment.

Equations

• AnalyticNumberTheory.LargeSieve.standardBVHighChosenUnconditionalTypeIIExponent A = 3 * A + 200

def AnalyticNumberTheory.LargeSieve.standardBVHighChosenUnconditionalTypeIIConductorExponent (A : ℕ) : ℕ

Explicit conductor exponent for the chosen all-aspect Type-II payment.

Equations

• AnalyticNumberTheory.LargeSieve.standardBVHighChosenUnconditionalTypeIIConductorExponent A = 2 * (A + 50)

noncomputable def AnalyticNumberTheory.LargeSieve.standardBVHighChosenUnconditionalTypeIICutoff (A N : ℕ) : ℕ

Both Vaughan cutoffs are the literal logarithmic conductor threshold.

Equations

• AnalyticNumberTheory.LargeSieve.standardBVHighChosenUnconditionalTypeIICutoff A N = AnalyticNumberTheory.LargeSieve.logConductorThreshold N (AnalyticNumberTheory.LargeSieve.standardBVHighChosenUnconditionalTypeIIConductorExponent A)

theorem AnalyticNumberTheory.LargeSieve.standardBVHighChosenUnconditionalTypeII_activeCard_le (A N : ℕ) : (vaughanTypeIIActiveCanonicalRectangles N (standardBVHighChosenUnconditionalTypeIICutoff A N) (standardBVHighChosenUnconditionalTypeIICutoff A N)).card ≤ (N.log2 + 1) ^ 2

The concrete active rectangle family has the advertised squared binary-log cardinality budget.

theorem AnalyticNumberTheory.LargeSieve.standardBVHighChosenUnconditional_typeII (A : ℕ) : have B := 3 * A + 200; have C := 2 * (A + 50); have u := fun (N : ℕ) => logConductorThreshold N C; have v := fun (N : ℕ) => logConductorThreshold N C; ∃ (K : ℝ), 0 < K ∧ ∀ᶠ (N : ℕ) in Filter.atTop, have Q := MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N ↑B; 4 * discreteAbelAmplifierPrefixMax N * conductorHarmonicFactor Q ^ 2 * highConductorVaughanTypeIIMean N Q C (u N) (v N) ≤ K * ↑N / Real.log ↑N ^ A

Unconditional closure of exactly the chosen-parameter Type-II high-conductor contribution.

theorem AnalyticNumberTheory.LargeSieve.standardBVHighChosenUnconditional_typeI (A : ℕ) : have B := 3 * A + 200; have C := 2 * (A + 50); have u := fun (N : ℕ) => logConductorThreshold N C; have v := fun (N : ℕ) => logConductorThreshold N C; ∃ (K : ℝ), 0 < K ∧ ∀ᶠ (N : ℕ) in Filter.atTop, have Q := MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N ↑B; 4 * discreteAbelAmplifierPrefixMax N * conductorHarmonicFactor Q ^ 2 * highConductorVaughanTypeIMean N Q C (u N) (v N) ≤ K * ↑N / Real.log ↑N ^ A

The elementary finite-complex-Cauchy Type-I estimate is payable at the same explicit cutoff. No row-triangle theorem is used here.

theorem AnalyticNumberTheory.LargeSieve.standardBVHighChosenUnconditional_cutoff_le_balanced_eventually (A : ℕ) : ∀ᶠ (N : ℕ) in Filter.atTop, logConductorThreshold N (2 * (A + 50)) ≤ standardBVBalancedSmallCutoff N

theorem AnalyticNumberTheory.LargeSieve.standardBVHighChosenUnconditional_small (A : ℕ) : have B := 3 * A + 200; have C := 2 * (A + 50); have v := fun (N : ℕ) => logConductorThreshold N C; ∃ (K : ℝ), 0 < K ∧ ∀ᶠ (N : ℕ) in Filter.atTop, have Q := MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N ↑B; have P := 4 * discreteAbelAmplifierPrefixMax N * conductorHarmonicFactor Q ^ 2; P * highConductorVaughanSmallMean N Q C (v N) ≤ K * ↑N / Real.log ↑N ^ A

Unconditional closure of exactly the small Vaughan lane at the chosen parameters B=3*A+200, C=2*(A+50), and v(N)=logConductorThreshold N C.

theorem AnalyticNumberTheory.LargeSieve.standardBVHighChosenUnconditional : StandardBVHighTypeITypeIIHybridChosenSource

Unconditional inhabitant of the genuine chosen high-conductor source. The shared pair is u(N)=v(N)=logConductorThreshold N (2*(A+50)).