Variable-length primitive maximal large sieve for Vaughan Type I

This module does not collect the products d*m (or d*e*m) back into one coefficient sequence of length N. Each short row keeps its physical prefix length, and the Rademacher--Menshov loss is paid separately at that length. Consequently the large-sieve ledger contains primitiveLargeSieveConstant (L r) Q for each row r, rather than one copy of the length-N constant multiplying an already collected length-N moment.

noncomputable def AnalyticNumberTheory.LargeSieve.variableLengthPrimitivePrefixBudget {ι : Type u_1} [DecidableEq ι] (S : Finset ι) (c : ι → ℤ → ℂ) (L : ι → ℕ) (Q : ℕ) : ℝ

The exact row-by-row RHS of the variable-length maximal large sieve. The factor (log₂ L+1)^2 is the explicit Rademacher--Menshov payment for a complete prefix maximum in that row.

Equations

• AnalyticNumberTheory.LargeSieve.variableLengthPrimitivePrefixBudget S c L Q = ∑ r ∈ S, ↑((L r).log2 + 1) ^ 2 * AnalyticNumberTheory.LargeSieve.primitiveLargeSieveConstant (L r) Q * ∑ m ∈ Finset.Icc (0 + 1) (0 + ↑(L r)), ‖c r m‖ ^ 2

theorem AnalyticNumberTheory.LargeSieve.weighted_primitive_variableLength_prefix_maximal {ι : Type u_1} [DecidableEq ι] (S : Finset ι) (c : ι → ℤ → ℂ) (L : ι → ℕ) (Q : ℕ) (hQ : 0 < Q) : ∑ r ∈ S, ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, primitiveCharacterPrefixMaxSquare (c r) 0 (L r) q χ ≤ variableLengthPrimitivePrefixBudget S c L Q

Variable-length prefix large sieve. Every short row is sent to the primitive maximal theorem at its own length. In particular no ambient N occurs in the analytic constant unless it is already one of the row lengths.

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanTypeIFirstRowCoeff (b : ℕ → ℂ) (d : ℕ) (m : ℤ) : ℂ

The long row in the first Type-I lane after fixing d.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanTypeIFirstRowCoeff b d m = b (d * m.toNat) * ↑(Real.log ↑m.toNat)

def AnalyticNumberTheory.LargeSieve.vaughanTypeIMiddleRowCoeff (b : ℕ → ℂ) (a : ℕ) (m : ℤ) : ℂ

The long row in the middle Type-I lane after fixing the product a=d*e.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanTypeIMiddleRowCoeff b a m = b (a * m.toNat)

def AnalyticNumberTheory.LargeSieve.vaughanTypeIFirstRowLength (N d : ℕ) : ℕ

First-lane physical row length.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanTypeIFirstRowLength N d = N / d

def AnalyticNumberTheory.LargeSieve.vaughanTypeIMiddleRowLength (N a : ℕ) : ℕ

Middle-lane physical row length, indexed by the short product a=d*e.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanTypeIMiddleRowLength N a = N / a

def AnalyticNumberTheory.LargeSieve.vaughanTypeIMiddlePairRowCoeff (b : ℕ → ℂ) (de : ℕ × ℕ) (m : ℤ) : ℂ

The same middle row with the two short shells kept separate.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanTypeIMiddlePairRowCoeff b de m = b (de.1 * de.2 * m.toNat)

def AnalyticNumberTheory.LargeSieve.vaughanTypeIMiddlePairRowLength (N : ℕ) (de : ℕ × ℕ) : ℕ

Equations

• AnalyticNumberTheory.LargeSieve.vaughanTypeIMiddlePairRowLength N de = N / (de.1 * de.2)

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanTypeIFirstShortEnergy (DS : Finset ℕ) : ℝ

Literal Möbius square-energy on a first-lane shell.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanTypeIFirstShortEnergy DS = ∑ d ∈ DS, ‖↑(ArithmeticFunction.moebius d)‖ ^ 2

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanTypeIMiddleShortEnergy (DS ES : Finset ℕ) : ℝ

Literal μ²Λ² energy on two middle-lane shells.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanTypeIMiddleShortEnergy DS ES = ∑ d ∈ DS, ∑ e ∈ ES, ‖↑(ArithmeticFunction.moebius d) * ↑(ArithmeticFunction.vonMangoldt e)‖ ^ 2

theorem AnalyticNumberTheory.LargeSieve.vaughanTypeIFirstShortEnergy_le_card (DS : Finset ℕ) : vaughanTypeIFirstShortEnergy DS ≤ ↑DS.card

theorem AnalyticNumberTheory.LargeSieve.vaughanTypeIMiddleShortEnergy_le_mangoldt (DS ES : Finset ℕ) : vaughanTypeIMiddleShortEnergy DS ES ≤ ↑DS.card * ∑ e ∈ ES, ‖↑(ArithmeticFunction.vonMangoldt e)‖ ^ 2

