Actual dyadic partition for the AP-normalized Vaughan Type-I mean

def AnalyticNumberTheory.LargeSieve.vaughanTypeIFirstDyadicShell (u k : ℕ) : Finset ℕ

Dyadic first-lane shell: positive d ≤ u with log₂ d = k.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanTypeIFirstDyadicShell u k = {d ∈ Finset.Icc 1 u | d.log2 = k}

def AnalyticNumberTheory.LargeSieve.vaughanTypeIMiddleProductDyadicShell (u v k : ℕ) : Finset (ℕ × ℕ)

Dyadic product shell in the middle lane. It partitions by the actual short product d*e, rather than by an ambient rectangle.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanTypeIMiddleProductDyadicShell u v k = {de ∈ Finset.Icc 1 u ×ˢ Finset.Icc 1 v | (de.1 * de.2).log2 = k}

@[simp]

theorem AnalyticNumberTheory.LargeSieve.mem_vaughanTypeIFirstDyadicShell {u k d : ℕ} : d ∈ vaughanTypeIFirstDyadicShell u k ↔ 0 < d ∧ d ≤ u ∧ d.log2 = k

@[simp]

theorem AnalyticNumberTheory.LargeSieve.mem_vaughanTypeIMiddleProductDyadicShell {u v k d e : ℕ} : (d, e) ∈ vaughanTypeIMiddleProductDyadicShell u v k ↔ 0 < d ∧ d ≤ u ∧ 0 < e ∧ e ≤ v ∧ (d * e).log2 = k

theorem AnalyticNumberTheory.LargeSieve.vaughanTypeIFirstDyadicShell_bounds {u k d : ℕ} (hd : d ∈ vaughanTypeIFirstDyadicShell u k) : 2 ^ k ≤ d ∧ d < 2 ^ (k + 1)

A first shell really is contained in [2^k,2^(k+1)).

theorem AnalyticNumberTheory.LargeSieve.vaughanTypeIMiddleProductDyadicShell_bounds {u v k d e : ℕ} (hde : (d, e) ∈ vaughanTypeIMiddleProductDyadicShell u v k) : 2 ^ k ≤ d * e ∧ d * e < 2 ^ (k + 1)

A middle shell has the corresponding bounds on the actual product.

theorem AnalyticNumberTheory.LargeSieve.mem_own_vaughanTypeIFirstDyadicShell {u d : ℕ} (hd : 0 < d) (hdu : d ≤ u) : d ∈ vaughanTypeIFirstDyadicShell u d.log2

Every positive d ≤ u occurs in its actual dyadic shell.

theorem AnalyticNumberTheory.LargeSieve.mem_own_vaughanTypeIMiddleProductDyadicShell {u v d e : ℕ} (hd : 0 < d) (hdu : d ≤ u) (he : 0 < e) (hev : e ≤ v) : (d, e) ∈ vaughanTypeIMiddleProductDyadicShell u v (d * e).log2

Every positive pair in the Vaughan rectangle occurs in its product shell.

theorem AnalyticNumberTheory.LargeSieve.firstDyadicShell_index_lt {u k d : ℕ} (hd : d ∈ vaughanTypeIFirstDyadicShell u k) : k < u.log2 + 1

The shell index of a nonempty first shell lies in the advertised range.

theorem AnalyticNumberTheory.LargeSieve.middleProductDyadicShell_index_lt {u v k d e : ℕ} (hde : (d, e) ∈ vaughanTypeIMiddleProductDyadicShell u v k) : k < (u * v).log2 + 1

The shell index of a nonempty product shell lies in the advertised range.

noncomputable def AnalyticNumberTheory.LargeSieve.apNormalizedVaughanTypeIMiddleProductShellMean (S : Finset (ℕ × ℕ)) (N Q : ℕ) : ℝ

Literal AP-normalized mean of one middle product shell.

Equations

• AnalyticNumberTheory.LargeSieve.apNormalizedVaughanTypeIMiddleProductShellMean S N Q = AnalyticNumberTheory.LargeSieve.apNormalizedWeightedRowShellMean S (fun (de : ℕ × ℕ) => ↑(ArithmeticFunction.moebius de.1) * ↑(ArithmeticFunction.vonMangoldt de.2)) (AnalyticNumberTheory.LargeSieve.vaughanTypeIMiddlePairRowCoeff fun (x : ℕ) => 1) (AnalyticNumberTheory.LargeSieve.vaughanTypeIMiddlePairRowLength N) Q

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanTypeIFirstDyadicLogPay (u k N Q : ℕ) : ℝ

