Dyadic blocks for Liu's aggregate psi hyperbola

This module decomposes the exact source/von-Mangoldt hyperbola after both induced-character factors have been transferred to the primitive character. The blocks retain the condition a * m ≤ y; in particular, no full rectangle is substituted for the hyperbola. The resulting cells are staircases. A separate Cauchy--Schwarz/large-sieve estimate in each coordinate is therefore not available: in the ranges D^2 ≪ V and V ≪ D^2 it loses, respectively, the conductor saving and the source square-root saving.

def MathlibNt.SieveTheory.LiuWeight.liuPanDyadicShell (j : ℕ) : Finset ℕ

The half-open positive dyadic shell [2^j, 2^(j+1)).

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanDyadicShell j = Finset.Ico (2 ^ j) (2 ^ (j + 1))

theorem MathlibNt.SieveTheory.LiuWeight.mem_liuPanDyadicShell_iff_log {j n : ℕ} (hn : 0 < n) : n ∈ liuPanDyadicShell j ↔ Nat.log 2 n = j

theorem MathlibNt.SieveTheory.LiuWeight.sum_Icc_eq_sum_dyadicShell_of_le {α : Type u_1} [AddCommMonoid α] (g : ℕ → α) {T U : ℕ} (hTU : T ≤ U) : ∑ n ∈ Finset.Icc 1 T, g n = ∑ j ∈ Finset.range (Nat.log 2 U + 1), ∑ n ∈ Finset.Icc 1 T ∩ liuPanDyadicShell j, g n

A positive prefix is the disjoint sum of its dyadic shells. The ambient upper bound permits all later source and Lambda prefixes to use the same pair of logarithmic index ranges.

theorem MathlibNt.SieveTheory.LiuWeight.sum_range_succ_eq_sum_Icc_of_zero {α : Type u_1} [AddCommMonoid α] (g : ℕ → α) (T : ℕ) (hg : g 0 = 0) : ∑ n ∈ Finset.range (T + 1), g n = ∑ n ∈ Finset.Icc 1 T, g n

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanLogLambdaCoefficient (n : ℕ) : ℂ

Logarithmically normalized von Mangoldt coefficients, including their totalized zero values at 0 and 1.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanLogLambdaCoefficient n = ↑(ArithmeticFunction.vonMangoldt n / Real.log ↑n)

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuPanLogLambdaCoefficient_zero : liuPanLogLambdaCoefficient 0 = 0

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuPanLogLambdaCoefficient_one : liuPanLogLambdaCoefficient 1 = 0

theorem MathlibNt.SieveTheory.LiuWeight.norm_liuPanLogLambdaCoefficient_le_one (n : ℕ) : ‖liuPanLogLambdaCoefficient n‖ ≤ 1

theorem MathlibNt.SieveTheory.LiuWeight.liuPanLogLambdaCharacterPrefix_eq_primitive_dilations {q : ℕ} [NeZero q] (t : ℕ) (χ : DirichletCharacter ℂ q) : liuPanLogLambdaCharacterPrefix t q χ = ∑ r ∈ (q / χ.conductor).divisors, ↑(ArithmeticFunction.moebius r) * χ.primitiveCharacter ↑r * ∑ v ∈ Finset.range (t / r + 1), liuPanLogLambdaCoefficient (r * v) * χ.primitiveCharacter ↑v

Primitive/Mobius dilation of a logarithmic von Mangoldt prefix.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPrimitiveDilationLogLambdaHyperbola (y X q : ℕ) (f : ℕ → ℝ) (χ : DirichletCharacter ℂ q) : ℂ

The exact hyperbola after primitive transfer on both the source and Lambda sides. The inner cutoff still depends on the same source variable.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPrimitiveDilationLogLambdaHyperbola y X q f χ = ∑ e ∈ (q / χ.conductor).divisors, ↑(ArithmeticFunction.moebius e) * χ.primitiveCharacter ↑e * ∑ u ∈ Finset.range (X / e + 1), MathlibNt.SieveTheory.LiuWeight.liuPanSourceZeroExtension f (e * u) * χ.primitiveCharacter ↑u * ∑ r ∈ (q / χ.conductor).divisors, ↑(ArithmeticFunction.moebius r) * χ.primitiveCharacter ↑r * ∑ v ∈ Finset.range (y / (e * u) / r + 1), MathlibNt.SieveTheory.LiuWeight.liuPanLogLambdaCoefficient (r * v) * χ.primitiveCharacter ↑v

theorem MathlibNt.SieveTheory.LiuWeight.liuPanSourceLogLambdaCharacterHyperbola_eq_primitive_dilations {q : ℕ} [NeZero q] (y X : ℕ) (f : ℕ → ℝ) (χ : DirichletCharacter ℂ q) : liuPanSourceLogLambdaCharacterHyperbola y X q f χ = liuPanPrimitiveDilationLogLambdaHyperbola y X q f χ

Low-conductor primitive Siegel--Walfisz interface

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPrimitiveLogLambdaDilationPrefix (t r d : ℕ) (ψ : DirichletCharacter ℂ d) : ℂ

The exact logarithmic von Mangoldt prefix after dilation by r, twisted by a primitive character of level d.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPrimitiveLogLambdaDilationPrefix t r d ψ = ∑ v ∈ Finset.range (t / r + 1), MathlibNt.SieveTheory.LiuWeight.liuPanLogLambdaCoefficient (r * v) * ψ ↑v

theorem MathlibNt.SieveTheory.LiuWeight.norm_liuPanPrimitiveLogLambdaDilationPrefix_le (t r d : ℕ) (ψ : DirichletCharacter ℂ d) : ‖liuPanPrimitiveLogLambdaDilationPrefix t r d ψ‖ ≤ ↑(t / r)

The trivial global bound for a primitive dilated prefix. It is the short-prefix input in the low-conductor source transfer: importantly, its length is the actual reduced prefix t / r, not the ambient parameter.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanAggregateLogLambdaLowConductorPrimitiveDilationSum (D₀ y X q l : ℕ) (f : ℕ → ℝ) : ℂ