theorem AnalyticNumberTheory.LargeSieve.weighted_primitive_vaughanTypeIFirstRows (b : ℕ → ℂ) (N Q : ℕ) (DS : Finset ℕ) (hQ : 0 < Q) : ∑ d ∈ DS, ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, primitiveCharacterPrefixMaxSquare (vaughanTypeIFirstRowCoeff b d) 0 (N / d) q χ ≤ variableLengthPrimitivePrefixBudget DS (vaughanTypeIFirstRowCoeff b) (vaughanTypeIFirstRowLength N) Q

First Type-I dyadic row ledger. This is the genuine long-variable primitive estimate: the dth row uses length N/d.

theorem AnalyticNumberTheory.LargeSieve.weighted_primitive_vaughanTypeIMiddleRows (b : ℕ → ℂ) (N Q : ℕ) (AS : Finset ℕ) (hQ : 0 < Q) : ∑ a ∈ AS, ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, primitiveCharacterPrefixMaxSquare (vaughanTypeIMiddleRowCoeff b a) 0 (N / a) q χ ≤ variableLengthPrimitivePrefixBudget AS (vaughanTypeIMiddleRowCoeff b) (vaughanTypeIMiddleRowLength N) Q

Middle Type-I row ledger after grouping the two short variables by their product a=d*e. A two-shell implementation can map each (d,e) to this same row interface without changing the physical length N/(d*e).

theorem AnalyticNumberTheory.LargeSieve.weighted_primitive_vaughanTypeIMiddlePairRows (b : ℕ → ℂ) (N Q : ℕ) (DS ES : Finset ℕ) (hQ : 0 < Q) : ∑ de ∈ DS ×ˢ ES, ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, primitiveCharacterPrefixMaxSquare (vaughanTypeIMiddlePairRowCoeff b de) 0 (N / (de.1 * de.2)) q χ ≤ variableLengthPrimitivePrefixBudget (DS ×ˢ ES) (vaughanTypeIMiddlePairRowCoeff b) (vaughanTypeIMiddlePairRowLength N) Q

Two-shell version of the middle lane; the inner maximal large sieve is still applied at the variable length N/(d*e).

theorem AnalyticNumberTheory.LargeSieve.variableLengthPrimitivePrefixBudget_le_physicalScale {ι : Type u_1} [DecidableEq ι] (S : Finset ι) (c : ι → ℤ → ℂ) (L : ι → ℕ) (N Lmax Q : ℕ) (hL : ∀ r ∈ S, L r ≤ Lmax) (hpack : S.card * Lmax ≤ N) (henergy : ∀ r ∈ S, ↑((L r).log2 + 1) ^ 2 * ∑ m ∈ Finset.Icc (0 + 1) (0 + ↑(L r)), ‖c r m‖ ^ 2 ≤ 1) : variableLengthPrimitivePrefixBudget S c L Q ≤ ↑N + ↑S.card * ((2 * ↑⌈Real.log (↑Q ^ 2) / Real.log 2⌉₊ + 12) * ↑Q ^ 2)

Abstract physical-scale compression. If the RM-weighted energy of every row is at most one, the length contribution is #S * Lmax, not N times a collected moment. The hypothesis #S * Lmax ≤ N then gives exactly N + #S * K(Q) Q².

theorem AnalyticNumberTheory.LargeSieve.imprimitive_conductor_window_family_le_linear_typeI (F : (d : ℕ) → PrimitiveCharacter d → ℝ) (hF : ∀ (d : ℕ) (ψ : PrimitiveCharacter d), 0 ≤ F d ψ) (Q C : ℕ) (hC : 0 < C) : ∑ d ∈ Finset.Icc C (2 * C), imprimitiveConductorWeight Q d * ∑ ψ : PrimitiveCharacter d, F d ψ ≤ ↑(Q / C) * conductorHarmonicFactor (Q / C) * ∑ d ∈ Finset.Icc 1 (2 * C), ↑d / ↑d.totient * ∑ ψ : PrimitiveCharacter d, F d ψ

Linear-harmonic transport for an arbitrary nonnegative conductor family. This local form avoids routing the Type-I module through an all-character aggregate.

theorem AnalyticNumberTheory.LargeSieve.imprimitive_conductor_window_variableLength_prefix_le_linear {ι : Type u_1} [DecidableEq ι] (S : Finset ι) (c : ι → ℤ → ℂ) (L : ι → ℕ) (Q C : ℕ) (hC : 0 < C) : ∑ d ∈ Finset.Icc C (2 * C), imprimitiveConductorWeight Q d * ∑ ψ : PrimitiveCharacter d, ∑ r ∈ S, primitiveCharacterPrefixMaxSquare (c r) 0 (L r) d ψ ≤ ↑(Q / C) * conductorHarmonicFactor (Q / C) * variableLengthPrimitivePrefixBudget S c L (2 * C)

Linear-harmonic imprimitive conductor transport applied before the variable row lengths are forgotten. This is the connector used on every dyadic conductor window.