Prefix-maximal weighted primitive-character large sieve

This module isolates the finite Rademacher--Menshov transfer needed by Vaughan Type I/II arguments. A prefix is allowed to be written as a sum of at most L interval blocks, and the total block energy is allowed to cover each coefficient at most D times. The resulting loss is exactly L * D, uniformly in the coefficient sequence, the interval origin, the modulus bound, and the character.

For the usual aligned dyadic decomposition one takes L = D = Nat.log2 N + 1; the final corollary records the resulting square-log loss explicitly. Keeping the finite decomposition hypotheses visible makes the lemma directly reusable by Vaughan decompositions without introducing any analytic or asymptotic assumption.

noncomputable def AnalyticNumberTheory.LargeSieve.primitiveLargeSieveConstant (N Q : ℕ) : ℝ

The fully expanded constant in the non-maximal weighted primitive-character large sieve.

Equations

• AnalyticNumberTheory.LargeSieve.primitiveLargeSieveConstant N Q = ↑N + (2 * ↑⌈Real.log (↑Q ^ 2) / Real.log 2⌉₊ + 12) * ↑Q ^ 2

theorem AnalyticNumberTheory.LargeSieve.weighted_primitive_bombieri_davenport_explicit' (b : ℤ → ℂ) (M : ℤ) (N Q : ℕ) (hQ : 0 < Q) : ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, ‖∑ n ∈ Finset.Icc (M + 1) (M + ↑N), b n * ↑χ ↑n‖ ^ 2 ≤ primitiveLargeSieveConstant N Q * ∑ n ∈ Finset.Icc (M + 1) (M + ↑N), ‖b n‖ ^ 2

The existing Bombieri--Davenport estimate, packaged with its explicit constant for use by the maximal transfer.

theorem AnalyticNumberTheory.LargeSieve.primitiveLargeSieveConstant_mono_left {N₁ N₂ Q : ℕ} (hN : N₁ ≤ N₂) : primitiveLargeSieveConstant N₁ Q ≤ primitiveLargeSieveConstant N₂ Q

The explicit large-sieve constant is monotone in the interval length.

theorem AnalyticNumberTheory.LargeSieve.norm_finset_sum_sq_le_card_mul_sum_norm_sq {ι : Type u_1} [DecidableEq ι] (s : Finset ι) (z : ι → ℂ) : ‖∑ i ∈ s, z i‖ ^ 2 ≤ ↑s.card * ∑ i ∈ s, ‖z i‖ ^ 2

Squared norm of a finite sum, with the exact cardinality loss used in the Rademacher--Menshov step.

theorem AnalyticNumberTheory.LargeSieve.finiteComplexCauchy {ι : Type u_1} [DecidableEq ι] (s : Finset ι) (a b : ι → ℂ) : ‖∑ i ∈ s, a i * b i‖ ^ 2 ≤ (∑ i ∈ s, ‖a i‖ ^ 2) * ∑ i ∈ s, ‖b i‖ ^ 2

Exact finite complex Cauchy--Schwarz, with no intervening norm_sum_le.

noncomputable def AnalyticNumberTheory.LargeSieve.primitiveCharacterPrefixSquare (b : ℤ → ℂ) (M : ℤ) (y q : ℕ) (χ : PrimitiveCharacter q) : ℝ

Prefix square for one primitive character.

Equations

• AnalyticNumberTheory.LargeSieve.primitiveCharacterPrefixSquare b M y q χ = ‖∑ n ∈ Finset.Icc (M + 1) (M + ↑y), b n * ↑χ ↑n‖ ^ 2

noncomputable def AnalyticNumberTheory.LargeSieve.primitiveCharacterPrefixMaxSquare (b : ℤ → ℂ) (M : ℤ) (N q : ℕ) (χ : PrimitiveCharacter q) : ℝ

Maximum of the character-sum square over all integer prefixes 0 ≤ y ≤ N. The defining finite set is nonempty because it contains y = 0.

Equations

• AnalyticNumberTheory.LargeSieve.primitiveCharacterPrefixMaxSquare b M N q χ = (Finset.image (fun (y : ℕ) => AnalyticNumberTheory.LargeSieve.primitiveCharacterPrefixSquare b M y q χ) (Finset.range (N + 1))).max' ⋯

theorem AnalyticNumberTheory.LargeSieve.primitiveCharacterPrefixSquare_le_max (b : ℤ → ℂ) (M : ℤ) {N y q : ℕ} (hy : y ≤ N) (χ : PrimitiveCharacter q) : primitiveCharacterPrefixSquare b M y q χ ≤ primitiveCharacterPrefixMaxSquare b M N q χ

