Genuine bilinear blocks for Vaughan Type II

This module performs the finite rearrangement before any pointwise square is taken. A dyadic rectangle in the large variables d,e is rewritten from a prefix in n into the exact variables n = d*e*m; multiplicativity then puts one character on each variable. The final estimates apply Cauchy only in the outer d variable and leave the complete e,m sum visible.

def AnalyticNumberTheory.LargeSieve.vaughanDyadicBlock (D : ℕ) : Finset ℕ

The half-open dyadic interval (D,2D].

Equations

• AnalyticNumberTheory.LargeSieve.vaughanDyadicBlock D = Finset.Ioc D (2 * D)

@[simp]

theorem AnalyticNumberTheory.LargeSieve.mem_vaughanDyadicBlock {D d : ℕ} : d ∈ vaughanDyadicBlock D ↔ D < d ∧ d ≤ 2 * D

theorem AnalyticNumberTheory.LargeSieve.card_vaughanDyadicBlock (D : ℕ) : (vaughanDyadicBlock D).card = D

A dyadic block contains exactly D natural numbers.

theorem AnalyticNumberTheory.LargeSieve.sum_multiples_Icc_reindex {R : Type u_1} [AddCommMonoid R] (F : ℕ → R) {k y : ℕ} (hk : 0 < k) : ∑ n ∈ Finset.Icc 1 y with k ∣ n, F n = ∑ m ∈ Finset.Icc 1 (y / k), F (k * m)

Exact finite enumeration of the positive multiples of k in [1,y]. This is the atomic n = k*m reindexing used with k=d*e.

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanBilinearBlockPrefix (α β c : ℕ → ℂ) (y D E q : ℕ) (χ : PrimitiveCharacter q) : ℂ

Prefix form of one rectangular block. The divisibility indicator is the literal statement that the prefix index has a factorization n=d*e*m.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanBilinearBlockPrefix α β c y D E q χ = ∑ n ∈ Finset.Icc 1 y, c n * ↑χ ↑n * ∑ d ∈ AnalyticNumberTheory.LargeSieve.vaughanDyadicBlock D, ∑ e ∈ AnalyticNumberTheory.LargeSieve.vaughanDyadicBlock E, if d * e ∣ n then α d * β e else 0

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanBilinearBlockRaw (α β c : ℕ → ℂ) (y D E q : ℕ) (χ : PrimitiveCharacter q) : ℂ

The same block after the exact finite substitution n=d*e*m, but before splitting the character.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanBilinearBlockRaw α β c y D E q χ = ∑ d ∈ AnalyticNumberTheory.LargeSieve.vaughanDyadicBlock D, ∑ e ∈ AnalyticNumberTheory.LargeSieve.vaughanDyadicBlock E, α d * β e * ∑ m ∈ Finset.Icc 1 (y / (d * e)), c (d * e * m) * ↑χ ↑(d * e * m)

theorem AnalyticNumberTheory.LargeSieve.vaughanBilinearBlockPrefix_eq_raw (α β c : ℕ → ℂ) (y D E q : ℕ) (χ : PrimitiveCharacter q) (hD : 0 < D) (hE : 0 < E) : vaughanBilinearBlockPrefix α β c y D E q χ = vaughanBilinearBlockRaw α β c y D E q χ

Exact finite rectangular reindexing of a prefix. No convergence or analytic estimate is involved.

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanBilinearBlock (α β c : ℕ → ℂ) (y D E q : ℕ) (χ : PrimitiveCharacter q) : ℂ

Character-separated d,e,m form of a dyadic rectangular block.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanBilinearBlock α β c y D E q χ = ∑ d ∈ AnalyticNumberTheory.LargeSieve.vaughanDyadicBlock D, α d * ↑χ ↑d * ∑ e ∈ AnalyticNumberTheory.LargeSieve.vaughanDyadicBlock E, β e * ↑χ ↑e * ∑ m ∈ Finset.Icc 1 (y / (d * e)), c (d * e * m) * ↑χ ↑m

theorem AnalyticNumberTheory.LargeSieve.vaughanBilinearBlockRaw_eq_separated (α β c : ℕ → ℂ) (y D E q : ℕ) (χ : PrimitiveCharacter q) : vaughanBilinearBlockRaw α β c y D E q χ = vaughanBilinearBlock α β c y D E q χ

