Standard BV: exact dyadic square-mean to L¹ conversion

This module isolates the finite conversion which is needed before any Bombieri--Vinogradov conclusion may be claimed. The AP prefix error is supplied pointwise through the character expansion, not as a final BV premise. Every factor 1/φ(q), q/φ(q), the number of moduli in a block, and the number of conductor cells is retained.

The character quantity is a genuine prefix maximum. Nothing in this file replaces it by the endpoint y = N.

noncomputable def AnalyticNumberTheory.LargeSieve.weightedNonprincipalPrefixSquare (b : ℤ → ℂ) (N : ℕ) (S : Finset ℕ) : ℝ

The square ledger on a chosen set of levels, with the exact q / φ(q) weight used by the primitive large sieve.

Equations

• AnalyticNumberTheory.LargeSieve.weightedNonprincipalPrefixSquare b N S = ∑ q ∈ S, ↑q / ↑q.totient * ∑ χ ∈ AnalyticNumberTheory.LargeSieve.nonprincipalCharacters q, AnalyticNumberTheory.LargeSieve.characterPrefixMaxSquare χ b 0 N

noncomputable def AnalyticNumberTheory.LargeSieve.nonprincipalPrefixAmplitude (b : ℤ → ℂ) (N q : ℕ) (χ : DirichletCharacter ℂ q) : ℝ

The nonnegative amplitude whose square is the full character prefix maximum.

Equations

• AnalyticNumberTheory.LargeSieve.nonprincipalPrefixAmplitude b N q χ = √(AnalyticNumberTheory.LargeSieve.characterPrefixMaxSquare χ b 0 N)

theorem AnalyticNumberTheory.LargeSieve.nonprincipalPrefixAmplitude_nonneg (b : ℤ → ℂ) (N q : ℕ) (χ : DirichletCharacter ℂ q) : 0 ≤ nonprincipalPrefixAmplitude b N q χ

theorem AnalyticNumberTheory.LargeSieve.nonprincipalPrefixAmplitude_sq (b : ℤ → ℂ) (N q : ℕ) (χ : DirichletCharacter ℂ q) : nonprincipalPrefixAmplitude b N q χ ^ 2 = characterPrefixMaxSquare χ b 0 N

theorem AnalyticNumberTheory.LargeSieve.card_nonprincipalCharacters_le_totient {q : ℕ} (hq : 0 < q) : (nonprincipalCharacters q).card ≤ q.totient

There are at most φ(q) nonprincipal characters. This is kept as a separate public bookkeeping lemma because it is exactly what turns 1/φ(q)^2 after Cauchy into 1/φ(q).

theorem AnalyticNumberTheory.LargeSieve.one_modulus_character_cauchy (b : ℤ → ℂ) (N q : ℕ) (E : ℝ) (hq : 0 < q) (hE0 : 0 ≤ E) (hchar : E ≤ (↑q.totient)⁻¹ * ∑ χ ∈ nonprincipalCharacters q, nonprincipalPrefixAmplitude b N q χ) : ↑q * E ^ 2 ≤ ↑q / ↑q.totient * ∑ χ ∈ nonprincipalCharacters q, characterPrefixMaxSquare χ b 0 N

Character Cauchy at one level. Starting from the literal AP majorant E(q) ≤ φ(q)⁻¹ ∑_{χ≠χ₀} M(q,χ), the result is written with the large-sieve weight q/φ(q): no totient weight is discarded.

theorem AnalyticNumberTheory.LargeSieve.modulus_block_square_to_L1 (b : ℤ → ℂ) (N R : ℕ) (S : Finset ℕ) (E : ℕ → ℝ) (hR : 0 < R) (hlevels : ∀ q ∈ S, R ≤ q) (hE0 : ∀ q ∈ S, 0 ≤ E q) (hchar : ∀ q ∈ S, E q ≤ (↑q.totient)⁻¹ * ∑ χ ∈ nonprincipalCharacters q, nonprincipalPrefixAmplitude b N q χ) : ↑R * (∑ q ∈ S, E q) ^ 2 ≤ ↑S.card * weightedNonprincipalPrefixSquare b N S

Exact Cauchy conversion on an arbitrary modulus block. If every modulus in S is at least R, then

R (∑ E_q)^2 ≤ #S · ∑ (q/φ(q))∑χ M(q,χ)^2.

Thus the cardinality is not silently replaced by R; that optional estimate is a later, separate step.

