Structured Type-II coefficient energy for Vaughan's identity

This module opens the large--large divisor pair in vaughanThird. Its coefficient budget retains the outer large divisor multiplicity, the inner large divisor multiplicity for each outer divisor, and every Möbius and von Mangoldt weight. In particular the Type-II lane is not bounded by treating vaughanTypeIICoeff as an opaque sequence.

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

The genuine large--large divisor-pair energy of vaughanThird.

The first cardinality counts eligible d > u; the cardinality inside the d-sum counts eligible e > v dividing n / d. The summand keeps the factorized Möbius/von-Mangoldt weight instead of hiding it in a packaged Type-II coefficient.

Equations

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

theorem AnalyticNumberTheory.LargeSieve.vaughanThird_sq_le_divisorEnergy (n u v : ℕ) : Sieve.vaughanThird n u v ^ 2 ≤ vaughanTypeIIDivisorEnergy n u v

Nested Cauchy--Schwarz on the actual large--large divisor structure.

theorem AnalyticNumberTheory.LargeSieve.vaughanTypeII_sq_le_divisorEnergy (n u v : ℕ) : vaughanTypeII n u v ^ 2 ≤ vaughanTypeIIDivisorEnergy n u v

The same structural estimate at the public Type-II alias.

theorem AnalyticNumberTheory.LargeSieve.vaughanTypeIIDivisorEnergy_nonneg (n u v : ℕ) : 0 ≤ vaughanTypeIIDivisorEnergy n u v

theorem AnalyticNumberTheory.LargeSieve.vaughanTypeIICoeff_norm_sq_le_divisorEnergy (b : ℤ → ℂ) (u v : ℕ) (n : ℤ) : ‖vaughanTypeIICoeff b u v n‖ ^ 2 ≤ ‖b n‖ ^ 2 * vaughanTypeIIDivisorEnergy n.toNat u v

Pointwise coefficient estimate with the scalar coefficient b n separate from the expanded large--large divisor energy.

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

Structured finite ℓ² coefficient energy on [1,N]. The interval keeps N literal, while each summand keeps u, v, both divisor multiplicities, and all Möbius/Λ weights.

theorem AnalyticNumberTheory.LargeSieve.weighted_vaughan_prefix_large_sieve_structured_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, ‖b n‖ ^ 2 * vaughanTypeIIDivisorEnergy n.toNat u v + ∑ n ∈ Finset.Icc 1 ↑N, ‖vaughanSmallCoeff b v n‖ ^ 2)

Weighted Vaughan prefix ledger with both non-small lanes expanded. Type I uses its cutoff-factor divisor budget and Type II uses the genuine large--large nested divisor-pair energy above; only the explicitly retained small range is left as a packaged norm lane.