@[irreducible]

def MathlibNt.SieveTheory.dyadicPrefixBlocks : ℕ → ℕ → List (ℕ × ℕ)

The (ordered) dyadic blocks in the binary decomposition of [start,start+rem). The recursive call is on the remainder after removing the largest dyadic block.

Equations

• MathlibNt.SieveTheory.dyadicPrefixBlocks x✝ 0 = []
• MathlibNt.SieveTheory.dyadicPrefixBlocks x✝ rem.succ = (x✝, 2 ^ Nat.log 2 (rem + 1)) :: MathlibNt.SieveTheory.dyadicPrefixBlocks (x✝ + 2 ^ Nat.log 2 (rem + 1)) (rem + 1 - 2 ^ Nat.log 2 (rem + 1))

def MathlibNt.SieveTheory.dyadicBlockSum {α : Type u_1} [AddCommMonoid α] (f : ℕ → α) (b : ℕ × ℕ) : α

Equations

• MathlibNt.SieveTheory.dyadicBlockSum f b = ∑ n ∈ Finset.Ico b.1 (b.1 + b.2), f n

theorem MathlibNt.SieveTheory.dyadicPrefixBlocks_sum {α : Type u_1} [AddCommMonoid α] (f : ℕ → α) (start rem : ℕ) : (List.map (dyadicBlockSum f) (dyadicPrefixBlocks start rem)).sum = ∑ n ∈ Finset.Ico start (start + rem), f n

theorem MathlibNt.SieveTheory.dyadicPrefixBlocks_card_le (start rem : ℕ) : (dyadicPrefixBlocks start rem).length ≤ 1 + Nat.log 2 rem

theorem MathlibNt.SieveTheory.list_norm_sum_le {α : Type u_1} [SeminormedAddCommGroup α] (l : List α) : ‖l.sum‖ ≤ (List.map norm l).sum

theorem MathlibNt.SieveTheory.list_sq_sum_le (l : List ℝ) : l.sum ^ 2 ≤ ↑l.length * (List.map (fun (x : ℝ) => x ^ 2) l).sum

theorem MathlibNt.SieveTheory.dyadic_prefix_norm_sq_le {α : Type u_1} [SeminormedAddCommGroup α] (f : ℕ → α) (start rem : ℕ) : ‖∑ n ∈ Finset.Ico start (start + rem), f n‖ ^ 2 ≤ ↑(dyadicPrefixBlocks start rem).length * (List.map (fun (b : ℕ × ℕ) => ‖∑ n ∈ Finset.Ico b.1 (b.1 + b.2), f n‖ ^ 2) (dyadicPrefixBlocks start rem)).sum

theorem MathlibNt.SieveTheory.sum_divisors_moebius_complex {d : ℕ} : ∑ e ∈ d.divisors, ↑(ArithmeticFunction.moebius e) = if d = 1 then 1 else 0

theorem MathlibNt.SieveTheory.sum_moebius_if_dvd_eq_coprime {r n : ℕ} (hr : r ≠ 0) : (∑ e ∈ r.divisors, if e ∣ n then ↑(ArithmeticFunction.moebius e) else 0) = if n.Coprime r then 1 else 0

Möbius inversion of the coprimality indicator in the coefficient field used by the character sums.

