Pointwise prefix bounds imply primitive prefix-amplitude bounds

This file is the finite, honest bridge needed by a pointwise Siegel--Walfisz theorem. Its premise bounds every actual twisted prefix through N; it does not assume the maximum that occurs in the conclusion.

theorem AnalyticNumberTheory.LargeSieve.primitivePrefixAmplitude_le_of_pointwise_integerPrefix (a : ℤ → ℂ) (N q : ℕ) (ψ : PrimitiveCharacter q) (B : ℝ) (hpointwise : ∀ y ≤ N, ‖∑ n ∈ Finset.Icc 1 ↑y, a n * ↑ψ ↑n‖ ≤ B) : primitivePrefixAmplitude a N q ψ ≤ B

A bound for every integer prefix, including the empty prefix at y = 0, bounds the square root of the primitive-character prefix-square maximum.

theorem AnalyticNumberTheory.LargeSieve.primitivePrefixAmplitude_vonMangoldt_le_of_pointwise_lambdaCharacterPrefix (N q : ℕ) (ψ : PrimitiveCharacter q) (B : ℝ) (hpointwise : ∀ y ≤ N, ‖lambdaCharacterPrefix y q ↑ψ‖ ≤ B) : primitivePrefixAmplitude vonMangoldtIntegerCoeff N q ψ ≤ B

A uniform pointwise bound for the natural-number Chebyshev twists bounds the primitive prefix amplitude. The conversion uses Λ(0) = 0, the exact cast from [1,y] ⊆ ℕ to [1,(y : ℤ)], and the underlying character ψ.1.

theorem AnalyticNumberTheory.LargeSieve.nonprincipalPrimitivePsiSiegelWalfiszSource_of_pointwise_lambdaCharacterPrefix (hpointwise : ∀ (C D : ℕ), ∃ (K : ℝ), 0 < K ∧ ∀ᶠ (N : ℕ) in Filter.atTop, 2 ≤ N → ∀ d ∈ Finset.Icc 2 (logConductorThreshold N C), ∀ (ψ : PrimitiveCharacter d), ↑ψ ≠ 1 → ∀ y ≤ N, ‖lambdaCharacterPrefix y d ↑ψ‖ ≤ K * ↑N / Real.log ↑N ^ D) : NonprincipalPrimitivePsiSiegelWalfiszSource

A future Siegel--Walfisz theorem uniform in every endpoint y ≤ N feeds directly into the exact nonprincipal primitive source used by Standard BV. The hypothesis is pointwise in y, rather than a renamed amplitude bound.