Exact multiplicative separation of the character across n=d*e*m.

theorem AnalyticNumberTheory.LargeSieve.vaughanBilinearBlockPrefix_eq_separated (α β c : ℕ → ℂ) (y D E q : ℕ) (χ : PrimitiveCharacter q) (hD : 0 < D) (hE : 0 < E) : vaughanBilinearBlockPrefix α β c y D E q χ = vaughanBilinearBlock α β c y D E q χ

Combined exact prefix-to-bilinear theorem for one dyadic rectangle.

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanBilinearInner (β c : ℕ → ℂ) (y E q d : ℕ) (χ : PrimitiveCharacter q) : ℂ

The still-bilinear inner e,m packet after selecting the outer variable d. This is deliberately not squared pointwise in the product n.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanBilinearInner β c y E q d χ = ∑ e ∈ AnalyticNumberTheory.LargeSieve.vaughanDyadicBlock E, β e * ↑χ ↑e * ∑ m ∈ Finset.Icc 1 (y / (d * e)), c (d * e * m) * ↑χ ↑m

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanBilinearOuterEnergy (β c : ℕ → ℂ) (y D E q : ℕ) (χ : PrimitiveCharacter q) : ℝ

The exact norm interface left after Cauchy in d only.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanBilinearOuterEnergy β c y D E q χ = ∑ d ∈ AnalyticNumberTheory.LargeSieve.vaughanDyadicBlock D, ‖AnalyticNumberTheory.LargeSieve.vaughanBilinearInner β c y E q d χ‖ ^ 2

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanBilinearLeftEnergy (α : ℕ → ℂ) (D q : ℕ) (χ : PrimitiveCharacter q) : ℝ

The d-coefficient energy, with the character twist kept literal.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanBilinearLeftEnergy α D q χ = ∑ d ∈ AnalyticNumberTheory.LargeSieve.vaughanDyadicBlock D, ‖α d * ↑χ ↑d‖ ^ 2

theorem AnalyticNumberTheory.LargeSieve.vaughanBilinearBlock_norm_sq_le (α β c : ℕ → ℂ) (y D E q : ℕ) (χ : PrimitiveCharacter q) : ‖vaughanBilinearBlock α β c y D E q χ‖ ^ 2 ≤ vaughanBilinearLeftEnergy α D q χ * vaughanBilinearOuterEnergy β c y D E q χ

One-variable Cauchy--Schwarz. The physical ledger has one outer d energy and one sum of squared e,m packets; there is no D²E² pointwise coefficient loss.

theorem AnalyticNumberTheory.LargeSieve.sum_primitive_vaughanBilinearBlock_norm_sq_le (α β c : ℕ → ℂ) (y D E q : ℕ) : ∑ χ : PrimitiveCharacter q, ‖vaughanBilinearBlock α β c y D E q χ‖ ^ 2 ≤ ∑ χ : PrimitiveCharacter q, vaughanBilinearLeftEnergy α D q χ * vaughanBilinearOuterEnergy β c y D E q χ

Primitive-character block-norm interface. A future bilinear primitive large sieve can consume the remaining sum of outer energies directly.

theorem AnalyticNumberTheory.LargeSieve.vaughanBilinearLeftEnergy_le_blockLength (α : ℕ → ℂ) (D q : ℕ) (χ : PrimitiveCharacter q) (A : ℝ) (hA : ∀ d ∈ vaughanDyadicBlock D, ‖α d * ↑χ ↑d‖ ^ 2 ≤ A) : vaughanBilinearLeftEnergy α D q χ ≤ ↑D * A

Literal physical scale after Cauchy in d: a pointwise bound on the twisted left coefficient costs exactly the block length D, not D².

def AnalyticNumberTheory.LargeSieve.vaughanMoebiusCoeff (d : ℕ) : ℂ

Vaughan's actual factor weights for the Type-II rectangle.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanMoebiusCoeff d = ↑(ArithmeticFunction.moebius d)

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanMangoldtCoeff (e : ℕ) : ℂ

Equations