The low-conductor sum after applying the exact source/Lambda dilation identity to every lifted primitive character.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanAggregateLogLambdaLowConductorPrimitiveDilationSum D₀ y X q l f = if q = 0 then 0 else (↑q.totient)⁻¹ * ∑ d ∈ Finset.Icc 2 q, if d ≤ D₀ then if hdq : d ∣ q then ∑ ψ ∈ MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerPrimitiveCharacters d, have χ := (DirichletCharacter.changeLevel hdq) ψ; star (χ ↑l) * MathlibNt.SieveTheory.LiuWeight.liuPanPrimitiveDilationLogLambdaHyperbola y X q f χ else 0 else 0

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateLogLambdaLowConductorSum_eq_primitive_dilations (D₀ y X q l : ℕ) (f : ℕ → ℝ) : liuPanAggregateLogLambdaLowConductorSum D₀ y X q l f = liuPanAggregateLogLambdaLowConductorPrimitiveDilationSum D₀ y X q l f

The low-conductor sum is exactly its two-sided primitive-dilation form, before any norm or sourcewise triangle inequality.

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateLogLambdaLowConductorPrimitiveDilationSum_zero (D₀ y X l : ℕ) (f : ℕ → ℝ) : liuPanAggregateLogLambdaLowConductorPrimitiveDilationSum D₀ y X 0 l f = 0

@[simp]

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateLogLambdaLowConductorPrimitiveDilationSum_one (D₀ y X l : ℕ) (f : ℕ → ℝ) : liuPanAggregateLogLambdaLowConductorPrimitiveDilationSum D₀ y X 1 l f = 0

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanAggregateLogLambdaLowPrimitiveDilationMaxL (D₀ y N q : ℕ) (f : ℕ → ℝ) : ℝ