theorem MathlibNt.SieveTheory.dirichletCharacter_eq_primitive_mul_coprimeIndicator {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (n : ℕ) : χ ↑n = χ.primitiveCharacter ↑n * if n.Coprime (q / χ.conductor) then 1 else 0

An induced character is its primitive character times the exact coprimality indicator for the quotient of its level by its conductor.

theorem MathlibNt.SieveTheory.dirichletCharacter_eq_primitive_mul_moebius {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (n : ℕ) : χ ↑n = χ.primitiveCharacter ↑n * ∑ e ∈ (q / χ.conductor).divisors, if e ∣ n then ↑(ArithmeticFunction.moebius e) else 0

Exact Möbius expansion of the noncoprime correction for an induced Dirichlet character.

theorem MathlibNt.SieveTheory.sum_range_ite_dvd {α : Type u_1} [AddCommMonoid α] (f : ℕ → α) {e : ℕ} (he : 0 < e) (y : ℕ) : (∑ n ∈ Finset.range (y + 1), if e ∣ n then f n else 0) = ∑ m ∈ Finset.range (y / e + 1), f (e * m)

Reindex a finite sum restricted to multiples of e by its quotient.

theorem MathlibNt.SieveTheory.characterPrefixSum_eq_sum_primitive_dilations {q : ℕ} [NeZero q] (a : ℕ → ℂ) (χ : DirichletCharacter ℂ q) (y : ℕ) : ∑ n ∈ Finset.range (y + 1), a n * χ ↑n = ∑ e ∈ (q / χ.conductor).divisors, ↑(ArithmeticFunction.moebius e) * χ.primitiveCharacter ↑e * ∑ m ∈ Finset.range (y / e + 1), a (e * m) * χ.primitiveCharacter ↑m

Conductor-first transfer for one prefix. The noncoprime correction is linearized before any character Cauchy--Schwarz: each divisor e dilates the coefficient sequence and leaves one primitive character sum.

theorem MathlibNt.SieveTheory.dirichletCharacter_norm_le_one (q : ℕ) (χ : DirichletCharacter ℂ q) (a : ZMod q) : ‖χ a‖ ≤ 1

A Dirichlet-character value has norm at most one, including at nonunits.

theorem MathlibNt.SieveTheory.moebius_complex_norm_le_one (e : ℕ) : ‖↑(ArithmeticFunction.moebius e)‖ ≤ 1

The complex cast of the Möbius function has norm at most one.

theorem MathlibNt.SieveTheory.characterPrefixSum_norm_le_sum_primitive_dilations {q : ℕ} [NeZero q] (a : ℕ → ℂ) (χ : DirichletCharacter ℂ q) (y : ℕ) : ‖∑ n ∈ Finset.range (y + 1), a n * χ ↑n‖ ≤ ∑ e ∈ (q / χ.conductor).divisors, ‖∑ m ∈ Finset.range (y / e + 1), a (e * m) * χ.primitiveCharacter ↑m‖

The conductor-first linear transfer for one prefix. Crucially, the triangle inequality is taken only after the exact noncoprime Möbius expansion; no all-character square mean is introduced.

noncomputable def MathlibNt.SieveTheory.characterPrefixSquare (a : ℕ → ℂ) (q y : ℕ) (χ : DirichletCharacter ℂ q) : ℝ

Equations

• MathlibNt.SieveTheory.characterPrefixSquare a q y χ = ‖∑ n ∈ Finset.range y, a n * χ ↑n‖ ^ 2

noncomputable def MathlibNt.SieveTheory.characterPrefixSquareMax (a : ℕ → ℂ) (q N : ℕ) (χ : DirichletCharacter ℂ q) : ℝ

Equations

• MathlibNt.SieveTheory.characterPrefixSquareMax a q N χ = (Finset.image (fun (y : ℕ) => MathlibNt.SieveTheory.characterPrefixSquare a q y χ) (Finset.range (N + 1))).max' ⋯

noncomputable def MathlibNt.SieveTheory.characterDyadicPrefixEnergy (a : ℕ → ℂ) (q y : ℕ) (χ : DirichletCharacter ℂ q) : ℝ

Equations

• MathlibNt.SieveTheory.characterDyadicPrefixEnergy a q y χ = (List.map (fun (b : ℕ × ℕ) => ‖∑ n ∈ Finset.Ico b.1 (b.1 + b.2), a n * χ ↑n‖ ^ 2) (MathlibNt.SieveTheory.dyadicPrefixBlocks 0 y)).sum

noncomputable def MathlibNt.SieveTheory.characterDyadicPrefixEnergyMax (a : ℕ → ℂ) (q N : ℕ) (χ : DirichletCharacter ℂ q) : ℝ

Equations

• MathlibNt.SieveTheory.characterDyadicPrefixEnergyMax a q N χ = (Finset.image (fun (y : ℕ) => MathlibNt.SieveTheory.characterDyadicPrefixEnergy a q y χ) (Finset.range (N + 1))).max' ⋯

theorem MathlibNt.SieveTheory.characterPrefixSquareMax_le_dyadic (a : ℕ → ℂ) (q N : ℕ) (χ : DirichletCharacter ℂ q) : characterPrefixSquareMax a q N χ ≤ ↑(1 + Nat.log 2 (N + 1)) * characterDyadicPrefixEnergyMax a q N χ

The pointwise Rademacher--Menshov reduction. Unlike a maximum taken after the character average, this keeps the prefix maximum inside each primitive character summand, which is the form needed for conductor regrouping.

noncomputable def MathlibNt.SieveTheory.primitiveCharacterPrefixMaxMean (Q : ℕ) (a : ℕ → ℂ) (N : ℕ) : ℝ

Equations

• MathlibNt.SieveTheory.primitiveCharacterPrefixMaxMean Q a N = ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : DirichletCharacter ℂ q with χ.IsPrimitive, MathlibNt.SieveTheory.characterPrefixSquareMax a q N χ

noncomputable def MathlibNt.SieveTheory.primitiveCharacterDyadicMaxMean (Q : ℕ) (a : ℕ → ℂ) (N : ℕ) : ℝ

Equations

• MathlibNt.SieveTheory.primitiveCharacterDyadicMaxMean Q a N = ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : DirichletCharacter ℂ q with χ.IsPrimitive, MathlibNt.SieveTheory.characterDyadicPrefixEnergyMax a q N χ

theorem MathlibNt.SieveTheory.primitiveCharacterPrefixMaxMean_le_dyadic (Q : ℕ) (a : ℕ → ℂ) (N : ℕ) : primitiveCharacterPrefixMaxMean Q a N ≤ ↑(1 + Nat.log 2 (N + 1)) * primitiveCharacterDyadicMaxMean Q a N

Exact primitive-character maximal reduction with the prefix maximum inside the character sum and the original q / φ(q) weight unchanged.

noncomputable def MathlibNt.SieveTheory.natZeroExtension (a : ℕ → ℂ) : ℤ → ℂ

Extend a sequence on the naturals by zero to the integers. This is the coefficient interface required by bombieriDavenport_le.

Equations

• MathlibNt.SieveTheory.natZeroExtension a z = if 0 ≤ z then a z.toNat else 0

theorem MathlibNt.SieveTheory.natZeroExtension_block_sum (a : ℕ → ℂ) (start len q : ℕ) (χ : DirichletCharacter ℂ q) : ∑ z ∈ Finset.Icc (↑start - 1 + 1) (↑start - 1 + ↑len), natZeroExtension a z * χ ↑z = ∑ n ∈ Finset.Ico start (start + len), a n * χ ↑n

theorem MathlibNt.SieveTheory.natZeroExtension_block_norm_sq_sum (a : ℕ → ℂ) (start len : ℕ) : ∑ z ∈ Finset.Icc (↑start - 1 + 1) (↑start - 1 + ↑len), ‖natZeroExtension a z‖ ^ 2 = ∑ n ∈ Finset.Ico start (start + len), ‖a n‖ ^ 2

theorem MathlibNt.SieveTheory.primitiveCharacterBlockMean_le_largeSieve (Q : ℕ) (hQ : 0 < Q) (a : ℕ → ℂ) (start len : ℕ) : ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : DirichletCharacter ℂ q with χ.IsPrimitive, ‖∑ n ∈ Finset.Ico start (start + len), a n * χ ↑n‖ ^ 2 ≤ AnalyticNumberTheory.LargeSieve.largeSieveBound len (1 / ↑Q ^ 2) * ∑ n ∈ Finset.Ico start (start + len), ‖a n‖ ^ 2

Bombieri--Davenport on one natural-number block, retaining exactly the original primitive-character and q / φ(q) weights.

theorem MathlibNt.SieveTheory.dyadicAlignedBlocks_sum {α : Type u_1} [AddCommMonoid α] (f : ℕ → α) (p J : ℕ) : ∑ j ∈ Finset.range J, ∑ n ∈ Finset.Ico (j * p) ((j + 1) * p), f n = ∑ n ∈ Finset.range (J * p), f n

The adjacent aligned blocks of a fixed length partition their union.

theorem MathlibNt.SieveTheory.dyadicAlignedBlocks_energy_le (a : ℕ → ℂ) (N p : ℕ) : ∑ j ∈ Finset.range ((N + 1) / p), ∑ n ∈ Finset.Ico (j * p) ((j + 1) * p), ‖a n‖ ^ 2 ≤ ∑ n ∈ Finset.range (N + 1), ‖a n‖ ^ 2

At a fixed aligned dyadic scale, every coefficient energy is charged at most once.

theorem MathlibNt.SieveTheory.largeSieveBound_mono_length (u v : ℕ) (δ : ℝ) (h : u ≤ v) : AnalyticNumberTheory.LargeSieve.largeSieveBound u δ ≤ AnalyticNumberTheory.LargeSieve.largeSieveBound v δ

theorem MathlibNt.SieveTheory.primitiveCharacterAlignedDyadicBlockMean_le (Q : ℕ) (hQ : 0 < Q) (a : ℕ → ℂ) (N p : ℕ) (hp : p ≤ N + 1) : ∑ j ∈ Finset.range ((N + 1) / p), ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : DirichletCharacter ℂ q with χ.IsPrimitive, ‖∑ n ∈ Finset.Ico (j * p) ((j + 1) * p), a n * χ ↑n‖ ^ 2 ≤ AnalyticNumberTheory.LargeSieve.largeSieveBound (N + 1) (1 / ↑Q ^ 2) * ∑ n ∈ Finset.range (N + 1), ‖a n‖ ^ 2

The primitive-character square mean over all aligned blocks at one scale. The coefficient energy occurs only once, rather than once for every prefix.

theorem MathlibNt.SieveTheory.primitiveCharacterAlignedDyadicMean_le (Q : ℕ) (hQ : 0 < Q) (a : ℕ → ℂ) (N : ℕ) : ∑ k ∈ Finset.range (1 + Nat.log 2 (N + 1)), ∑ j ∈ Finset.range ((N + 1) / 2 ^ k), ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : DirichletCharacter ℂ q with χ.IsPrimitive, ‖∑ n ∈ Finset.Ico (j * 2 ^ k) ((j + 1) * 2 ^ k), a n * χ ↑n‖ ^ 2 ≤ ↑(1 + Nat.log 2 (N + 1)) * (AnalyticNumberTheory.LargeSieve.largeSieveBound (N + 1) (1 / ↑Q ^ 2) * ∑ n ∈ Finset.range (N + 1), ‖a n‖ ^ 2)

Summing the aligned block estimate through the binary scales costs just one fixed logarithmic factor.

theorem MathlibNt.SieveTheory.dyadicPrefixBlocks_start_le (start rem : ℕ) (b : ℕ × ℕ) (hb : b ∈ dyadicPrefixBlocks start rem) : start ≤ b.1

Every block in the recursive decomposition starts no earlier than the left endpoint of the interval being decomposed.

theorem MathlibNt.SieveTheory.dyadicPrefixBlocks_nodup (start rem : ℕ) : (dyadicPrefixBlocks start rem).Nodup

theorem MathlibNt.SieveTheory.dyadicPrefixBlocks_aligned_aux (rem K start : ℕ) (hstart : 2 ^ K ∣ start) (hlog : Nat.log 2 rem ≤ K) (b : ℕ × ℕ) (hb : b ∈ dyadicPrefixBlocks start rem) : ∃ k ≤ K, b.2 = 2 ^ k ∧ 2 ^ k ∣ b.1 ∧ b.1 + b.2 ≤ start + rem

Alignment, scale control, and containment in the original interval for each recursively selected dyadic block.

theorem MathlibNt.SieveTheory.dyadicPrefixBlocks_aligned (y : ℕ) (b : ℕ × ℕ) (hb : b ∈ dyadicPrefixBlocks 0 y) : ∃ k ≤ Nat.log 2 y, b.2 = 2 ^ k ∧ 2 ^ k ∣ b.1 ∧ b.1 + b.2 ≤ y

noncomputable def MathlibNt.SieveTheory.alignedDyadicBlockIndices (N : ℕ) : Finset ((_ : ℕ) × ℕ)

Equations

• MathlibNt.SieveTheory.alignedDyadicBlockIndices N = (Finset.range (1 + Nat.log 2 (N + 1))).sigma fun (k : ℕ) => Finset.range ((N + 1) / 2 ^ k)

noncomputable def MathlibNt.SieveTheory.alignedDyadicBlockEmbedding : (_ : ℕ) × ℕ ↪ ℕ × ℕ

Equations

• MathlibNt.SieveTheory.alignedDyadicBlockEmbedding = { toFun := fun (x : (_ : ℕ) × ℕ) => (x.snd * 2 ^ x.fst, 2 ^ x.fst), inj' := MathlibNt.SieveTheory.alignedDyadicBlockEmbedding._proof_2 }

theorem MathlibNt.SieveTheory.dyadicPrefixBlock_mem_alignedDyadicBlockIndices (N y : ℕ) (hy : y ≤ N) (b : ℕ × ℕ) (hb : b ∈ dyadicPrefixBlocks 0 y) : ∃ x ∈ alignedDyadicBlockIndices N, alignedDyadicBlockEmbedding x = b

theorem MathlibNt.SieveTheory.alignedDyadicBlockIndices_sum (N : ℕ) (f : ℕ × ℕ → ℝ) : ∑ b ∈ Finset.map alignedDyadicBlockEmbedding (alignedDyadicBlockIndices N), f b = ∑ k ∈ Finset.range (1 + Nat.log 2 (N + 1)), ∑ j ∈ Finset.range ((N + 1) / 2 ^ k), f (j * 2 ^ k, 2 ^ k)

theorem MathlibNt.SieveTheory.characterDyadicPrefixEnergy_le_aligned (a : ℕ → ℂ) (q N y : ℕ) (χ : DirichletCharacter ℂ q) (hy : y ≤ N) : characterDyadicPrefixEnergy a q y χ ≤ ∑ b ∈ Finset.map alignedDyadicBlockEmbedding (alignedDyadicBlockIndices N), ‖∑ n ∈ Finset.Ico b.1 (b.1 + b.2), a n * χ ↑n‖ ^ 2

theorem MathlibNt.SieveTheory.characterDyadicPrefixEnergyMax_le_aligned (a : ℕ → ℂ) (q N : ℕ) (χ : DirichletCharacter ℂ q) : characterDyadicPrefixEnergyMax a q N χ ≤ ∑ b ∈ Finset.map alignedDyadicBlockEmbedding (alignedDyadicBlockIndices N), ‖∑ n ∈ Finset.Ico b.1 (b.1 + b.2), a n * χ ↑n‖ ^ 2

theorem MathlibNt.SieveTheory.primitiveCharacterDyadicMaxMean_le_alignedIndices (Q : ℕ) (a : ℕ → ℂ) (N : ℕ) : primitiveCharacterDyadicMaxMean Q a N ≤ ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : DirichletCharacter ℂ q with χ.IsPrimitive, ∑ b ∈ Finset.map alignedDyadicBlockEmbedding (alignedDyadicBlockIndices N), ‖∑ n ∈ Finset.Ico b.1 (b.1 + b.2), a n * χ ↑n‖ ^ 2

theorem MathlibNt.SieveTheory.dependent_sum_comm {α : Type u_1} {γ : Type u_2} {δ : Type u_3} {β : α → Type u_4} [AddCommMonoid δ] (s : Finset α) (t : (a : α) → Finset (β a)) (u : Finset γ) (f : (a : α) → β a → γ → δ) : ∑ a ∈ s, ∑ b ∈ t a, ∑ c ∈ u, f a b c = ∑ c ∈ u, ∑ a ∈ s, ∑ b ∈ t a, f a b c

theorem MathlibNt.SieveTheory.primitiveCharacterDyadicMaxMean_le_aligned (Q : ℕ) (a : ℕ → ℂ) (N : ℕ) : primitiveCharacterDyadicMaxMean Q a N ≤ ∑ k ∈ Finset.range (1 + Nat.log 2 (N + 1)), ∑ j ∈ Finset.range ((N + 1) / 2 ^ k), ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : DirichletCharacter ℂ q with χ.IsPrimitive, ‖∑ n ∈ Finset.Ico (j * 2 ^ k) ((j + 1) * 2 ^ k), a n * χ ↑n‖ ^ 2

The existing dyadic-prefix maximum is controlled by the aligned block family. The latter has one copy of the coefficient energy at each scale.

theorem MathlibNt.SieveTheory.primitiveCharacterPrefixMaxMean_le_largeSieve (Q : ℕ) (hQ : 0 < Q) (a : ℕ → ℂ) (N : ℕ) : primitiveCharacterPrefixMaxMean Q a N ≤ ↑(1 + Nat.log 2 (N + 1)) ^ 2 * (AnalyticNumberTheory.LargeSieve.largeSieveBound (N + 1) (1 / ↑Q ^ 2) * ∑ n ∈ Finset.range (N + 1), ‖a n‖ ^ 2)

End-to-end maximal Bombieri--Davenport estimate for natural coefficients. The two fixed logarithmic factors respectively come from the prefix Rademacher--Menshov reduction and the aligned dyadic scales.

theorem MathlibNt.SieveTheory.characterPrefixSquareMax_truncate (a : ℕ → ℂ) (q N : ℕ) (χ : DirichletCharacter ℂ q) : characterPrefixSquareMax (fun (n : ℕ) => if n < N then a n else 0) q N χ = characterPrefixSquareMax a q N χ

Truncating a coefficient sequence at the largest index used by a prefix maximum does not change that maximum.

theorem MathlibNt.SieveTheory.primitiveCharacterPrefixMaxMean_le_largeSieve_exact (Q : ℕ) (hQ : 0 < Q) (a : ℕ → ℂ) (N : ℕ) : primitiveCharacterPrefixMaxMean Q a N ≤ ↑(1 + Nat.log 2 (N + 1)) ^ 2 * (AnalyticNumberTheory.LargeSieve.largeSieveBound (N + 1) (1 / ↑Q ^ 2) * ∑ n ∈ Finset.range N, ‖a n‖ ^ 2)

The maximal large sieve only charges coefficients actually occurring in its prefixes; the apparent final endpoint in the aligned-block proof is removable by truncation.

theorem MathlibNt.SieveTheory.largeSieveBound_le_mul_log_of_sq_le (N Q : ℕ) (hN : 1 ≤ N) (hQ : 0 < Q) (hQsq : Q ^ 2 ≤ N) : AnalyticNumberTheory.LargeSieve.largeSieveBound (N + 2) (1 / ↑Q ^ 2) ≤ (17 + 4 / Real.log 2) * ↑N * Real.log ↑(N + 2)

At square-root conductor range, the explicit weak large-sieve constant costs only one logarithm.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerDilatedCoefficientEnergy_le (N e : ℕ) (he : 0 < e) : ∑ m ∈ Finset.range (N / e + 1), ‖↑(liuPanPrimePowerCoefficient N (e * m))‖ ^ 2 ≤ ∑ n ∈ Finset.range (N + 1), liuPanPrimePowerCoefficient N n ^ 2

A positive dilation selects distinct coefficients from the original [0,N] energy and therefore cannot increase its square mass.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerDilatedPrefixMaxMean_le_largeSieve (N Q e : ℕ) (hQ : 0 < Q) (he : 0 < e) : primitiveCharacterPrefixMaxMean Q (fun (m : ℕ) => ↑(liuPanPrimePowerCoefficient N (e * m))) (N / e + 1) ≤ ↑(1 + Nat.log 2 (N / e + 2)) ^ 2 * (AnalyticNumberTheory.LargeSieve.largeSieveBound (N / e + 2) (1 / ↑Q ^ 2) * ∑ n ∈ Finset.range (N + 1), liuPanPrimePowerCoefficient N n ^ 2)

The maximal primitive mean of every positive dilation is controlled by the same undilated coefficient energy.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerDilatedPrefixMaxMean_sqrt_le (N Q e : ℕ) (hQ : 0 < Q) (he : 0 < e) : √(primitiveCharacterPrefixMaxMean Q (fun (m : ℕ) => ↑(liuPanPrimePowerCoefficient N (e * m))) (N / e + 1)) ≤ ↑(1 + Nat.log 2 (N + 2)) * √(AnalyticNumberTheory.LargeSieve.largeSieveBound (N + 2) (1 / ↑Q ^ 2) * ∑ n ∈ Finset.range (N + 1), liuPanPrimePowerCoefficient N n ^ 2)

After taking square roots, every positive dilation has one common large-sieve and dyadic factor.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerNonprincipalCharacters (q : ℕ) : Finset (DirichletCharacter ℂ q)

The finite set of genuinely nonprincipal characters at a fixed level.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerNonprincipalCharacters q = Finset.univ.erase 1

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerInducedPrefixUpper (N q : ℕ) (χ : DirichletCharacter ℂ q) : ℝ

The primitive-prefix majorant obtained from one induced character after the exact Möbius dilation expansion.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerInducedPrefixUpper N q χ = ∑ e ∈ (q / χ.conductor).divisors, √(MathlibNt.SieveTheory.characterPrefixSquareMax (fun (m : ℕ) => ↑(MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerCoefficient N (e * m))) χ.conductor (N / e + 1) χ.primitiveCharacter)

theorem MathlibNt.SieveTheory.LiuWeight.characterPrefixNorm_le_sqrt_squareMax (a : ℕ → ℂ) (q N y : ℕ) (χ : DirichletCharacter ℂ q) (hy : y ≤ N) : ‖∑ n ∈ Finset.range y, a n * χ ↑n‖ ≤ √(characterPrefixSquareMax a q N χ)

A prefix norm is bounded by the square root of its finite prefix-square maximum.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerCharacterPrefixNorm_le_inducedPrefixUpper {N y q : ℕ} (hq : 0 < q) (hy : y ≤ N) (χ : DirichletCharacter ℂ q) : ‖∑ n ∈ Finset.range (y + 1), ↑(liuPanPrimePowerCoefficient N n) * χ ↑n‖ ≤ liuPanPrimePowerInducedPrefixUpper N q χ

Every induced-character prefix is bounded linearly by primitive prefixes of the dilated coefficient sequences.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerNonprincipalDiscrepancy_abs_le_characterPrefixNormSum {N y q l : ℕ} (hq : 0 < q) (hl : IsUnit ↑l) : |liuPanPrimePowerNonprincipalDiscrepancy N y q l| ≤ (↑q.totient)⁻¹ * ∑ χ ∈ liuPanPrimePowerNonprincipalCharacters q, ‖∑ n ∈ Finset.range (y + 1), ↑(liuPanPrimePowerCoefficient N n) * χ ↑n‖

Triangle inequality for the exact nonprincipal character expansion, before any Cauchy--Schwarz step.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerNonprincipalDiscrepancyMaxY_le_inducedPrefixUpper (N q : ℕ) (hq : 0 < q) : liuPanPrimePowerNonprincipalDiscrepancyMaxY N q ≤ (↑q.totient)⁻¹ * ∑ χ ∈ liuPanPrimePowerNonprincipalCharacters q, liuPanPrimePowerInducedPrefixUpper N q χ

The maximum over residue classes and prefixes is bounded before conductor regrouping by the linear induced-character primitive-prefix majorant.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerInducedPrefixTransfer (N Q : ℕ) : ℝ

The finite linear transfer that still retains every inducing level and character. Its conductor regrouping is an exact finite reindexing.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerInducedPrefixTransfer N Q = ∑ q ∈ Finset.Icc 1 Q, MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerModulusWeight q * (↑q.totient)⁻¹ * ∑ χ ∈ MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerNonprincipalCharacters q, MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerInducedPrefixUpper N q χ

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerConductorPrefixTransfer (N Q : ℕ) : ℝ

The same finite transfer regrouped first by primitive conductor. Inducing levels and their character fibers remain explicit.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerConductorPrefixTransfer N Q = ∑ d ∈ Finset.Icc 1 Q, ∑ q ∈ Finset.Icc 1 Q, MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerModulusWeight q * (↑q.totient)⁻¹ * ∑ χ ∈ MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerNonprincipalCharacters q with χ.conductor = d, MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerInducedPrefixUpper N q χ

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerPrimitiveCharacters (d : ℕ) : Finset (DirichletCharacter ℂ d)

The primitive characters at an exact conductor.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerPrimitiveCharacters d = {χ : DirichletCharacter ℂ d | χ.IsPrimitive}

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerPrimitiveCharacterLifts (q d : ℕ) (hdq : d ∣ q) : Finset (DirichletCharacter ℂ q)

Primitive characters of conductor d, lifted to a fixed multiple q.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerPrimitiveCharacterLifts q d hdq = Finset.image (⇑(DirichletCharacter.changeLevel hdq)) (MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerPrimitiveCharacters d)

theorem MathlibNt.SieveTheory.LiuWeight.primitiveCharacter_apply_eq_self_of_isPrimitive {d : ℕ} (ψ : DirichletCharacter ℂ d) (hψ : ψ.IsPrimitive) (a : ℤ) : ψ.primitiveCharacter ↑a = ψ ↑a

A primitive character agrees pointwise with its canonical primitive character. The pointwise form avoids transporting across conductor equality.

theorem MathlibNt.SieveTheory.LiuWeight.characterPrefixSquare_changeLevel_primitive {a : ℕ → ℂ} {q d y : ℕ} [NeZero q] (hdq : d ∣ q) (ψ : DirichletCharacter ℂ d) (hψ : ψ.IsPrimitive) : characterPrefixSquare a ((DirichletCharacter.changeLevel hdq) ψ).conductor y ((DirichletCharacter.changeLevel hdq) ψ).primitiveCharacter = characterPrefixSquare a d y ψ

Prefix squares of the primitive character underlying a lifted primitive character are exactly the original primitive-character prefix squares.

theorem MathlibNt.SieveTheory.LiuWeight.characterPrefixSquareMax_changeLevel_primitive {a : ℕ → ℂ} {q d M : ℕ} [NeZero q] (hdq : d ∣ q) (ψ : DirichletCharacter ℂ d) (hψ : ψ.IsPrimitive) : characterPrefixSquareMax a ((DirichletCharacter.changeLevel hdq) ψ).conductor M ((DirichletCharacter.changeLevel hdq) ψ).primitiveCharacter = characterPrefixSquareMax a d M ψ

The finite prefix-square maximum is unchanged when the character is first lifted and then canonically reduced to its primitive conductor.

theorem MathlibNt.SieveTheory.LiuWeight.characterPrefixSquareMax_nonneg (a : ℕ → ℂ) (q N : ℕ) (χ : DirichletCharacter ℂ q) : 0 ≤ characterPrefixSquareMax a q N χ

Prefix-square maxima are nonnegative.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerPrimitiveCharacters_card_le_totient (d : ℕ) [NeZero d] : (liuPanPrimePowerPrimitiveCharacters d).card ≤ d.totient

The primitive characters form a subset of all characters, whose cardinality is Euler's totient.

theorem MathlibNt.SieveTheory.LiuWeight.primitiveCharacterPrefixSqrtSum_le (a : ℕ → ℂ) (d M : ℕ) [NeZero d] : ∑ ψ ∈ liuPanPrimePowerPrimitiveCharacters d, √(characterPrefixSquareMax a d M ψ) ≤ √↑d.totient * √(∑ ψ ∈ liuPanPrimePowerPrimitiveCharacters d, characterPrefixSquareMax a d M ψ)

Cauchy--Schwarz over the primitive characters at one exact conductor.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerInducedPrefixUpper_changeLevel_primitive {N q d : ℕ} [NeZero q] (hdq : d ∣ q) (ψ : DirichletCharacter ℂ d) (hψ : ψ.IsPrimitive) : liuPanPrimePowerInducedPrefixUpper N q ((DirichletCharacter.changeLevel hdq) ψ) = ∑ e ∈ (q / d).divisors, √(characterPrefixSquareMax (fun (m : ℕ) => ↑(liuPanPrimePowerCoefficient N (e * m))) d (N / e + 1) ψ)

Normalization of every lifted induced upper bound to the original primitive character and the explicit conductor quotient.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerNonprincipalCharacters_filter_conductor_eq_lifts (q d : ℕ) [NeZero q] (hdq : d ∣ q) (hd : 1 < d) : {χ ∈ liuPanPrimePowerNonprincipalCharacters q | χ.conductor = d} = liuPanPrimePowerPrimitiveCharacterLifts q d hdq

At a fixed positive level and conductor greater than one, the conductor fiber is exactly the injective image of primitive characters.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerInducedPrefixUpper_sum_conductor_eq_primitive_lifts (N q d : ℕ) [NeZero q] (hdq : d ∣ q) (hd : 1 < d) : ∑ χ ∈ liuPanPrimePowerNonprincipalCharacters q with χ.conductor = d, liuPanPrimePowerInducedPrefixUpper N q χ = ∑ ψ ∈ liuPanPrimePowerPrimitiveCharacters d, liuPanPrimePowerInducedPrefixUpper N q ((DirichletCharacter.changeLevel hdq) ψ)

Reindexing a fixed conductor fiber loses no multiplicity: every induced character is represented by exactly one primitive character.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerPrimitiveLiftPrefixTransfer (N Q : ℕ) : ℝ

The conductor-first transfer after exact reindexing by primitive characters. Divisibility of the conductor into the inducing level and the conductor-one exclusion remain explicit.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerPrimitiveLiftPrefixTransfer N Q = ∑ d ∈ Finset.Icc 1 Q, ∑ q ∈ Finset.Icc 1 Q, MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerModulusWeight q * (↑q.totient)⁻¹ * if _hd1 : d = 1 then 0 else if hdq : d ∣ q then ∑ ψ ∈ MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerPrimitiveCharacters d, MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerInducedPrefixUpper N q ((DirichletCharacter.changeLevel hdq) ψ) else 0

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerPrimitiveDilationPrefixTransfer (N Q : ℕ) : ℝ

The primitive-lift transfer after removing all dependent conductor transports. Every remaining term is a prefix maximum at the explicit conductor d for a dilated coefficient sequence.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerPrimitiveDilationPrefixTransfer N Q = ∑ d ∈ Finset.Icc 1 Q, ∑ q ∈ Finset.Icc 1 Q, MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerModulusWeight q * (↑q.totient)⁻¹ * if d = 1 then 0 else if d ∣ q then ∑ ψ ∈ MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerPrimitiveCharacters d, ∑ e ∈ (q / d).divisors, √(MathlibNt.SieveTheory.characterPrefixSquareMax (fun (m : ℕ) => ↑(MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerCoefficient N (e * m))) d (N / e + 1) ψ) else 0

theorem MathlibNt.SieveTheory.LiuWeight.sum_Icc_dvd_eq_sum_Icc_div (Q d : ℕ) (hd : 0 < d) (f : ℕ → ℝ) : (∑ q ∈ Finset.Icc 1 Q, if d ∣ q then f q else 0) = ∑ r ∈ Finset.Icc 1 (Q / d), f (d * r)

Positive multiples of d in [1, Q] are uniquely parametrized by their positive cofactors in [1, Q / d].

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerCofactorWeightSum_le_H3Mass (Q e : ℕ) : (∑ r ∈ Finset.Icc 1 Q, if e ∣ r then liuPanPrimePowerModulusWeight (r / e) / ↑(r / e).totient else 0) ≤ liuPanPrimePowerH3Mass Q

Summing the complementary cofactor weight over multiples of a fixed divisor costs at most the finite H₃ mass.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerModulusWeight_div_totient_le_three_factors {d r e : ℕ} (he : e ∣ r) : liuPanPrimePowerModulusWeight (d * r) / ↑(d * r).totient ≤ liuPanPrimePowerModulusWeight d / ↑d.totient * (liuPanPrimePowerModulusWeight e / ↑e.totient) * (liuPanPrimePowerModulusWeight (r / e) / ↑(r / e).totient)

The three-factor decomposition remains an upper bound without a squarefree hypothesis, because nonsquarefree product weights vanish.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerCofactorDilationPrefixTransfer (N Q : ℕ) : ℝ

The primitive dilation transfer with inducing levels written uniquely as q = d * r. This removes the divisibility branch while retaining the conductor-one exclusion and every cofactor/divisor multiplicity.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerCofactorDilationPrefixTransfer N Q = ∑ d ∈ Finset.Icc 1 Q, if d = 1 then 0 else ∑ r ∈ Finset.Icc 1 (Q / d), MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerModulusWeight (d * r) * (↑(d * r).totient)⁻¹ * ∑ ψ ∈ MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerPrimitiveCharacters d, ∑ e ∈ r.divisors, √(MathlibNt.SieveTheory.characterPrefixSquareMax (fun (m : ℕ) => ↑(MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerCoefficient N (e * m))) d (N / e + 1) ψ)

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerH3DilationPrefixTransfer (N Q : ℕ) : ℝ

The conductor/dilation functional left after the complementary cofactor has been summed under H₃.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerH3DilationPrefixTransfer N Q = MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerH3Mass Q * ∑ d ∈ Finset.Icc 2 Q, MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerModulusWeight d / ↑d.totient * ∑ e ∈ Finset.Icc 1 Q, MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerModulusWeight e / ↑e.totient * ∑ ψ ∈ MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerPrimitiveCharacters d, √(MathlibNt.SieveTheory.characterPrefixSquareMax (fun (m : ℕ) => ↑(MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerCoefficient N (e * m))) d (N / e + 1) ψ)

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerPrimitiveCauchyPrefixTransfer (N Q : ℕ) : ℝ

The post-primitive-character Cauchy functional, arranged with the dilation outside so that the remaining Cauchy--Schwarz inequality is over conductors.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerPrimitiveCauchyPrefixTransfer N Q = MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerH3Mass Q * ∑ e ∈ Finset.Icc 1 Q, MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerModulusWeight e / ↑e.totient * ∑ d ∈ Finset.Icc 2 Q, MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerModulusWeight d / ↑d.totient * √↑d.totient * √(∑ ψ ∈ MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerPrimitiveCharacters d, MathlibNt.SieveTheory.characterPrefixSquareMax (fun (m : ℕ) => ↑(MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerCoefficient N (e * m))) d (N / e + 1) ψ)

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerWeight_sqrt_totient_factor {d : ℕ} (hd : 0 < d) : liuPanPrimePowerModulusWeight d / ↑d.totient * √↑d.totient = √(liuPanPrimePowerModulusWeight d ^ 2 / ↑d) * √(↑d / ↑d.totient)

Algebraic square-root factorization that aligns the conductor coefficient with J₉ and the d / φ(d) primitive large-sieve weight.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerModulusWeight_sq_div_eq_J9_term (d : ℕ) : liuPanPrimePowerModulusWeight d ^ 2 / ↑d = ↑(ArithmeticFunction.moebius d) ^ 2 * 9 ^ d.primeFactors.card / ↑d

Squaring the squarefree modulus weight gives exactly the J₉ summand.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerConductorWeightSqSum_le_J9Mass (Q : ℕ) : ∑ d ∈ Finset.Icc 2 Q, liuPanPrimePowerModulusWeight d ^ 2 / ↑d ≤ liuPanPrimePowerJ9Mass Q

The conductor square mass on [2,Q] is contained in the finite J₉ mass.

theorem MathlibNt.SieveTheory.LiuWeight.primitiveCharacterPrefixMaxMean_Icc_two_le (Q : ℕ) (a : ℕ → ℂ) (M : ℕ) : ∑ d ∈ Finset.Icc 2 Q, ↑d / ↑d.totient * ∑ ψ ∈ liuPanPrimePowerPrimitiveCharacters d, characterPrefixSquareMax a d M ψ ≤ primitiveCharacterPrefixMaxMean Q a M

Restricting the primitive maximal mean to conductors at least two can only decrease it.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerH3J9PrefixTransfer (N Q : ℕ) : ℝ

The exact finite target after both Cauchy--Schwarz steps. It contains only the H₃ and J₉ masses and the already established primitive maximal mean.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerH3J9PrefixTransfer N Q = MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerH3Mass Q * ∑ e ∈ Finset.Icc 1 Q, MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerModulusWeight e / ↑e.totient * (√(MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerJ9Mass Q) * √(MathlibNt.SieveTheory.primitiveCharacterPrefixMaxMean Q (fun (m : ℕ) => ↑(MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerCoefficient N (e * m))) (N / e + 1)))

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerModulusWeightSum_le_H3Mass (Q : ℕ) : ∑ e ∈ Finset.Icc 1 Q, liuPanPrimePowerModulusWeight e / ↑e.totient ≤ liuPanPrimePowerH3Mass Q

The positive dilation weights on [1,Q] are contained in H₃(Q).

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerH3J9PrefixTransfer_le_largeSieve (N Q : ℕ) (hQ : 0 < Q) : liuPanPrimePowerH3J9PrefixTransfer N Q ≤ liuPanPrimePowerH3Mass Q ^ 2 * √(liuPanPrimePowerJ9Mass Q) * (↑(1 + Nat.log 2 (N + 2)) * √(AnalyticNumberTheory.LargeSieve.largeSieveBound (N + 2) (1 / ↑Q ^ 2) * ∑ n ∈ Finset.range (N + 1), liuPanPrimePowerCoefficient N n ^ 2))

All primitive means in the exact H₃/J₉ transfer are bounded by one global coefficient energy and one common large-sieve factor.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerCofactorSum_le_H3Mass (Q d : ℕ) (F : ℕ → ℝ) (hF : ∀ (e : ℕ), 0 ≤ F e) : ∑ r ∈ Finset.Icc 1 (Q / d), liuPanPrimePowerModulusWeight (d * r) / ↑(d * r).totient * ∑ e ∈ r.divisors, F e ≤ liuPanPrimePowerH3Mass Q * (liuPanPrimePowerModulusWeight d / ↑d.totient) * ∑ e ∈ Finset.Icc 1 Q, liuPanPrimePowerModulusWeight e / ↑e.totient * F e

Abstract cofactor summation: after the squarefree three-factor estimate, the complementary quotient is absorbed by H₃.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerCofactorDilationPrefixTransfer_le_H3 (N Q : ℕ) : liuPanPrimePowerCofactorDilationPrefixTransfer N Q ≤ liuPanPrimePowerH3DilationPrefixTransfer N Q

The exact cofactor transfer is bounded by the explicit post-H₃ conductor/dilation functional.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerH3DilationPrefixTransfer_le_primitiveCauchy (N Q : ℕ) : liuPanPrimePowerH3DilationPrefixTransfer N Q ≤ liuPanPrimePowerPrimitiveCauchyPrefixTransfer N Q

Cauchy--Schwarz over the primitive characters at each exact conductor, without summing over inducing levels first.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerPrimitiveCauchyPrefixTransfer_le_H3_J9 (N Q : ℕ) : liuPanPrimePowerPrimitiveCauchyPrefixTransfer N Q ≤ liuPanPrimePowerH3J9PrefixTransfer N Q

Cauchy--Schwarz over conductors gives the exact finite H₃/J₉ primitive-maximal functional.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerPrimitiveDilationPrefixTransfer_eq_cofactor (N Q : ℕ) : liuPanPrimePowerPrimitiveDilationPrefixTransfer N Q = liuPanPrimePowerCofactorDilationPrefixTransfer N Q

Exact conductor/cofactor reindexing of the primitive dilation transfer.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerPrimitiveDilationPrefixTransfer_le_H3_J9 (N Q : ℕ) : liuPanPrimePowerPrimitiveDilationPrefixTransfer N Q ≤ liuPanPrimePowerH3J9PrefixTransfer N Q

Full exact finite reduction of the primitive dilation transfer to the H₃/J₉ masses and primitive maximal large-sieve means.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerPrimitiveLiftPrefixTransfer_eq_dilation (N Q : ℕ) : liuPanPrimePowerPrimitiveLiftPrefixTransfer N Q = liuPanPrimePowerPrimitiveDilationPrefixTransfer N Q

Exact normalization of the conductor-first lift transfer.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerNonprincipalCharacters_filter_conductor_one (q : ℕ) [NeZero q] : {χ ∈ liuPanPrimePowerNonprincipalCharacters q | χ.conductor = 1} = ∅

The conductor-one fiber is absent from every positive-level nonprincipal character set.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerConductorPrefixTransfer_eq_primitiveLiftPrefixTransfer (N Q : ℕ) : liuPanPrimePowerConductorPrefixTransfer N Q = liuPanPrimePowerPrimitiveLiftPrefixTransfer N Q

Exact primitive-character reindexing of the whole conductor transfer. No character or inducing-level multiplicity is discarded.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerInducedPrefixTransfer_eq_conductorPrefixTransfer (N Q : ℕ) : liuPanPrimePowerInducedPrefixTransfer N Q = liuPanPrimePowerConductorPrefixTransfer N Q

Exact finite conductor regrouping, with no character multiplicity or coprimality factor suppressed.

theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanPrimePowerCharacterNoncoprimeResidual_le_inducedPrefixTransfer (N : ℕ) (B : ℝ) : liuMainPanPrimePowerCharacterNoncoprimeResidual N B ≤ liuPanPrimePowerInducedPrefixTransfer N (panModulusCutoff N B)

The original residual is bounded by the finite induced-character transfer. The modulus-zero term is annihilated by its weight; modulus one contributes no nonprincipal character.

theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanPrimePowerCharacterNoncoprimeResidual_le_conductorPrefixTransfer (N : ℕ) (B : ℝ) : liuMainPanPrimePowerCharacterNoncoprimeResidual N B ≤ liuPanPrimePowerConductorPrefixTransfer N (panModulusCutoff N B)

Conductor-first form of the exact residual transfer.

theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanPrimePowerCharacterNoncoprimeResidual_le_primitiveLiftPrefixTransfer (N : ℕ) (B : ℝ) : liuMainPanPrimePowerCharacterNoncoprimeResidual N B ≤ liuPanPrimePowerPrimitiveLiftPrefixTransfer N (panModulusCutoff N B)

The original residual transferred all the way to uniquely indexed primitive characters, while retaining every inducing level and Möbius dilation.

theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanPrimePowerCharacterNoncoprimeResidual_le_H3_J9 (N : ℕ) (B : ℝ) : liuMainPanPrimePowerCharacterNoncoprimeResidual N B ≤ liuPanPrimePowerH3J9PrefixTransfer N (panModulusCutoff N B)

Exact finite H₃/J₉ maximal large-sieve reduction for the original nonprincipal prime-power residual.

theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanPrimePowerCharacterNoncoprimeResidual_eq_zero_of_cutoff_eq_zero (N : ℕ) (B : ℝ) (hQ : panModulusCutoff N B = 0) : liuMainPanPrimePowerCharacterNoncoprimeResidual N B = 0

A zero conductor cutoff leaves only modulus zero, whose Möbius weight annihilates the residual.

theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanPrimePowerCharacterNoncoprimeResidual_le_largeSieveEnergy (N : ℕ) (B : ℝ) (hQ : 0 < panModulusCutoff N B) : liuMainPanPrimePowerCharacterNoncoprimeResidual N B ≤ liuPanPrimePowerH3Mass (panModulusCutoff N B) ^ 2 * √(liuPanPrimePowerJ9Mass (panModulusCutoff N B)) * (↑(1 + Nat.log 2 (N + 2)) * √(AnalyticNumberTheory.LargeSieve.largeSieveBound (N + 2) (1 / ↑(panModulusCutoff N B) ^ 2) * ∑ n ∈ Finset.range (N + 1), liuPanPrimePowerCoefficient N n ^ 2))

The original residual is bounded by one explicit maximal large-sieve factor and the global square mass of the collected source coefficient.

theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanPrimePowerCharacterNoncoprimeResidual_le_largeSieveCoefficientBound : ∃ (C : ℝ), 0 < C ∧ ∀ (N : ℕ) (B : ℝ), 8 ≤ N → 0 < panModulusCutoff N B → liuMainPanPrimePowerCharacterNoncoprimeResidual N B ≤ liuPanPrimePowerH3Mass (panModulusCutoff N B) ^ 2 * √(liuPanPrimePowerJ9Mass (panModulusCutoff N B)) * (↑(1 + Nat.log 2 (N + 2)) * √(AnalyticNumberTheory.LargeSieve.largeSieveBound (N + 2) (1 / ↑(panModulusCutoff N B) ^ 2) * ((1 + (Real.log ↑(N + 1) / Real.log 2) ^ 2) * (C * ↑N ^ (107 / 120)))))

Substituting the source coefficient's L² estimate leaves only explicit scalar factors in the residual bound.

theorem MathlibNt.SieveTheory.LiuWeight.panModulusCutoff_sq_le (N : ℕ) (B : ℝ) (hN : 3 ≤ N) (hB : 0 ≤ B) : panModulusCutoff N B ^ 2 ≤ N

For nonnegative logarithmic cutoff exponent, the Pan conductor range lies inside the square-root range.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimePower_cutoff_log_add_two_le_two_mul_log (N : ℕ) (B : ℝ) (hN : 3 ≤ N) (hB : 0 ≤ B) : Real.log ↑(panModulusCutoff N B + 2) ≤ 2 * Real.log ↑N

theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanPrimePowerCharacterNoncoprimeResidual_le_explicitScalar : ∃ (C : ℝ), 0 < C ∧ ∀ (N : ℕ) (B : ℝ), 8 ≤ N → 0 ≤ B → 0 < panModulusCutoff N B → liuMainPanPrimePowerCharacterNoncoprimeResidual N B ≤ liuPanPrimePowerH3Mass (panModulusCutoff N B) ^ 2 * √(liuPanPrimePowerJ9Mass (panModulusCutoff N B)) * (↑(1 + Nat.log 2 (N + 2)) * √((17 + 4 / Real.log 2) * ↑N * Real.log ↑(N + 2) * ((1 + (Real.log ↑(N + 1) / Real.log 2) ^ 2) * (C * ↑N ^ (107 / 120)))))

The weak large-sieve constant is now fully eliminated from the residual bound at Pan's cutoff. Only the explicit H₃, J₉, and logarithmic scalar factors remain.

theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanPrimePowerCharacterNoncoprimeResidual_le_rpow_polylog : ∃ (C : ℝ), 0 < C ∧ ∀ (N : ℕ) (B : ℝ), 8 ≤ N → 0 ≤ B → liuMainPanPrimePowerCharacterNoncoprimeResidual N B ≤ C * ↑N ^ (227 / 240) * Real.log ↑N ^ 20

The maximal nonprincipal residual has the source exponent 227/240; all conductor, dyadic, and coefficient-multiplicity costs fit in log(N)^20.