• AnalyticNumberTheory.LargeSieve.vaughanMangoldtCoeff e = ↑(ArithmeticFunction.vonMangoldt e)

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanTypeIIBlockAt (n D E : ℕ) : ℂ

The contribution at n from one dyadic rectangle in the two large divisor variables of Sieve.vaughanThird.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanTypeIIBlockAt n D E = ∑ d ∈ n.divisors with d ∈ AnalyticNumberTheory.LargeSieve.vaughanDyadicBlock D, ∑ e ∈ (n / d).divisors with e ∈ AnalyticNumberTheory.LargeSieve.vaughanDyadicBlock E, AnalyticNumberTheory.LargeSieve.vaughanMoebiusCoeff d * AnalyticNumberTheory.LargeSieve.vaughanMangoldtCoeff e

theorem AnalyticNumberTheory.LargeSieve.vaughanTypeIIBlockAt_eq_rectangular {n D E : ℕ} (hn : 0 < n) (hD : 0 < D) : vaughanTypeIIBlockAt n D E = ∑ d ∈ vaughanDyadicBlock D, ∑ e ∈ vaughanDyadicBlock E, if d * e ∣ n then vaughanMoebiusCoeff d * vaughanMangoldtCoeff e else 0

The nested divisor definition of a Type-II rectangle is exactly the fixed rectangular pair sum with the condition d*e ∣ n.

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanTypeIIBlockPrefix (b : ℕ → ℂ) (y D E q : ℕ) (χ : PrimitiveCharacter q) : ℂ

The literal prefix contribution of one Type-II divisor rectangle.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanTypeIIBlockPrefix b y D E q χ = ∑ n ∈ Finset.Icc 1 y, b n * ↑χ ↑n * AnalyticNumberTheory.LargeSieve.vaughanTypeIIBlockAt n D E

theorem AnalyticNumberTheory.LargeSieve.vaughanTypeIIBlockPrefix_eq_generic (b : ℕ → ℂ) (y D E q : ℕ) (χ : PrimitiveCharacter q) (hD : 0 < D) : vaughanTypeIIBlockPrefix b y D E q χ = vaughanBilinearBlockPrefix vaughanMoebiusCoeff vaughanMangoldtCoeff b y D E q χ

The rectangular indicator prefix used by the generic reindexing is the actual nested Vaughan Type-II divisor block.

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanTypeIIBilinearBlock (b : ℕ → ℂ) (y D E q : ℕ) (χ : PrimitiveCharacter q) : ℂ

The concrete Type-II block uses Möbius in d, von Mangoldt in e, and keeps the external coefficient at the physical product d*e*m.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanTypeIIBilinearBlock b y D E q χ = AnalyticNumberTheory.LargeSieve.vaughanBilinearBlock AnalyticNumberTheory.LargeSieve.vaughanMoebiusCoeff AnalyticNumberTheory.LargeSieve.vaughanMangoldtCoeff b y D E q χ

theorem AnalyticNumberTheory.LargeSieve.vaughanTypeIIBlockPrefix_eq_bilinear (b : ℕ → ℂ) (y D E q : ℕ) (χ : PrimitiveCharacter q) (hD : 0 < D) (hE : 0 < E) : vaughanTypeIIBlockPrefix b y D E q χ = vaughanTypeIIBilinearBlock b y D E q χ

Headline algebraic rearrangement for an actual Vaughan Type-II dyadic rectangle: prefix in n, exact substitution n=d*e*m, and character separation, all as a finite equality.

theorem AnalyticNumberTheory.LargeSieve.sum_vaughanTypeIIBlockPrefix_eq_bilinear (b : ℕ → ℂ) (y q : ℕ) (χ : PrimitiveCharacter q) (DS ES : Finset ℕ) (hDS : ∀ D ∈ DS, 0 < D) (hES : ∀ E ∈ ES, 0 < E) : ∑ D ∈ DS, ∑ E ∈ ES, vaughanTypeIIBlockPrefix b y D E q χ = ∑ D ∈ DS, ∑ E ∈ ES, vaughanTypeIIBilinearBlock b y D E q χ

Finite family version: once positive dyadic block bases have been selected, the whole block sum is reindexed rectangle by rectangle. Disjoint-cover bookkeeping is intentionally separate from this algebraic theorem.