High-conductor dyadic primitive means

This file keeps the AP weight 1 / φ(d) until the unsquared primitive mean has been converted, by two honest Cauchy--Schwarz steps, to the square-large-sieve weight d / φ(d). In particular the restriction R < d ≤ Q is never erased.

The resulting ledger is deliberately exact: the lower conductor cutoff enters through the harmonic tail ∑_{R<d≤Q} 1/d, not through a fictitious 1/R. Consequently an N/√R (or Q√N) conclusion is produced only from the stated square-ledger strengthening. This module is only a connector and narrow saving consumer: it does not construct, inhabit, or certify any high-source input.

noncomputable def AnalyticNumberTheory.LargeSieve.highConductorPrimitiveMean (R Q : ℕ) (A : (d : ℕ) → PrimitiveCharacter d → ℝ) : ℝ

Literal AP-normalized primitive L¹ mean on the retained conductor block R < d ≤ Q. The amplitudes are nonnegative row maxima in applications.

Equations

• AnalyticNumberTheory.LargeSieve.highConductorPrimitiveMean R Q A = ∑ d ∈ Finset.Ioc R Q, 1 / ↑d.totient * ∑ χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter d, A d χ

noncomputable def AnalyticNumberTheory.LargeSieve.highConductorPrimitiveSquareLedger (R Q : ℕ) (A : (d : ℕ) → PrimitiveCharacter d → ℝ) : ℝ

Literal primitive square-large-sieve ledger on the same conductor block.

Equations

• AnalyticNumberTheory.LargeSieve.highConductorPrimitiveSquareLedger R Q A = ∑ d ∈ Finset.Ioc R Q, ↑d / ↑d.totient * ∑ χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter d, A d χ ^ 2

noncomputable def AnalyticNumberTheory.LargeSieve.highConductorHarmonicTail (R Q : ℕ) : ℝ

The exact modulus-Cauchy factor left by the high-conductor restriction.

Equations

• AnalyticNumberTheory.LargeSieve.highConductorHarmonicTail R Q = ∑ d ∈ Finset.Ioc R Q, 1 / ↑d

theorem AnalyticNumberTheory.LargeSieve.primitiveMeanAt_sq_le_squareLedgerAt {d : ℕ} (hd : 0 < d) (A : PrimitiveCharacter d → ℝ) : (√↑d / ↑d.totient * ∑ χ : PrimitiveCharacter d, A χ) ^ 2 ≤ ↑d / ↑d.totient * ∑ χ : PrimitiveCharacter d, A χ ^ 2

At one positive conductor, character Cauchy converts the square of the AP-normalized L¹ row to the primitive large-sieve weight.

theorem AnalyticNumberTheory.LargeSieve.highConductorPrimitiveMean_sq_le_harmonic_mul_squareLedger (R Q : ℕ) (A : (d : ℕ) → PrimitiveCharacter d → ℝ) : highConductorPrimitiveMean R Q A ^ 2 ≤ highConductorHarmonicTail R Q * highConductorPrimitiveSquareLedger R Q A

Exact high-conductor primitive Cauchy ledger. This is the finite connector used by both Type-I and Type-II rows. It preserves R < d ≤ Q, the unsquared 1/φ(d) weight, and the d/φ(d) square ledger.

theorem AnalyticNumberTheory.LargeSieve.one_div_top_le_highConductorHarmonicTail {R Q : ℕ} (hRQ : R < Q) : 1 / ↑Q ≤ highConductorHarmonicTail R Q

If the high block is nonempty, its genuine Cauchy factor contains the top term 1/Q. This records that the lower cutoff does not turn the harmonic factor into 1/R.

def AnalyticNumberTheory.LargeSieve.highConductorPhysicalSquareMajorant (H C N Q D : ℝ) : ℝ

Schematic square majorant delivered by both physical row arguments after inserting the true coefficient energy: the large-sieve length term times the row/tensor energy is the diagonal N²; the modulus term is kept separately.

Equations

• AnalyticNumberTheory.LargeSieve.highConductorPhysicalSquareMajorant H C N Q D = H * (N ^ 2 + C * Q ^ 2 * N * D)

theorem AnalyticNumberTheory.LargeSieve.diagonal_le_highConductorPhysicalSquareMajorant {H C N Q D : ℝ} (hH : 0 ≤ H) (hC : 0 ≤ C) (hN : 0 ≤ N) (hD : 0 ≤ D) : H * N ^ 2 ≤ highConductorPhysicalSquareMajorant H C N Q D