Reduced-residue and shared-endpoint maximum of the exact low-conductor primitive-dilation sum.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanAggregateLogLambdaLowPrimitiveDilationMaxL D₀ y N q f = if h : (AnalyticNumberTheory.Sieve.unitResidues q).Nonempty then (Finset.image (fun (l : ℕ) => ‖MathlibNt.SieveTheory.LiuWeight.liuPanAggregateLogLambdaLowConductorPrimitiveDilationSum D₀ y N q l f‖) (AnalyticNumberTheory.Sieve.unitResidues q)).max' ⋯ else 0

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanAggregateLogLambdaLowPrimitiveDilationMaxY (D₀ N q : ℕ) (f : ℕ → ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanAggregateLogLambdaLowPrimitiveDilationMaxY D₀ N q f = (Finset.image (fun (y : ℕ) => MathlibNt.SieveTheory.LiuWeight.liuPanAggregateLogLambdaLowPrimitiveDilationMaxL D₀ y N q f) (Finset.range (N + 1))).max' ⋯

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuMainPanAggregateLogLambdaLowPrimitiveDilationAverage (D₀ N : ℕ) (f : ℕ → ℝ) (B : ℝ) : ℝ

The original squarefree 3^omega modulus average, now with both induced-character dilations visible in every summand.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuMainPanAggregateLogLambdaLowPrimitiveDilationAverage D₀ N f B = ∑ q ∈ Finset.range (MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N B + 1), MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerModulusWeight q * MathlibNt.SieveTheory.LiuWeight.liuPanAggregateLogLambdaLowPrimitiveDilationMaxY D₀ N q f

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateLogLambdaLowConductorMaxL_eq_primitive_dilations (D₀ y N q : ℕ) (f : ℕ → ℝ) : liuPanAggregateLogLambdaLowConductorMaxL D₀ y N q f = liuPanAggregateLogLambdaLowPrimitiveDilationMaxL D₀ y N q f

theorem MathlibNt.SieveTheory.LiuWeight.liuPanAggregateLogLambdaLowConductorMaxY_eq_primitive_dilations (D₀ N q : ℕ) (f : ℕ → ℝ) : liuPanAggregateLogLambdaLowConductorMaxY D₀ N q f = liuPanAggregateLogLambdaLowPrimitiveDilationMaxY D₀ N q f

theorem MathlibNt.SieveTheory.LiuWeight.liuMainPanAggregateLogLambdaLowConductorAverage_eq_primitive_dilations (D₀ N : ℕ) (f : ℕ → ℝ) (B : ℝ) : liuMainPanAggregateLogLambdaLowConductorAverage D₀ N f B = liuMainPanAggregateLogLambdaLowPrimitiveDilationAverage D₀ N f B

def MathlibNt.SieveTheory.LiuWeight.LiuPanPrimitiveLogLambdaDilationSiegelWalfiszBoundAt (N D₀ : ℕ) (A C : ℝ) : Prop

Uniform finite Siegel--Walfisz input for every primitive conductor 2 ≤ d ≤ D₀ and every Lambda-side dilation. The saving is measured at the actual reduced prefix t / r, so the estimate remains meaningful for short prefixes; no estimate is asserted here.

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuPanPrimitiveLogLambdaDilationSiegelWalfiszBoundAt N D₀ A C = (0 < C ∧ ∀ d ∈ Finset.Icc 2 D₀, ∀ ψ ∈ MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerPrimitiveCharacters d, ∀ (r t : ℕ), t ≤ N → have x := t / r; ‖MathlibNt.SieveTheory.LiuWeight.liuPanPrimitiveLogLambdaDilationPrefix t r d ψ‖ ≤ C * ↑x / Real.log ↑(x + 2) ^ A)

theorem MathlibNt.SieveTheory.LiuWeight.norm_liuPanPrimitiveLogLambdaDilationPrefix_le_min_of_siegelWalfisz {N D₀ : ℕ} {A Csw : ℝ} (hSW : LiuPanPrimitiveLogLambdaDilationSiegelWalfiszBoundAt N D₀ A Csw) {d : ℕ} (hd : d ∈ Finset.Icc 2 D₀) (ψ : DirichletCharacter ℂ d) (hψ : ψ ∈ liuPanPrimePowerPrimitiveCharacters d) (r t : ℕ) (ht : t ≤ N) : ‖liuPanPrimitiveLogLambdaDilationPrefix t r d ψ‖ ≤ min (↑(t / r)) (Csw * ↑(t / r) / Real.log ↑(t / r + 2) ^ A)

The pointwise source-transfer input is the minimum of the short-prefix trivial bound and the primitive Siegel--Walfisz bound, both at the same actual reduced prefix.

theorem MathlibNt.SieveTheory.LiuWeight.norm_liuPanPrimitiveLogLambdaDilationPrefix_le_of_reduced_le {t r d L : ℕ} (htr : t / r ≤ L) (ψ : DirichletCharacter ℂ d) : ‖liuPanPrimitiveLogLambdaDilationPrefix t r d ψ‖ ≤ ↑L

In the short range the global prefix bound is available with no Siegel--Walfisz input.

theorem MathlibNt.SieveTheory.LiuWeight.norm_liuPanSourceZeroExtension_source_eq (N a : ℕ) : ‖liuPanSourceZeroExtension (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) a‖ = liuWeight N (liuSourceZ10 N) (liuSourceY3 N) a

The norm of the zero-extended actual Liu source is exactly its indicator weight, including the totalized value at zero.

theorem MathlibNt.SieveTheory.LiuWeight.sum_norm_liuPanSourceZeroExtension_source_le_three_mul_rpow_two_thirds (N : ℕ) (hN : 1 ≤ N) : ∑ a ∈ Finset.Icc 1 N, ‖liuPanSourceZeroExtension (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) a‖ ≤ 3 * ↑N ^ (2 / 3)

The actual Liu source has the required short-range mass bound.

theorem MathlibNt.SieveTheory.LiuWeight.sum_norm_liuPanSourceZeroExtension_source_div_le_one_add_log (N : ℕ) : ∑ a ∈ Finset.Icc 1 N, ‖liuPanSourceZeroExtension (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) a‖ / ↑a ≤ 1 + Real.log ↑N

The actual Liu source has the required reciprocal mass bound for the long reduced-prefix range.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPrimitiveDilationLogLambdaHyperbolaNormEnvelope (y X q : ℕ) (f : ℕ → ℝ) (χ : DirichletCharacter ℂ q) : ℝ

The finite triangle-inequality envelope of one primitive two-dilation hyperbola. It keeps the source dilation e, the Lambda dilation r, and the actual common quotient y / (e * u) visible.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPrimitiveDilationLogLambdaHyperbolaNormEnvelope y X q f χ = ∑ e ∈ (q / χ.conductor).divisors, ‖↑(ArithmeticFunction.moebius e) * χ.primitiveCharacter ↑e‖ * ∑ u ∈ Finset.range (X / e + 1), ‖MathlibNt.SieveTheory.LiuWeight.liuPanSourceZeroExtension f (e * u) * χ.primitiveCharacter ↑u‖ * ∑ r ∈ (q / χ.conductor).divisors, ‖↑(ArithmeticFunction.moebius r) * χ.primitiveCharacter ↑r‖ * ‖MathlibNt.SieveTheory.LiuWeight.liuPanPrimitiveLogLambdaDilationPrefix (y / (e * u)) r χ.conductor χ.primitiveCharacter‖

theorem MathlibNt.SieveTheory.LiuWeight.norm_liuPanPrimitiveDilationLogLambdaHyperbola_le_envelope (y X q : ℕ) (f : ℕ → ℝ) (χ : DirichletCharacter ℂ q) : ‖liuPanPrimitiveDilationLogLambdaHyperbola y X q f χ‖ ≤ liuPanPrimitiveDilationLogLambdaHyperbolaNormEnvelope y X q f χ

The exact primitive hyperbola is bounded by its finite source/Lambda envelope before any cofactor estimate. This is the finite transfer which permits the short/long choice to be made at (y / (e * u)) / r in each summand.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPrimitiveDilationLogLambdaHyperbolaSplitEnvelope (y X q : ℕ) (A Csw : ℝ) (f : ℕ → ℝ) (χ : DirichletCharacter ℂ q) : ℝ

The source/Lambda envelope after the pointwise short/long split at each actual reduced prefix.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPrimitiveDilationLogLambdaHyperbolaSplitEnvelope y X q A Csw f χ = ∑ e ∈ (q / χ.conductor).divisors, ‖↑(ArithmeticFunction.moebius e) * χ.primitiveCharacter ↑e‖ * ∑ u ∈ Finset.range (X / e + 1), ‖MathlibNt.SieveTheory.LiuWeight.liuPanSourceZeroExtension f (e * u) * χ.primitiveCharacter ↑u‖ * ∑ r ∈ (q / χ.conductor).divisors, ‖↑(ArithmeticFunction.moebius r) * χ.primitiveCharacter ↑r‖ * min (↑(y / (e * u) / r)) (Csw * ↑(y / (e * u) / r) / Real.log ↑(y / (e * u) / r + 2) ^ A)

theorem MathlibNt.SieveTheory.LiuWeight.norm_liuPanPrimitiveDilationLogLambdaHyperbola_le_splitEnvelope {N D₀ : ℕ} {A Csw : ℝ} {y X q : ℕ} {f : ℕ → ℝ} {χ : DirichletCharacter ℂ q} (hSW : LiuPanPrimitiveLogLambdaDilationSiegelWalfiszBoundAt N D₀ A Csw) (hy : y ≤ N) (hd : χ.conductor ∈ Finset.Icc 2 D₀) (hψ : χ.primitiveCharacter ∈ liuPanPrimePowerPrimitiveCharacters χ.conductor) : ‖liuPanPrimitiveDilationLogLambdaHyperbola y X q f χ‖ ≤ liuPanPrimitiveDilationLogLambdaHyperbolaSplitEnvelope y X q A Csw f χ

Uniform primitive Siegel--Walfisz input bounds every two-dilation hyperbola by the split envelope. The condition on χ.primitiveCharacter is the exact primitive-character fact supplied by the conductor-fibre regrouping.

def MathlibNt.SieveTheory.LiuWeight.LiuPanLowConductorLogarithmicCutoffAt (D₀ : ℕ → ℕ) (K : ℝ) (N0 : ℕ) : Prop

The logarithmic conductor range required by the low-conductor Siegel--Walfisz regime.

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuPanLowConductorLogarithmicCutoffAt D₀ K N0 = (0 ≤ K ∧ ∀ (N : ℕ), N0 ≤ N → ↑(D₀ N) ≤ Real.log ↑(N + 2) ^ K)

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanLowConductorWeightedShortCofactorMass (D₀ Q : ℕ) : ℝ

The exact cofactor mass for reduced prefixes below the source-transfer cutoff. Both primitive dilations are retained as divisor counts.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanLowConductorWeightedShortCofactorMass D₀ Q = ∑ q ∈ Finset.range (Q + 1), if q = 0 then 0 else MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerModulusWeight q / ↑q.totient * ∑ d ∈ Finset.Icc 2 q, if d ≤ D₀ then if d ∣ q then ↑(MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerPrimitiveCharacters d).card * ↑(q / d).divisors.card * ↑(q / d).divisors.card else 0 else 0

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanLowConductorWeightedLongCofactorMass (D₀ Q : ℕ) : ℝ

The exact cofactor mass in the long reduced-prefix range: the outer dilation contributes its divisor count, while the Lambda-side dilation retains its reciprocal saving.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanLowConductorWeightedLongCofactorMass D₀ Q = ∑ q ∈ Finset.range (Q + 1), if q = 0 then 0 else MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerModulusWeight q / ↑q.totient * ∑ d ∈ Finset.Icc 2 q, if d ≤ D₀ then if d ∣ q then ↑(MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerPrimitiveCharacters d).card * ↑(q / d).divisors.card * ∑ r ∈ (q / d).divisors, (↑r)⁻¹ else 0 else 0

def MathlibNt.SieveTheory.LiuWeight.LiuPanAggregateLowConductorSourceTransferBoundAt (D₀ : ℕ → ℕ) (R Csw B : ℝ) (N0 : ℕ) : Prop

The finite source-transfer comparison after splitting every actual reduced prefix (y / (e * u)) / r at the source cutoff. Its two displayed masses are purely finite cofactor bookkeeping; the preceding envelope theorem and the actual Liu source mass/reciprocal-mass lemmas isolate the remaining comparison. No saving at the ambient parameter N is postulated for short prefixes.

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuPanAggregateLowConductorSourceTransferBoundAt D₀ R Csw B N0 = ∀ (N : ℕ), N0 ≤ N → MathlibNt.SieveTheory.LiuWeight.LiuPanPrimitiveLogLambdaDilationSiegelWalfiszBoundAt N (D₀ N) R Csw → MathlibNt.SieveTheory.LiuWeight.liuMainPanAggregateLogLambdaLowPrimitiveDilationAverage (D₀ N) N (MathlibNt.SieveTheory.LiuWeight.liuWeight N (MathlibNt.SieveTheory.LiuWeight.liuSourceZ10 N) (MathlibNt.SieveTheory.LiuWeight.liuSourceY3 N)) B ≤ (3 * ↑N ^ (5 / 6) + Csw * 6 ^ R * ↑N * (1 + Real.log ↑(N + 2)) / Real.log ↑(N + 2) ^ R) * (MathlibNt.SieveTheory.LiuWeight.liuPanLowConductorWeightedShortCofactorMass (D₀ N) (MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N B) + MathlibNt.SieveTheory.LiuWeight.liuPanLowConductorWeightedLongCofactorMass (D₀ N) (MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N B))

def MathlibNt.SieveTheory.LiuWeight.LiuPanPrimitiveLowConductorSourceTransferLocalBoundAt (D₀ : ℕ → ℕ) (R Csw : ℝ) (N0 : ℕ) : Prop

The only remaining low-conductor source-transfer input after the exact primitive character regrouping: for one fixed conductor fibre and one fixed primitive character, the split envelope is bounded by the displayed short/long cofactor masses. This is the smallest remaining finite source-transfer obligation; the theorems below prove all residue, shared-y, and modulus lifting around it.

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuPanPrimitiveLowConductorSourceTransferLocalBoundAt D₀ R Csw N0 = ∀ (N : ℕ), N0 ≤ N → ∀ (q d : ℕ), d ∈ Finset.Icc 2 (D₀ N) → ∀ (hdq : d ∣ q), ∀ ψ ∈ MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerPrimitiveCharacters d, ∀ y ≤ N, MathlibNt.SieveTheory.LiuWeight.liuPanPrimitiveDilationLogLambdaHyperbolaSplitEnvelope y N q R Csw (MathlibNt.SieveTheory.LiuWeight.liuWeight N (MathlibNt.SieveTheory.LiuWeight.liuSourceZ10 N) (MathlibNt.SieveTheory.LiuWeight.liuSourceY3 N)) ((DirichletCharacter.changeLevel hdq) ψ) ≤ (3 * ↑N ^ (5 / 6) + Csw * 6 ^ R * ↑N * (1 + Real.log ↑(N + 2)) / Real.log ↑(N + 2) ^ R) * (↑(q / d).divisors.card * ↑(q / d).divisors.card + ↑(q / d).divisors.card * ∑ r ∈ (q / d).divisors, (↑r)⁻¹)

theorem MathlibNt.SieveTheory.LiuWeight.LiuPanPrimitiveLowConductorSourceTransferLocalBoundAt.of_primitive_siegelWalfisz (D₀ : ℕ → ℕ) {R Csw : ℝ} (hR : 0 < R) (hCsw : 0 < Csw) : LiuPanPrimitiveLowConductorSourceTransferLocalBoundAt D₀ R Csw 3

The finite local source transfer is unconditional once R and the Siegel--Walfisz constant are positive. Thus primitive Siegel--Walfisz is the only analytic input left in the low-conductor lane.

theorem MathlibNt.SieveTheory.LiuWeight.LiuPanAggregateLowConductorSourceTransferBoundAt.of_local {D₀ : ℕ → ℕ} {R Csw B : ℝ} {N0 : ℕ} (hlocal : LiuPanPrimitiveLowConductorSourceTransferLocalBoundAt D₀ R Csw N0) : LiuPanAggregateLowConductorSourceTransferBoundAt D₀ R Csw B N0

A local split-envelope transfer on each primitive conductor fibre implies the previous aggregate low-conductor source-transfer bound after restoring the reduced-residue maximum, the shared y maximum, and the original modulus average.

def MathlibNt.SieveTheory.LiuWeight.LiuPanLowConductorWeightedCofactorMassBoundAt (D₀ : ℕ → ℕ) (B Ccofactor Kcut Kcof : ℝ) (N0 : ℕ) : Prop

The only remaining finite arithmetic bookkeeping in the low-conductor lane: bound the displayed short and long squarefree 3^omega cofactor masses when the conductor cutoff is at most a fixed power of the logarithm.

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuPanLowConductorWeightedCofactorMassBoundAt D₀ B Ccofactor Kcut Kcof N0 = ∀ (N : ℕ), N0 ≤ N → ↑(D₀ N) ≤ Real.log ↑(N + 2) ^ Kcut → MathlibNt.SieveTheory.LiuWeight.liuPanLowConductorWeightedShortCofactorMass (D₀ N) (MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N B) + MathlibNt.SieveTheory.LiuWeight.liuPanLowConductorWeightedLongCofactorMass (D₀ N) (MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N B) ≤ Ccofactor * Real.log ↑(N + 2) ^ Kcof

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

A squarefree Euler-product envelope for the two cofactor divisor factors. The coefficient 12^ω(q)/φ(q) is what remains after retaining the outer 3^ω(q) and bounding the two complementary squarefree divisor counts by 2^ω(q) each.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanLowConductorCofactorEnvelopeMass Q = ∑ q ∈ Finset.range (Q + 1), ↑(ArithmeticFunction.moebius q) ^ 2 * 12 ^ q.primeFactors.card / ↑q.totient

theorem MathlibNt.SieveTheory.LiuWeight.liuPanLowConductorCofactorEnvelopeMass_nonneg (Q : ℕ) : 0 ≤ liuPanLowConductorCofactorEnvelopeMass Q

theorem MathlibNt.SieveTheory.LiuWeight.liuPanLowConductorCofactorEnvelopeMass_le_prod_one_add (Q : ℕ) : liuPanLowConductorCofactorEnvelopeMass Q ≤ ∏ p ∈ AnalyticNumberTheory.Mertens.primesUpTo Q, (1 + 24 / ↑p)

Subset expansion of the finite squarefree cofactor envelope.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanLowConductorCofactorEnvelopeMass_le_polylog : ∃ (C : ℝ), 0 < C ∧ ∀ (Q : ℕ), liuPanLowConductorCofactorEnvelopeMass Q ≤ C * Real.log (↑Q + 2) ^ 24

The squarefree cofactor envelope has a fixed unconditional logarithmic growth. This is only the finite Euler-product/Mertens estimate.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanLowConductorWeightedCofactorMasses_le_envelope (D₀ Q : ℕ) : liuPanLowConductorWeightedShortCofactorMass D₀ Q + liuPanLowConductorWeightedLongCofactorMass D₀ Q ≤ 2 * ↑D₀ ^ 2 * liuPanLowConductorCofactorEnvelopeMass Q

Both exact cofactor masses are bounded by the same finite squarefree Euler-product envelope, with the conductor range counted only after the primitive-character bound has been applied.

theorem MathlibNt.SieveTheory.LiuWeight.exists_liuPanLowConductorWeightedCofactorMassBoundAt (D₀ : ℕ → ℕ) (B Kcut : ℝ) (hB : 0 ≤ B) (_hKcut : 0 ≤ Kcut) : ∃ (Ccofactor : ℝ), 0 < Ccofactor ∧ LiuPanLowConductorWeightedCofactorMassBoundAt D₀ B Ccofactor Kcut (2 * Kcut + 24) 3

The finite weighted cofactor bookkeeping is unconditional. It uses only the stated logarithmic conductor cutoff; the Euler-product estimate is the finite Mertens bound above, not a Siegel--Walfisz or BV input.

theorem MathlibNt.SieveTheory.LiuWeight.LiuMainPanAggregateLowConductorSiegelWalfiszBoundAt.of_primitive {D₀ : ℕ → ℕ} {A C B R Csw Ccofactor Kcut Kcof : ℝ} {N0 : ℕ} (hSW : ∀ (N : ℕ), N0 ≤ N → LiuPanPrimitiveLogLambdaDilationSiegelWalfiszBoundAt N (D₀ N) R Csw) (hlocal : LiuPanPrimitiveLowConductorSourceTransferLocalBoundAt D₀ R Csw N0) (hcofactor : LiuPanLowConductorWeightedCofactorMassBoundAt D₀ B Ccofactor Kcut Kcof N0) (hcutoff : LiuPanLowConductorLogarithmicCutoffAt D₀ Kcut N0) (hscale : ∀ (N : ℕ), N0 ≤ N → (3 * ↑N ^ (5 / 6) + Csw * 6 ^ R * ↑N * (1 + Real.log ↑(N + 2)) / Real.log ↑(N + 2) ^ R) * (Ccofactor * Real.log ↑(N + 2) ^ Kcof) ≤ C * ↑N / Real.log ↑N ^ A) : LiuMainPanAggregateLowConductorSiegelWalfiszBoundAt D₀ A C B N0

A uniform primitive Siegel--Walfisz estimate, the exact weighted cofactor transfer, and the final scalar comparison imply the existing low-conductor source-family bound.

def MathlibNt.SieveTheory.LiuWeight.LiuPanPrimitiveLogLambdaDilationSiegelWalfiszProducer (D₀ : ℕ → ℕ) : Prop

A source-family primitive Siegel--Walfisz producer at one conductor cutoff. The logarithmic cutoff exponent is chosen before the arbitrary saving R. This order is essential: the low-conductor endpoint must choose R with enough slack after seeing the fixed cutoff exponent, rather than allowing the cutoff exponent to depend circularly on that choice.

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuPanPrimitiveLogLambdaDilationSiegelWalfiszProducer D₀ = ∃ (Kcut : ℝ), 0 ≤ Kcut ∧ ∀ (R : ℝ), 0 < R → ∃ (Csw : ℝ), 0 < Csw ∧ ∃ (N0 : ℕ), MathlibNt.SieveTheory.LiuWeight.LiuPanLowConductorLogarithmicCutoffAt D₀ Kcut N0 ∧ ∀ (N : ℕ), N0 ≤ N → MathlibNt.SieveTheory.LiuWeight.LiuPanPrimitiveLogLambdaDilationSiegelWalfiszBoundAt N (D₀ N) R Csw

def MathlibNt.SieveTheory.LiuWeight.LiuMainPanAggregateLowConductorSiegelWalfiszSourceFamilyBound (D₀ : ℕ → ℕ) : Prop

The eventual low-conductor estimate, uniformly as a source family.

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuMainPanAggregateLowConductorSiegelWalfiszSourceFamilyBound D₀ = ∀ (A : ℝ), 0 < A → ∃ (C : ℝ), 0 < C ∧ ∃ (B : ℝ), 0 ≤ B ∧ ∃ (N0 : ℕ), MathlibNt.SieveTheory.LiuWeight.LiuMainPanAggregateLowConductorSiegelWalfiszBoundAt D₀ A C B N0

theorem MathlibNt.SieveTheory.LiuWeight.exists_liuPanLowConductorSiegelWalfiszScalarBoundAt (A Csw Ccofactor Kcut : ℝ) (hA : 0 < A) (hCsw : 0 < Csw) (hCcofactor : 0 < Ccofactor) (hKcut : 0 ≤ Kcut) : have Kcof := 2 * Kcut + 24; have R := A + Kcof + 2; ∃ (C : ℝ), 0 < C ∧ ∃ (N0 : ℕ), ∀ (N : ℕ), N0 ≤ N → (3 * ↑N ^ (5 / 6) + Csw * 6 ^ R * ↑N * (1 + Real.log ↑(N + 2)) / Real.log ↑(N + 2) ^ R) * (Ccofactor * Real.log ↑(N + 2) ^ Kcof) ≤ C * ↑N / Real.log ↑N ^ A

The short N^(5/6) term and the shifted-log Siegel--Walfisz term both absorb the finite cofactor loss log(N+2)^(2*Kcut+24).

theorem MathlibNt.SieveTheory.LiuWeight.LiuPanPrimitiveLogLambdaDilationSiegelWalfiszProducer.to_lowConductorSourceFamily {D₀ : ℕ → ℕ} (hproducer : LiuPanPrimitiveLogLambdaDilationSiegelWalfiszProducer D₀) : LiuMainPanAggregateLowConductorSiegelWalfiszSourceFamilyBound D₀

Uniform primitive Siegel--Walfisz is the sole remaining analytic input for the low-conductor source family. The local source transfer and both cofactor masses are supplied by unconditional theorems in this module.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPrimitiveDilationDyadicStaircase (j k y X q : ℕ) (f : ℕ → ℝ) (χ : DirichletCharacter ℂ q) : ℂ

One disjoint dyadic staircase cell after both primitive dilations. Its source and Lambda coordinates lie in half-open dyadic shells, while the exact hyperbola cutoff remains in the Lambda endpoint.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPrimitiveDilationDyadicStaircase j k y X q f χ = ∑ e ∈ (q / χ.conductor).divisors, ↑(ArithmeticFunction.moebius e) * χ.primitiveCharacter ↑e * ∑ u ∈ Finset.Icc 1 (X / e) ∩ MathlibNt.SieveTheory.LiuWeight.liuPanDyadicShell j, MathlibNt.SieveTheory.LiuWeight.liuPanSourceZeroExtension f (e * u) * χ.primitiveCharacter ↑u * ∑ r ∈ (q / χ.conductor).divisors, ↑(ArithmeticFunction.moebius r) * χ.primitiveCharacter ↑r * ∑ v ∈ Finset.Icc 1 (y / (e * u) / r) ∩ MathlibNt.SieveTheory.LiuWeight.liuPanDyadicShell k, MathlibNt.SieveTheory.LiuWeight.liuPanLogLambdaCoefficient (r * v) * χ.primitiveCharacter ↑v

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPrimitiveDilationDyadicExpansion (y X q : ℕ) (f : ℕ → ℝ) (χ : DirichletCharacter ℂ q) : ℂ

The exact nested dyadic expansion. For each pair of source/Lambda dilations, the only block labels are j ≤ log₂ X and k ≤ log₂ y.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPrimitiveDilationDyadicExpansion y X q f χ = ∑ e ∈ (q / χ.conductor).divisors, ↑(ArithmeticFunction.moebius e) * χ.primitiveCharacter ↑e * ∑ j ∈ Finset.range (Nat.log 2 X + 1), ∑ u ∈ Finset.Icc 1 (X / e) ∩ MathlibNt.SieveTheory.LiuWeight.liuPanDyadicShell j, MathlibNt.SieveTheory.LiuWeight.liuPanSourceZeroExtension f (e * u) * χ.primitiveCharacter ↑u * ∑ r ∈ (q / χ.conductor).divisors, ↑(ArithmeticFunction.moebius r) * χ.primitiveCharacter ↑r * ∑ k ∈ Finset.range (Nat.log 2 y + 1), ∑ v ∈ Finset.Icc 1 (y / (e * u) / r) ∩ MathlibNt.SieveTheory.LiuWeight.liuPanDyadicShell k, MathlibNt.SieveTheory.LiuWeight.liuPanLogLambdaCoefficient (r * v) * χ.primitiveCharacter ↑v

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimitiveDilationLogLambdaHyperbola_eq_dyadicExpansion {q : ℕ} [NeZero q] (y X : ℕ) (f : ℕ → ℝ) (χ : DirichletCharacter ℂ q) : liuPanPrimitiveDilationLogLambdaHyperbola y X q f χ = liuPanPrimitiveDilationDyadicExpansion y X q f χ

Exact O((1+log X)(1+log y)) dyadic staircase decomposition of the primitive-dilation hyperbola.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanSourceLogLambdaCharacterHyperbola_eq_dyadicExpansion {q : ℕ} [NeZero q] (y X : ℕ) (f : ℕ → ℝ) (χ : DirichletCharacter ℂ q) : liuPanSourceLogLambdaCharacterHyperbola y X q f χ = liuPanPrimitiveDilationDyadicExpansion y X q f χ

theorem MathlibNt.SieveTheory.LiuWeight.liuPanDyadicStaircaseIndex_card (X y : ℕ) : ((Finset.range (Nat.log 2 X + 1)).product (Finset.range (Nat.log 2 y + 1))).card = (Nat.log 2 X + 1) * (Nat.log 2 y + 1)

The displayed dyadic staircase family has exactly the advertised number of possible block labels.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanDyadicStaircaseIndex_card_le_sq {X y N : ℕ} (hX : X ≤ N) (hy : y ≤ N) : ((Finset.range (Nat.log 2 X + 1)).product (Finset.range (Nat.log 2 y + 1))).card ≤ (Nat.log 2 N + 1) ^ 2

When both hyperbola coordinates are at most N, the number of available dyadic source/Lambda labels is at most (1+log₂ N)^2.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanLogLambdaDyadicEnergy_le_card (T r k d : ℕ) (ψ : DirichletCharacter ℂ d) : ∑ v ∈ Finset.Icc 1 T ∩ liuPanDyadicShell k, ‖liuPanLogLambdaCoefficient (r * v) * ψ ↑v‖ ^ 2 ≤ ↑(Finset.Icc 1 T ∩ liuPanDyadicShell k).card

Lambda-side energy in every primitive dyadic cell is at most its length.

theorem MathlibNt.SieveTheory.LiuWeight.liuWeight_ne_zero_source_bounds {N a : ℕ} (hN : 1 ≤ N) (ha : liuWeight N (liuSourceZ10 N) (liuSourceY3 N) a ≠ 0) : ↑N ^ (13 / 30) < ↑a ∧ ↑a ≤ ↑N ^ (2 / 3)

The exact support geometry of Liu's source: every nonzero coefficient lies strictly above N^(13/30) and at most N^(2/3).

theorem MathlibNt.SieveTheory.LiuWeight.liuWeight_hyperbola_lambda_lt_rpow_seventeen_thirtieth {N a m : ℕ} (hN : 1 ≤ N) (ha : liuWeight N (liuSourceZ10 N) (liuSourceY3 N) a ≠ 0) (ham : a * m ≤ N) : ↑m < ↑N ^ (17 / 30)

On the exact product hyperbola, the source lower bound forces the von-Mangoldt variable below N^(17/30).

Fixed dilation staircase blocks

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPrimitiveDilationDyadicBlock (e r j k y X q : ℕ) (f : ℕ → ℝ) (χ : DirichletCharacter ℂ q) : ℂ

One fixed (e,r,j,k) block of the primitive hyperbola. This is a staircase, not a tensor-product rectangle: the upper endpoint of the v-sum still depends on u.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPrimitiveDilationDyadicBlock e r j k y X q f χ = ↑(ArithmeticFunction.moebius e) * χ.primitiveCharacter ↑e * (↑(ArithmeticFunction.moebius r) * χ.primitiveCharacter ↑r) * ∑ u ∈ Finset.Icc 1 (X / e) ∩ MathlibNt.SieveTheory.LiuWeight.liuPanDyadicShell j, MathlibNt.SieveTheory.LiuWeight.liuPanSourceZeroExtension f (e * u) * χ.primitiveCharacter ↑u * ∑ v ∈ Finset.Icc 1 (y / (e * u) / r) ∩ MathlibNt.SieveTheory.LiuWeight.liuPanDyadicShell k, MathlibNt.SieveTheory.LiuWeight.liuPanLogLambdaCoefficient (r * v) * χ.primitiveCharacter ↑v

theorem MathlibNt.SieveTheory.LiuWeight.Icc_inter_liuPanDyadicShell_eq_Ico (T j : ℕ) : Finset.Icc 1 T ∩ liuPanDyadicShell j = Finset.Ico (2 ^ j) (2 ^ j + (min (T + 1) (2 ^ (j + 1)) - 2 ^ j))

A dyadic shell clipped at a positive prefix is a half-open interval with the same left endpoint. This is the interval shape used by finite Perron.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanDilationStaircase_eq_filter {e r u y N k : ℕ} (he : 0 < e) (hr : 0 < r) (hu : 0 < u) (hyN : y ≤ N) : Finset.Icc 1 (y / (e * u) / r) ∩ liuPanDyadicShell k = {v ∈ Finset.Icc 1 (N / r) ∩ liuPanDyadicShell k | u * v ≤ y / (e * r)}

At fixed positive dilations, the staircase cutoff is exactly the product cutoff in the ambient clipped dyadic rectangle.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanPrimitiveDilationDyadicExpansion_eq_sum_blocks (y X q : ℕ) (f : ℕ → ℝ) (χ : DirichletCharacter ℂ q) : liuPanPrimitiveDilationDyadicExpansion y X q f χ = ∑ e ∈ (q / χ.conductor).divisors, ∑ j ∈ Finset.range (Nat.log 2 X + 1), ∑ r ∈ (q / χ.conductor).divisors, ∑ k ∈ Finset.range (Nat.log 2 y + 1), liuPanPrimitiveDilationDyadicBlock e r j k y X q f χ

Exposing the four finite block indices is an exact rearrangement. In particular this theorem does not replace a staircase by its ambient rectangle.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanSourceDilationDyadicEnergy (N e j : ℕ) (f : ℕ → ℝ) : ℝ

Source-side square energy for one fixed dilation and dyadic shell.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanSourceDilationDyadicEnergy N e j f = ∑ u ∈ Finset.Icc 1 (N / e) ∩ MathlibNt.SieveTheory.LiuWeight.liuPanDyadicShell j, ‖MathlibNt.SieveTheory.LiuWeight.liuPanSourceZeroExtension f (e * u)‖ ^ 2

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanLogLambdaDilationDyadicEnergy (N r k : ℕ) : ℝ

Lambda-side square energy for one fixed dilation and dyadic shell.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanLogLambdaDilationDyadicEnergy N r k = ∑ v ∈ Finset.Icc 1 (N / r) ∩ MathlibNt.SieveTheory.LiuWeight.liuPanDyadicShell k, ‖MathlibNt.SieveTheory.LiuWeight.liuPanLogLambdaCoefficient (r * v)‖ ^ 2

theorem MathlibNt.SieveTheory.LiuWeight.liuPanSourceDilationDyadicEnergy_le_card (N e j : ℕ) : liuPanSourceDilationDyadicEnergy N e j (liuWeight N (liuSourceZ10 N) (liuSourceY3 N)) ≤ ↑(Finset.Icc 1 (N / e) ∩ liuPanDyadicShell j).card

Liu's source is an exact indicator, so every fixed dilated source shell has energy at most its cardinality.

theorem MathlibNt.SieveTheory.LiuWeight.liuPanLogLambdaDilationDyadicEnergy_le_card (N r k : ℕ) : liuPanLogLambdaDilationDyadicEnergy N r k ≤ ↑(Finset.Icc 1 (N / r) ∩ liuPanDyadicShell k).card

The Lambda energy of a fixed dilated shell is bounded by its cardinality.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanPrimitiveDilationDyadicBlockMaxYL (N e r j k q : ℕ) (f : ℕ → ℝ) (χ : DirichletCharacter ℂ q) : ℝ

Uniform maximum over the shared hyperbola endpoint and reduced residue phase for one fixed primitive-dilation staircase block.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanPrimitiveDilationDyadicBlockMaxYL N e r j k q f χ = if hS : (AnalyticNumberTheory.Sieve.unitResidues q).Nonempty then (Finset.image (fun (y : ℕ) => (Finset.image (fun (l : ℕ) => ‖star (χ ↑l) * MathlibNt.SieveTheory.LiuWeight.liuPanPrimitiveDilationDyadicBlock e r j k y N q f χ‖) (AnalyticNumberTheory.Sieve.unitResidues q)).max' ⋯) (Finset.range (N + 1))).max' ⋯ else 0

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanWeightedPrimitiveDyadicBlockMean (N Q D e r j k : ℕ) : ℝ

The original squarefree 3^omega modulus weight, exact conductor fiber, and both complementary-cofactor divisor tests for a fixed (D,e,r,j,k) block.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanWeightedPrimitiveDyadicBlockMean N Q D e r j k = ∑ q ∈ Finset.range (Q + 1), if _hq : q = 0 then 0 else MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerModulusWeight q * (↑q.totient)⁻¹ * ∑ d ∈ Finset.Icc 2 q ∩ Finset.Ico D (2 * D), if hdq : d ∣ q then ∑ ψ ∈ MathlibNt.SieveTheory.LiuWeight.liuPanPrimePowerPrimitiveCharacters d, have χ := (DirichletCharacter.changeLevel hdq) ψ; if e ∈ (q / χ.conductor).divisors ∧ r ∈ (q / χ.conductor).divisors then MathlibNt.SieveTheory.LiuWeight.liuPanPrimitiveDilationDyadicBlockMaxYL N e r j k q (MathlibNt.SieveTheory.LiuWeight.liuWeight N (MathlibNt.SieveTheory.LiuWeight.liuSourceZ10 N) (MathlibNt.SieveTheory.LiuWeight.liuSourceY3 N)) χ else 0 else 0

def MathlibNt.SieveTheory.LiuWeight.LiuPanPrimitiveHyperbolaMaximalBlockBoundAt (N Q D e r j k : ℕ) (K : ℝ) : Prop

The precise local analytic input needed for one conductor/source/Lambda scale. Unlike two independent one-dimensional large-sieve estimates, its left side retains the hyperbola maximum, both induced-character dilations, and the original modulus/cofactor weights.

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuPanPrimitiveHyperbolaMaximalBlockBoundAt N Q D e r j k K = (MathlibNt.SieveTheory.LiuWeight.liuPanWeightedPrimitiveDyadicBlockMean N Q D e r j k ≤ Real.log ↑N ^ K / ↑D * √((↑(2 ^ j) + ↑D ^ 2) * MathlibNt.SieveTheory.LiuWeight.liuPanSourceDilationDyadicEnergy N e j (MathlibNt.SieveTheory.LiuWeight.liuWeight N (MathlibNt.SieveTheory.LiuWeight.liuSourceZ10 N) (MathlibNt.SieveTheory.LiuWeight.liuSourceY3 N))) * √((↑(2 ^ k) + ↑D ^ 2) * MathlibNt.SieveTheory.LiuWeight.liuPanLogLambdaDilationDyadicEnergy N r k))

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPanAggregateMediumHighPowerProfile (N D₀ : ℕ) : ℝ

The power-saving profile predicted after summing the local primitive hyperbola estimates over conductor shells and complementary cofactors.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPanAggregateMediumHighPowerProfile N D₀ = ↑N / ↑D₀ + ↑N ^ (5 / 6) + ↑D₀ * √↑N

def MathlibNt.SieveTheory.LiuWeight.LiuPanAggregateMediumHighWeightedCofactorTransferBoundAt (D₀ : ℕ → ℕ) (B C K : ℝ) (N0 : ℕ) : Prop

The still-missing weighted cofactor transfer, isolated from the local primitive hyperbola estimate. It must sum the exact local block bounds without discarding the squarefree 3^omega weights or taking a pointwise cofactor maximum. No instance of this predicate is asserted in this module.

Equations

• MathlibNt.SieveTheory.LiuWeight.LiuPanAggregateMediumHighWeightedCofactorTransferBoundAt D₀ B C K N0 = ∀ (N : ℕ), N0 ≤ N → 0 < D₀ N → (∀ (D e r j k : ℕ), D₀ N < D → MathlibNt.SieveTheory.LiuWeight.LiuPanPrimitiveHyperbolaMaximalBlockBoundAt N (MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N B) D e r j k K) → MathlibNt.SieveTheory.LiuWeight.liuMainPanAggregateLogLambdaMediumHighConductorAverage (D₀ N) N (MathlibNt.SieveTheory.LiuWeight.liuWeight N (MathlibNt.SieveTheory.LiuWeight.liuSourceZ10 N) (MathlibNt.SieveTheory.LiuWeight.liuSourceY3 N)) B ≤ C * MathlibNt.SieveTheory.LiuWeight.liuPanAggregateMediumHighPowerProfile N (D₀ N) * Real.log ↑N ^ K

theorem MathlibNt.SieveTheory.LiuWeight.LiuMainPanAggregateMediumHighConductorBilinearBoundAt.of_local_blocks {D₀ : ℕ → ℕ} {A B C Chigh K : ℝ} {N0 : ℕ} (hlocal : ∀ (N : ℕ), N0 ≤ N → ∀ (D e r j k : ℕ), D₀ N < D → LiuPanPrimitiveHyperbolaMaximalBlockBoundAt N (panModulusCutoff N B) D e r j k K) (htransfer : LiuPanAggregateMediumHighWeightedCofactorTransferBoundAt D₀ B C K N0) (hD₀ : ∀ (N : ℕ), N0 ≤ N → 0 < D₀ N) (hpower : ∀ (N : ℕ), N0 ≤ N → C * liuPanAggregateMediumHighPowerProfile N (D₀ N) * Real.log ↑N ^ K ≤ Chigh * ↑N / Real.log ↑N ^ A) : LiuMainPanAggregateMediumHighConductorBilinearBoundAt D₀ A Chigh B N0

Once the local primitive hyperbola inequality, the weighted cofactor transfer, and the final numerical parameter comparison are available, they supply the existing medium/high source-family contract.