theorem AnalyticNumberTheory.LargeSieve.modulus_block_square_threshold (b : ℤ → ℂ) (N R : ℕ) (S : Finset ℕ) (E : ℕ → ℝ) (T : ℝ) (hR : 0 < R) (hT : 0 ≤ T) (hlevels : ∀ q ∈ S, R ≤ q) (hE0 : ∀ q ∈ S, 0 ≤ E q) (hchar : ∀ q ∈ S, E q ≤ (↑q.totient)⁻¹ * ∑ χ ∈ nonprincipalCharacters q, nonprincipalPrefixAmplitude b N q χ) (hthreshold : ↑S.card * weightedNonprincipalPrefixSquare b N S ≤ ↑R * T ^ 2) : ∑ q ∈ S, E q ≤ T

The exact sufficient square-mean threshold on one modulus block. In quotient notation it is

weighted square ≤ (R / #S) T².

The cross-multiplied statement remains meaningful for an empty block and contains no hidden division by its cardinality.

theorem AnalyticNumberTheory.LargeSieve.conductor_cells_supply_block_threshold {ι : Type u_1} (J : Finset ι) (W : ι → ℝ) (qCard R : ℕ) (T : ℝ) (hJ : J.Nonempty) (_hW0 : ∀ j ∈ J, 0 ≤ W j) (hcell : ∀ j ∈ J, ↑qCard * ↑J.card * W j ≤ ↑R * T ^ 2) : ↑qCard * ∑ j ∈ J, W j ≤ ↑R * T ^ 2

If a conductor regrouping splits the square ledger into J.card cells, this is the exact per-cell threshold. The conductor-block cardinality is visible: no cell may merely be bounded by the whole one-block budget.

theorem AnalyticNumberTheory.LargeSieve.sum_dyadic_blocks_to_L1 {ι : Type u_1} (I : Finset ι) (blockSum T : ι → ℝ) (target : ℝ) (hblock : ∀ i ∈ I, blockSum i ≤ T i) (hbudget : ∑ i ∈ I, T i ≤ target) : ∑ i ∈ I, blockSum i ≤ target

Exact allocation across dyadic modulus blocks. A block budget T i is proved from its own square threshold; summing the allocations gives the final L¹ target. Taking all T i = N/(L log(N)^A) displays the familiar extra L² in the required square mean.

noncomputable def AnalyticNumberTheory.LargeSieve.standardBVBlockSquareThreshold (N logN A R m L : ℝ) : ℝ

Exact equal-allocation square threshold. L is the number of dyadic modulus blocks, m the number of actual moduli in the present block, and R its lower endpoint.

Equations

• AnalyticNumberTheory.LargeSieve.standardBVBlockSquareThreshold N logN A R m L = R / m * (N / (L * logN ^ A)) ^ 2

theorem AnalyticNumberTheory.LargeSieve.standardBVBlockSquareThreshold_crossmul (N logN A R m L : ℝ) (hm : 0 < m) : m * standardBVBlockSquareThreshold N logN A R m L = R * (N / (L * logN ^ A)) ^ 2

Cross-multiplied form of the preceding threshold; this is the form consumed by modulus_block_square_threshold.

Substitution ledger for the currently proved producers

These are transparent scale expressions, not hypotheses asserting BV. Their factorizations identify exactly which payments must be compared with the preceding threshold.

noncomputable def AnalyticNumberTheory.LargeSieve.existingTypeIPrefixWindowScale (N Q C B : ℕ) : ℝ

Current unconditional collected Type-I prefix scale on conductor window C ≤ d ≤ 2C. It pays the linear conductor transport (Q/C) H(Q/C), RM log₂(N)^2, the full (N+C² log C) large-sieve factor, and the proved 108 B² N log(N)^5 coefficient moment.

Equations

• AnalyticNumberTheory.LargeSieve.existingTypeIPrefixWindowScale N Q C B = ↑(Q / C) * AnalyticNumberTheory.LargeSieve.conductorHarmonicFactor (Q / C) * ↑(N.log2 + 1) ^ 2 * AnalyticNumberTheory.LargeSieve.primitiveLargeSieveConstant N (2 * C) * (108 * ↑B ^ 2 * ↑N * Real.log ↑(N + 1) ^ 5)

noncomputable def AnalyticNumberTheory.LargeSieve.existingTypeIIShortPrefixWindowScale (N Q C k B : ℕ) : ℝ

Current short-length Type-II prefix scale on conductor window C and outer shell 2^k. Unlike the obsolete endpoint route, this retains the prefix maximum and cancels 2^k · (N/2^k) in the length charge. The currently proved tensor moment still contributes 27 B² N log(N)^5.

Equations

• AnalyticNumberTheory.LargeSieve.existingTypeIIShortPrefixWindowScale N Q C k B = ↑(Q / C) * AnalyticNumberTheory.LargeSieve.conductorHarmonicFactor (Q / C) * ↑((AnalyticNumberTheory.LargeSieve.vaughanCanonicalTensorLength N k).log2 + 1) ^ 2 * (↑N + ↑(2 ^ k) * ((2 * ↑⌈Real.log (↑(2 * C) ^ 2) / Real.log 2⌉₊ + 12) * ↑(2 * C) ^ 2)) * (27 * ↑B ^ 2 * ↑N * Real.log ↑(N + 1) ^ 5)

noncomputable def AnalyticNumberTheory.LargeSieve.squareThresholdDeficitRatio (scale N logN A R qCard blockCount : ℝ) : ℝ

Ratio to the exact one-block threshold. A ratio at most one is sufficient; a ratio larger than one measures the missing factor without suppressing any Q/C, harmonic, RM, or block-cardinality payment.

Equations

• AnalyticNumberTheory.LargeSieve.squareThresholdDeficitRatio scale N logN A R qCard blockCount = qCard * scale / (R * (N / (blockCount * logN ^ A)) ^ 2)

noncomputable def AnalyticNumberTheory.LargeSieve.lambdaCorrectionThresholdRatio (N Q A R qCard blockCount : ℕ) : ℝ

The Λ change-level correction ratio, with its proved Q² polylog² scale inserted literally.

Equations

• AnalyticNumberTheory.LargeSieve.lambdaCorrectionThresholdRatio N Q A R qCard blockCount = AnalyticNumberTheory.LargeSieve.squareThresholdDeficitRatio (AnalyticNumberTheory.LargeSieve.vaughanLambdaConductorCorrectionScale N Q) (↑N) (Real.log ↑(N + 1)) ↑A ↑R ↑qCard ↑blockCount

noncomputable def AnalyticNumberTheory.LargeSieve.typeIThresholdRatio (N Q C B A R qCard blockCount : ℕ) : ℝ

Type-I ratio after literal substitution of the existing producer.

Equations

• AnalyticNumberTheory.LargeSieve.typeIThresholdRatio N Q C B A R qCard blockCount = AnalyticNumberTheory.LargeSieve.squareThresholdDeficitRatio (AnalyticNumberTheory.LargeSieve.existingTypeIPrefixWindowScale N Q C B) (↑N) (Real.log ↑(N + 1)) ↑A ↑R ↑qCard ↑blockCount

noncomputable def AnalyticNumberTheory.LargeSieve.typeIIThresholdRatio (N Q C k B A R qCard blockCount : ℕ) : ℝ

Type-II ratio after literal substitution of the genuine short-prefix producer.

Equations

• AnalyticNumberTheory.LargeSieve.typeIIThresholdRatio N Q C k B A R qCard blockCount = AnalyticNumberTheory.LargeSieve.squareThresholdDeficitRatio (AnalyticNumberTheory.LargeSieve.existingTypeIIShortPrefixWindowScale N Q C k B) (↑N) (Real.log ↑(N + 1)) ↑A ↑R ↑qCard ↑blockCount

theorem AnalyticNumberTheory.LargeSieve.existingTypeIPrefixWindowScale_has_N_sq_log5 (N Q C B : ℕ) (hN : 0 < N) : ↑(Q / C) * conductorHarmonicFactor (Q / C) * (108 * ↑B ^ 2 * ↑N ^ 2 * Real.log ↑(N + 1) ^ 5) ≤ existingTypeIPrefixWindowScale N Q C B

The current Type-I scale contains an unavoidable displayed N² log^5 subscale before RM and the remaining large-sieve logarithm are counted. This is a lower bound on the produced majorant, not on the true character sum.

theorem AnalyticNumberTheory.LargeSieve.existingTypeIIShortPrefixWindowScale_has_length_payment (N Q C k B : ℕ) : ↑(Q / C) * conductorHarmonicFactor (Q / C) * ↑((vaughanCanonicalTensorLength N k).log2 + 1) ^ 2 * (27 * ↑B ^ 2 * ↑N ^ 2 * Real.log ↑(N + 1) ^ 5) ≤ existingTypeIIShortPrefixWindowScale N Q C k B

The Type-II short-prefix producer still pays the linear conductor factor Q/C, its harmonic factor, and the complete tensor N log^5 moment. Its length term alone is therefore the displayed N² log^5 quantity times those weights and the RM factor.