Structured Type-I coefficient energy for Vaughan's identity

This module opens the two divisor/convolution sums inside vaughanTypeICoeff. The resulting finite majorant records the outer truncated-divisor multiplicity, the logarithmic first convolution, and the complete inner truncated-divisor multiplicity of the middle convolution. Thus the Type-I lane is not discharged by treating vaughanTypeICoeff as an opaque sequence.

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanFirstDivisorEnergy (n u : ℕ) : ℝ

The explicit Cauchy energy of the truncated μ * log convolution.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanFirstDivisorEnergy n u = ↑{d ∈ n.divisors | d ≤ u}.card * ∑ d ∈ n.divisors with d ≤ u, (↑(ArithmeticFunction.moebius d) * Real.log ↑(n / d)) ^ 2

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanMiddleDivisorEnergy (n u v : ℕ) : ℝ

The explicit nested Cauchy energy of the truncated μ * Λ convolution. The inner divisor cardinality is retained separately for every outer divisor.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanMiddleDivisorEnergy n u v = ↑{d ∈ n.divisors | d ≤ u}.card * ∑ d ∈ n.divisors with d ≤ u, ↑{e ∈ (n / d).divisors | e ≤ v}.card * ∑ e ∈ (n / d).divisors with e ≤ v, (↑(ArithmeticFunction.moebius d) * ArithmeticFunction.vonMangoldt e) ^ 2

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanTypeIStructuredEnergy (n u v : ℕ) : ℝ

The pointwise structured Type-I budget. The factor 2 is exactly the loss in (A-B)^2 ≤ 2(A^2+B^2).

Equations

• AnalyticNumberTheory.LargeSieve.vaughanTypeIStructuredEnergy n u v = 2 * (AnalyticNumberTheory.LargeSieve.vaughanFirstDivisorEnergy n u + AnalyticNumberTheory.LargeSieve.vaughanMiddleDivisorEnergy n u v)

theorem AnalyticNumberTheory.LargeSieve.vaughanFirst_sq_le_divisorEnergy (n u : ℕ) : Sieve.vaughanFirst n u ^ 2 ≤ vaughanFirstDivisorEnergy n u

theorem AnalyticNumberTheory.LargeSieve.vaughanMiddle_sq_le_divisorEnergy (n u v : ℕ) : Sieve.vaughanMiddle n u v ^ 2 ≤ vaughanMiddleDivisorEnergy n u v

theorem AnalyticNumberTheory.LargeSieve.vaughanTypeI_sq_le_structuredEnergy (n u v : ℕ) : vaughanTypeI n u v ^ 2 ≤ vaughanTypeIStructuredEnergy n u v

Genuine Type-I pointwise estimate, obtained by expanding both divisor convolutions rather than applying a norm estimate to the already-packaged coefficient.

theorem AnalyticNumberTheory.LargeSieve.vaughanTypeIStructuredEnergy_nonneg (n u v : ℕ) : 0 ≤ vaughanTypeIStructuredEnergy n u v

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanTypeICutoffEnergy (n u v : ℕ) : ℝ

A coarser version of the structured energy in which the two truncated cardinalities are replaced by the literal cutoff factors u+1 and v+1. The divisor sums themselves (and hence every logarithmic/Λ factor) remain visible.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanTypeICutoffEnergy n u v = 2 * (↑(u + 1) * ∑ d ∈ n.divisors with d ≤ u, (↑(ArithmeticFunction.moebius d) * Real.log ↑(n / d)) ^ 2 + ↑(u + 1) * ∑ d ∈ n.divisors with d ≤ u, ↑(v + 1) * ∑ e ∈ (n / d).divisors with e ≤ v, (↑(ArithmeticFunction.moebius d) * ArithmeticFunction.vonMangoldt e) ^ 2)

theorem AnalyticNumberTheory.LargeSieve.vaughanTypeIStructuredEnergy_le_cutoffEnergy (n u v : ℕ) : vaughanTypeIStructuredEnergy n u v ≤ vaughanTypeICutoffEnergy n u v

theorem AnalyticNumberTheory.LargeSieve.vaughanTypeICutoffEnergy_nonneg (n u v : ℕ) : 0 ≤ vaughanTypeICutoffEnergy n u v

theorem AnalyticNumberTheory.LargeSieve.vaughanTypeICoeff_norm_sq_le (b : ℤ → ℂ) (u v : ℕ) (n : ℤ) : ‖vaughanTypeICoeff b u v n‖ ^ 2 ≤ ‖b n‖ ^ 2 * vaughanTypeIStructuredEnergy n.toNat u v

Pointwise coefficient-energy estimate with the scalar weight b left visible.

theorem AnalyticNumberTheory.LargeSieve.vaughanTypeICoeff_norm_sq_le_cutoff (b : ℤ → ℂ) (u v : ℕ) (n : ℤ) : ‖vaughanTypeICoeff b u v n‖ ^ 2 ≤ ‖b n‖ ^ 2 * vaughanTypeICutoffEnergy n.toNat u v

Pointwise version with the literal cutoff factors u+1 and v+1.

theorem AnalyticNumberTheory.LargeSieve.vaughanTypeICoeff_energy_le (b : ℤ → ℂ) (N u v : ℕ) : ∑ n ∈ Finset.Icc 1 ↑N, ‖vaughanTypeICoeff b u v n‖ ^ 2 ≤ ∑ n ∈ Finset.Icc 1 ↑N, ‖b n‖ ^ 2 * vaughanTypeIStructuredEnergy n.toNat u v

The finite ℓ² Type-I coefficient energy on [1,N], with N, both cutoffs, all logarithms, and both divisor multiplicities explicit.

theorem AnalyticNumberTheory.LargeSieve.vaughanTypeICoeff_energy_le_cutoff (b : ℤ → ℂ) (N u v : ℕ) : ∑ n ∈ Finset.Icc 1 ↑N, ‖vaughanTypeICoeff b u v n‖ ^ 2 ≤ ∑ n ∈ Finset.Icc 1 ↑N, ‖b n‖ ^ 2 * vaughanTypeICutoffEnergy n.toNat u v

Fully explicit cutoff-factor form of the finite Type-I energy bound.

theorem AnalyticNumberTheory.LargeSieve.weighted_vaughan_prefix_large_sieve_typeI_ledger (b : ℤ → ℂ) (N Q u v : ℕ) (hQ : 0 < Q) : ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, primitiveCharacterPrefixMaxSquare (vaughanLambdaCoeff b) 0 N q χ ≤ 3 * ↑(N.log2 + 1) ^ 2 * primitiveLargeSieveConstant N Q * (∑ n ∈ Finset.Icc 1 ↑N, ‖b n‖ ^ 2 * vaughanTypeICutoffEnergy n.toNat u v + ∑ n ∈ Finset.Icc 1 ↑N, ‖vaughanTypeIICoeff b u v n‖ ^ 2 + ∑ n ∈ Finset.Icc 1 ↑N, ‖vaughanSmallCoeff b v n‖ ^ 2)

The weighted prefix large-sieve ledger with the Type-I lane replaced by its genuine divisor/convolution energy. The Type-II and small lanes remain visible as the next independent fronts.