The genuine coefficient-energy diagonal survives every nonnegative physical square majorant. Restricting conductors after this row estimate cannot remove it.

theorem AnalyticNumberTheory.LargeSieve.highConductorPhysicalSquareMajorant_not_le_of_target_lt_diagonal {H C N Q D target : ℝ} (hH : 0 ≤ H) (hC : 0 ≤ C) (hN : 0 ≤ N) (hD : 0 ≤ D) (htarget : target < H * N ^ 2) : ¬highConductorPhysicalSquareMajorant H C N Q D ≤ target

Formal non-payment certificate: whenever a desired squared budget lies strictly below the surviving H N² diagonal, the available physical majorant cannot imply that budget, regardless of the modulus-dependent row.

def AnalyticNumberTheory.LargeSieve.HighConductorTypeISquareSaving (R Q N : ℕ) (K : ℝ) (A : (d : ℕ) → PrimitiveCharacter d → ℝ) : Prop

The narrow square-ledger strengthening that really yields an N/√R Type-I scale. It is intentionally a statement about coefficient energy after large sieve, not a renamed bound on the unsquared high mean.

Equations

• AnalyticNumberTheory.LargeSieve.HighConductorTypeISquareSaving R Q N K A = (AnalyticNumberTheory.LargeSieve.highConductorHarmonicTail R Q * AnalyticNumberTheory.LargeSieve.highConductorPrimitiveSquareLedger R Q A ≤ (K * ↑N / √↑R) ^ 2)

def AnalyticNumberTheory.LargeSieve.HighConductorTypeIISquareSaving (R Q N : ℕ) (K : ℝ) (A : (d : ℕ) → PrimitiveCharacter d → ℝ) : Prop

The parallel strengthening giving a Q√N Type-II scale.

Equations

• AnalyticNumberTheory.LargeSieve.HighConductorTypeIISquareSaving R Q N K A = (AnalyticNumberTheory.LargeSieve.highConductorHarmonicTail R Q * AnalyticNumberTheory.LargeSieve.highConductorPrimitiveSquareLedger R Q A ≤ (K * ↑Q * √↑N) ^ 2)

theorem AnalyticNumberTheory.LargeSieve.highConductorTypeI_le {R Q N : ℕ} {K : ℝ} (A : (d : ℕ) → PrimitiveCharacter d → ℝ) (hA : ∀ (d : ℕ) (χ : PrimitiveCharacter d), 0 ≤ A d χ) (hK : 0 ≤ K) (h : HighConductorTypeISquareSaving R Q N K A) : highConductorPrimitiveMean R Q A ≤ K * ↑N / √↑R

Actual Type-I row maxima reach the N/√R scale once their retained high-conductor square ledger has the preceding saving.

theorem AnalyticNumberTheory.LargeSieve.highConductorTypeII_le {R Q N : ℕ} {K : ℝ} (A : (d : ℕ) → PrimitiveCharacter d → ℝ) (hA : ∀ (d : ℕ) (χ : PrimitiveCharacter d), 0 ≤ A d χ) (hK : 0 ≤ K) (h : HighConductorTypeIISquareSaving R Q N K A) : highConductorPrimitiveMean R Q A ≤ K * ↑Q * √↑N

Actual Type-II row maxima reach the Q√N scale once their retained high-conductor square ledger has the parallel saving.

theorem AnalyticNumberTheory.LargeSieve.highConductorHybrid_of_typeI_typeII_squareLedgers {R Q N : ℕ} {KI KII : ℝ} (typeIRow typeIIRow : (d : ℕ) → PrimitiveCharacter d → ℝ) (hI0 : ∀ (d : ℕ) (χ : PrimitiveCharacter d), 0 ≤ typeIRow d χ) (hII0 : ∀ (d : ℕ) (χ : PrimitiveCharacter d), 0 ≤ typeIIRow d χ) (hKI : 0 ≤ KI) (hKII : 0 ≤ KII) (hI : HighConductorTypeISquareSaving R Q N KI typeIRow) (hII : HighConductorTypeIISquareSaving R Q N KII typeIIRow) : (highConductorPrimitiveMean R Q fun (d : ℕ) (χ : PrimitiveCharacter d) => typeIRow d χ + typeIIRow d χ) ≤ KI * ↑N / √↑R + KII * ↑Q * √↑N

A narrow conditional consumer combining two nonnegative rows. It assumes the two retained square-ledger savings explicitly; in particular it does not construct or inhabit a high-source input.