The exact physical payment attached to a first shell. This deliberately spells out the two literal ledgers; no global length-N moment is substituted.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanTypeIFirstDyadicLogPay u k N Q = √(AnalyticNumberTheory.LargeSieve.rowShellShortEnergy (AnalyticNumberTheory.LargeSieve.vaughanTypeIFirstDyadicShell u k) fun (d : ℕ) => ↑(ArithmeticFunction.moebius d)) * √(↑(2 ^ k) * AnalyticNumberTheory.LargeSieve.variableLengthPrimitivePrefixBudget (AnalyticNumberTheory.LargeSieve.vaughanTypeIFirstDyadicShell u k) (AnalyticNumberTheory.LargeSieve.vaughanTypeIFirstRowCoeff fun (x : ℕ) => 1) (AnalyticNumberTheory.LargeSieve.vaughanTypeIFirstRowLength N) Q) * √(AnalyticNumberTheory.LargeSieve.conductorHarmonicFactor Q)

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanTypeIMiddleProductDyadicLogPay (u v k N Q : ℕ) : ℝ

The analogous honest product-shell payment.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanTypeIMiddleProductDyadicLogPay u v k N Q = √(AnalyticNumberTheory.LargeSieve.rowShellShortEnergy (AnalyticNumberTheory.LargeSieve.vaughanTypeIMiddleProductDyadicShell u v k) fun (de : ℕ × ℕ) => ↑(ArithmeticFunction.moebius de.1) * ↑(ArithmeticFunction.vonMangoldt de.2)) * √(↑(2 ^ k) * AnalyticNumberTheory.LargeSieve.variableLengthPrimitivePrefixBudget (AnalyticNumberTheory.LargeSieve.vaughanTypeIMiddleProductDyadicShell u v k) (AnalyticNumberTheory.LargeSieve.vaughanTypeIMiddlePairRowCoeff fun (x : ℕ) => 1) (AnalyticNumberTheory.LargeSieve.vaughanTypeIMiddlePairRowLength N) Q) * √(AnalyticNumberTheory.LargeSieve.conductorHarmonicFactor Q)

theorem AnalyticNumberTheory.LargeSieve.apNormalizedVaughanTypeIFirstDyadicShell_physical (u k N Q : ℕ) (hN : 0 < N) (hQ : 0 < Q) (hcard : ∀ q ∈ Finset.Icc 1 Q, Fintype.card (PrimitiveCharacter q) ≤ q.totient) : apNormalizedVaughanTypeIFirstShellMean (vaughanTypeIFirstDyadicShell u k) N Q ≤ vaughanTypeIFirstDyadicLogPay u k N Q * (↑N + ↑Q * √(↑N * ↑(2 ^ k)))

Every first shell meets the existing physical lemma with its literal energy and variable-length budget.

theorem AnalyticNumberTheory.LargeSieve.apNormalizedVaughanTypeIMiddleProductDyadicShell_physical (u v k N Q : ℕ) (hN : 0 < N) (hQ : 0 < Q) (hcard : ∀ q ∈ Finset.Icc 1 Q, Fintype.card (PrimitiveCharacter q) ≤ q.totient) : apNormalizedVaughanTypeIMiddleProductShellMean (vaughanTypeIMiddleProductDyadicShell u v k) N Q ≤ vaughanTypeIMiddleProductDyadicLogPay u v k N Q * (↑N + ↑Q * √(↑N * ↑(2 ^ k)))

Every middle product shell meets the same physical lemma.

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanTypeIActualDyadicLogPay (N Q u v : ℕ) : ℝ

Explicit common payment used by the finite shell assembler.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanTypeIActualDyadicLogPay N Q u v = ∑ k ∈ Finset.range (u.log2 + 1), AnalyticNumberTheory.LargeSieve.vaughanTypeIFirstDyadicLogPay u k N Q + ∑ k ∈ Finset.range ((u * v).log2 + 1), AnalyticNumberTheory.LargeSieve.vaughanTypeIMiddleProductDyadicLogPay u v k N Q

theorem AnalyticNumberTheory.LargeSieve.vaughanTypeIFirstDyadicLogPay_nonneg (u k N Q : ℕ) : 0 ≤ vaughanTypeIFirstDyadicLogPay u k N Q

theorem AnalyticNumberTheory.LargeSieve.vaughanTypeIMiddleProductDyadicLogPay_nonneg (u v k N Q : ℕ) : 0 ≤ vaughanTypeIMiddleProductDyadicLogPay u v k N Q

theorem AnalyticNumberTheory.LargeSieve.vaughanTypeIActualDyadicLogPay_nonneg (N Q u v : ℕ) : 0 ≤ vaughanTypeIActualDyadicLogPay N Q u v