def AnalyticNumberTheory.LargeSieve.vaughanTypeIRowCoefficient (a : ℂ) (b : ℤ → ℂ) (n : ℤ) : ℂ

Equations

• AnalyticNumberTheory.LargeSieve.vaughanTypeIRowCoefficient a b n = a * b n

noncomputable def AnalyticNumberTheory.LargeSieve.highConductorVaughanTypeIRowAmplitude (a : ℂ) (b : ℤ → ℂ) (M : ℤ) (L d : ℕ) (χ : PrimitiveCharacter d) : ℝ

Equations

• AnalyticNumberTheory.LargeSieve.highConductorVaughanTypeIRowAmplitude a b M L d χ = √(AnalyticNumberTheory.LargeSieve.primitiveCharacterPrefixMaxSquare (AnalyticNumberTheory.LargeSieve.vaughanTypeIRowCoefficient a b) M L d χ)

theorem AnalyticNumberTheory.LargeSieve.highConductorVaughanTypeIRow_squareLedger_le (R Q L : ℕ) (hQ : 0 < Q) (a : ℂ) (b : ℤ → ℂ) (M : ℤ) : highConductorPrimitiveSquareLedger R Q (highConductorVaughanTypeIRowAmplitude a b M L) ≤ ↑(L.log2 + 1) ^ 2 * primitiveLargeSieveConstant L Q * ∑ n ∈ Finset.Icc (M + 1) (M + ↑L), ‖vaughanTypeIRowCoefficient a b n‖ ^ 2

theorem AnalyticNumberTheory.LargeSieve.vaughanTypeIRowCoefficient_energy_eq (a : ℂ) (b : ℤ → ℂ) (M : ℤ) (L : ℕ) : ∑ n ∈ Finset.Icc (M + 1) (M + ↑L), ‖vaughanTypeIRowCoefficient a b n‖ ^ 2 = ‖a‖ ^ 2 * ∑ n ∈ Finset.Icc (M + 1) (M + ↑L), ‖b n‖ ^ 2

Expanding the fixed Vaughan Type-I row coefficient inserts its outer coefficient energy exactly once.

theorem AnalyticNumberTheory.LargeSieve.highConductorVaughanTypeIRow_squareLedger_le_expanded (R Q L : ℕ) (hQ : 0 < Q) (a : ℂ) (b : ℤ → ℂ) (M : ℤ) : highConductorPrimitiveSquareLedger R Q (highConductorVaughanTypeIRowAmplitude a b M L) ≤ ↑(L.log2 + 1) ^ 2 * primitiveLargeSieveConstant L Q * (‖a‖ ^ 2 * ∑ n ∈ Finset.Icc (M + 1) (M + ↑L), ‖b n‖ ^ 2)

Actual fixed-row high-conductor Type-I square ledger after row-coefficient expansion. This is a direct consequence of character orthogonality/large sieve; there is no conclusion-shaped square-saving premise.

theorem AnalyticNumberTheory.LargeSieve.highConductorVaughanTypeIRow_mean_sq_le (R Q L : ℕ) (hQ : 0 < Q) (a : ℂ) (b : ℤ → ℂ) (M : ℤ) : highConductorPrimitiveMean R Q (highConductorVaughanTypeIRowAmplitude a b M L) ^ 2 ≤ highConductorHarmonicTail R Q * (↑(L.log2 + 1) ^ 2 * primitiveLargeSieveConstant L Q * (‖a‖ ^ 2 * ∑ n ∈ Finset.Icc (M + 1) (M + ↑L), ‖b n‖ ^ 2))

The AP-normalized 1/φ(d) mean for one actual Type-I row. The exact high-conductor restriction survives both Cauchy steps. Its square is controlled by the harmonic tail times the proved, expanded physical row ledger.