Every prefix square is bounded by the corresponding finite prefix maximum.

theorem AnalyticNumberTheory.LargeSieve.primitiveCharacterPrefixMaxSquare_nonneg (b : ℤ → ℂ) (M : ℤ) (N d : ℕ) (ψ : PrimitiveCharacter d) : 0 ≤ primitiveCharacterPrefixMaxSquare b M N d ψ

Primitive prefix maxima are nonnegative.

theorem AnalyticNumberTheory.LargeSieve.weighted_primitive_prefix_maximal_of_interval_decomposition {ι : Type u_1} [Fintype ι] [DecidableEq ι] (b : ℤ → ℂ) (M : ℤ) (N Q L D : ℕ) (hQ : 0 < Q) (blockStart : ι → ℤ) (blockLength : ι → ℕ) (prefixBlocks : ℕ → Finset ι) (hdecomp : ∀ y ∈ Finset.range (N + 1), ∀ (f : ℤ → ℂ), ∑ n ∈ Finset.Icc (M + 1) (M + ↑y), f n = ∑ i ∈ prefixBlocks y, ∑ n ∈ Finset.Icc (blockStart i + 1) (blockStart i + ↑(blockLength i)), f n) (hcard : ∀ y ∈ Finset.range (N + 1), (prefixBlocks y).card ≤ L) (hlength : ∀ (i : ι), blockLength i ≤ N) (hoverlap : ∑ i : ι, ∑ n ∈ Finset.Icc (blockStart i + 1) (blockStart i + ↑(blockLength i)), ‖b n‖ ^ 2 ≤ ↑D * ∑ n ∈ Finset.Icc (M + 1) (M + ↑N), ‖b n‖ ^ 2) : ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, primitiveCharacterPrefixMaxSquare b M N q χ ≤ ↑L * ↑D * primitiveLargeSieveConstant N Q * ∑ n ∈ Finset.Icc (M + 1) (M + ↑N), ‖b n‖ ^ 2

Finite Rademacher--Menshov transfer for primitive characters.

The interval indexed by i is (blockStart i, blockStart i + blockLength i]. The first hypothesis says that every prefix is the sum of at most L selected blocks. The second bounds all block lengths by the ambient length N. The last is the overlap-energy estimate; for aligned dyadic blocks its sharp finite value is D = Nat.log2 N + 1.

The conclusion has the maximum inside the primitive-character sum. Its constant is uniform and completely explicit: L * D times the already proved N + (2⌈log₂(Q²)⌉+12)Q² constant.

theorem AnalyticNumberTheory.LargeSieve.weighted_primitive_prefix_maximal_of_dyadic_decomposition {ι : Type u_1} [Fintype ι] [DecidableEq ι] (b : ℤ → ℂ) (M : ℤ) (N Q : ℕ) (hQ : 0 < Q) (blockStart : ι → ℤ) (blockLength : ι → ℕ) (prefixBlocks : ℕ → Finset ι) (hdecomp : ∀ y ∈ Finset.range (N + 1), ∀ (f : ℤ → ℂ), ∑ n ∈ Finset.Icc (M + 1) (M + ↑y), f n = ∑ i ∈ prefixBlocks y, ∑ n ∈ Finset.Icc (blockStart i + 1) (blockStart i + ↑(blockLength i)), f n) (hcard : ∀ y ∈ Finset.range (N + 1), (prefixBlocks y).card ≤ N.log2 + 1) (hlength : ∀ (i : ι), blockLength i ≤ N) (hoverlap : ∑ i : ι, ∑ n ∈ Finset.Icc (blockStart i + 1) (blockStart i + ↑(blockLength i)), ‖b n‖ ^ 2 ≤ ↑(N.log2 + 1) * ∑ n ∈ Finset.Icc (M + 1) (M + ↑N), ‖b n‖ ^ 2) : ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, primitiveCharacterPrefixMaxSquare b M N q χ ≤ ↑(N.log2 + 1) ^ 2 * primitiveLargeSieveConstant N Q * ∑ n ∈ Finset.Icc (M + 1) (M + ↑N), ‖b n‖ ^ 2

Dyadic/Rademacher--Menshov specialization. Supplying the standard aligned finite dyadic decomposition with depth Nat.log2 N + 1 gives the exact new loss (Nat.log2 N + 1)², on top of the pre-existing additive large-sieve logarithm. All constants remain uniform in b, M, Q, and every primitive character.