Suzuki Lemma 14.4 error objects and algebraic normalization (κ = 1)

Source-faithful transcription of the objects used around (14.13)--(14.15). The Section 13 majorants T̂⁺, T̂⁻ are parameters: their genuinely analytic monotonicity and integral estimates are exposed below as named premises.

inductive MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign : Type

The two signs occurring in the Section 13 majorants.

• plus : ErrorSign
• minus : ErrorSign

@[instance_reducible]

instance MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.instDecidableEqErrorSign : DecidableEq ErrorSign

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.instDecidableEqErrorSign x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.instReprErrorSign.repr : ErrorSign → ℕ → Std.Format

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.instReprErrorSign.repr MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.plus prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.plus")).group prec✝
• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.instReprErrorSign.repr MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.minus prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.minus")).group prec✝

@[instance_reducible]

instance MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.instReprErrorSign : Repr ErrorSign

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.instReprErrorSign = { reprPrec := MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.instReprErrorSign.repr }

def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.opposite : ErrorSign → ErrorSign

Reversal of sign, used because the induction step changes parity.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.plus.opposite = MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.minus
• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.minus.opposite = MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.plus

@[simp]

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.opposite_plus : plus.opposite = minus

@[simp]

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.opposite_minus : minus.opposite = plus

@[simp]

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.opposite_opposite (sign : ErrorSign) : sign.opposite.opposite = sign

def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth (N : ℕ) : ErrorSign

Suzuki's convention: odd depth uses +, even depth uses -.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N = if Odd N then MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.plus else MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.minus

@[simp]

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth_of_odd {N : ℕ} (hN : Odd N) : ofDepth N = plus

@[simp]

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth_of_even {N : ℕ} (hN : Even N) : ofDepth N = minus

def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.epsilon : ErrorSign → ℝ

Suzuki's ε₊=1, ε₋=0.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.plus.epsilon = 1
• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.minus.epsilon = 0

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth_pred_eq_opposite {N : ℕ} (hN : 1 ≤ N) : ofDepth (N - 1) = (ofDepth N).opposite

Passing from N to N-1 reverses the sign.

structure MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers : Type

The two positive Section 13 majorants T̂⁺ and T̂⁻. At κ = 1 Suzuki is in the κ > 1/2 branch of (13.1), hence κ̂ = κ = 1: δ does not occur in this branch. The functions remain analytic input here.

• betaHat : ℝ
• Tplus : ℝ → ℝ
• Tminus : ℝ → ℝ

def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers.T (H : Section13HatLayers) : ErrorSign → ℝ → ℝ

Signed lookup for T̂⁺ and T̂⁻.

Equations

• H.T MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.plus = H.Tplus
• H.T MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.minus = H.Tminus

def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers.kappaHat (_H : Section13HatLayers) : ℝ

At κ=1, equation (13.1) gives κ̂ = κ = 1.

Equations

• _H.kappaHat = 1

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope (H : Section13HatLayers) (N : ℕ) (D d s : ℝ) : ℝ

Exact κ=1 specialization of Suzuki's E_N(D,s) = (1+s^d/log D)^s s^(κ̂-κ+1) T̂^±(s). The sign is + for odd N and - for even N.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H N D d s = (1 + s ^ d / Real.log D) ^ s * s ^ (H.kappaHat - 1 + 1) * H.T (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N) s

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.qD (H : Section13HatLayers) (sign : ErrorSign) (D d Δ s : ℝ) : ℝ

Exact κ=1 specialization of Suzuki's q_D^±.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.qD H sign D d Δ s = (1 + s ^ d / Real.log D) ^ (s - 1) * (s - 1) ^ (H.kappaHat - 1 + 1) * H.T sign (s - 1) * (s / (s - 1)) ^ Δ

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.lambda (H : Section13HatLayers) (sign : ErrorSign) (D d ε t : ℝ) : ℝ

Exact κ=1 specialization of Suzuki's auxiliary Λ_ε^±(t) = (1+(t+ε)^d/log D)^t t^(κ̂+1) T̂^±(t), ε=0,1.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.lambda H sign D d ε t = (1 + (t + ε) ^ d / Real.log D) ^ t * t ^ (H.kappaHat + 1) * H.T sign t

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope_odd {N : ℕ} (hN : Odd N) (H : Section13HatLayers) (D d s : ℝ) : errorEnvelope H N D d s = (1 + s ^ d / Real.log D) ^ s * s * H.Tplus s

The source parity in E_N is exact.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope_even {N : ℕ} (hN : Even N) (H : Section13HatLayers) (D d s : ℝ) : errorEnvelope H N D d s = (1 + s ^ d / Real.log D) ^ s * s * H.Tminus s

The source parity in E_N is exact.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.equation14_13_source_normalization (H : Section13HatLayers) {N : ℕ} (hN : 1 ≤ N) (x d s : ℝ) : errorEnvelope H (N - 1) x d (s - 1) = (1 + (s - 1) ^ d / Real.log x) ^ (s - 1) * (s - 1) * H.T (ErrorSign.ofDepth N).opposite (s - 1)

Algebraic parity normalization preceding (14.13): the inherited depth N-1 uses the sign opposite to depth N.

def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_13PointwisePremise (H : Section13HatLayers) (N : ℕ) (D d Δ s x : ℝ) : Prop

The pointwise majorization used to pass from inherited E_{N-1} to (log D)^(-Δ) q_D^∓. Its proof is the genuinely analytic/base-comparison part immediately before (14.13), so it is represented as a premise.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_13PointwisePremise H N D d Δ s x = (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H (N - 1) x d (s - 1) * Real.log x ^ (-Δ) ≤ Real.log D ^ (-Δ) * MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.qD H (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N).opposite D d Δ s)

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.equation14_13_finset {ι : Type u_1} (S : Finset ι) (weight inherited qvalue : ι → ℝ) (logFactor : ℝ) (hweight : ∀ i ∈ S, 0 ≤ weight i) (hpointwise : ∀ i ∈ S, inherited i ≤ logFactor * qvalue i) : ∑ i ∈ S, weight i * inherited i ≤ logFactor * ∑ i ∈ S, weight i * qvalue i

Pure sum algebra in (14.13): a pointwise inherited-error bound remains valid after multiplication by nonnegative sieve weights and finite summation.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.equation14_14 (H : Section13HatLayers) (sign : ErrorSign) (D d Δ t : ℝ) (ht : 1 < t) : qD H sign D d Δ t * t = (1 + t ^ d / Real.log D) ^ (t - 1) * (t - 1) ^ (H.kappaHat + 1) * H.T sign (t - 1) * (t / (t - 1)) ^ (1 + Δ)

Algebraic identity (14.14), specialized to κ=1.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.equation14_15 (H : Section13HatLayers) (sign : ErrorSign) (D d Δ t : ℝ) (ht : 1 < t) : lambda H sign D d 1 (t - 1) * (t / (t - 1)) ^ (1 + Δ) = qD H sign D d Δ t * t

Algebraic identity (14.15), specialized to κ=1.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope_nonneg (H : Section13HatLayers) (N : ℕ) {D d s : ℝ} (hD : 1 < D) (hs : 0 ≤ s) (hT : 0 ≤ H.T (ErrorSign.ofDepth N) s) : 0 ≤ errorEnvelope H N D d s

Positivity of E_N from the currently available finite/Section-13 layer positivity data.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.qD_nonneg (H : Section13HatLayers) (sign : ErrorSign) {D d Δ s : ℝ} (hD : 1 < D) (hs : 1 ≤ s) (hT : 0 ≤ H.T sign (s - 1)) : 0 ≤ qD H sign D d Δ s

Positivity of q_D^± on its source range.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.lambda_nonneg (H : Section13HatLayers) (sign : ErrorSign) {D d ε t : ℝ} (hD : 1 < D) (hε : 0 ≤ ε) (ht : 0 ≤ t) (hT : 0 ≤ H.T sign t) : 0 ≤ lambda H sign D d ε t

Positivity of Λ_ε^± on the range used in Claim 14.6.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope_pos (H : Section13HatLayers) (N : ℕ) {D d s : ℝ} (hD : 1 < D) (hs : 0 < s) (hT : 0 < H.T (ErrorSign.ofDepth N) s) : 0 < errorEnvelope H N D d s

Strict positivity of E_N under the strict positivity furnished by Proposition 13.1 for T̂⁺,T̂⁻.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.qD_pos (H : Section13HatLayers) (sign : ErrorSign) {D d Δ s : ℝ} (hD : 1 < D) (hs : 1 < s) (hT : 0 < H.T sign (s - 1)) : 0 < qD H sign D d Δ s

Strict positivity of q_D^± on the range used by Lemma 8.7.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.lambda_pos (H : Section13HatLayers) (sign : ErrorSign) {D d ε t : ℝ} (hD : 1 < D) (hε : 0 ≤ ε) (ht : 0 < t) (hT : 0 < H.T sign t) : 0 < lambda H sign D d ε t

Strict positivity of Λ_ε^± for t>0, ε≥0.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.continuousOn_errorEnvelope (H : Section13HatLayers) (N : ℕ) (D d : ℝ) {a : ℝ} (hD : 1 < D) (ha : 0 < a) (hT : ContinuousOn (H.T (ErrorSign.ofDepth N)) (Set.Ici a)) : ContinuousOn (errorEnvelope H N D d) (Set.Ici a)

Continuity of E_N on a positive interval, conditional only on continuity of the selected Section 13 layer there.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.continuousOn_qD (H : Section13HatLayers) (sign : ErrorSign) (D d Δ : ℝ) (hD : 1 < D) (hT : Continuous (H.T sign)) : ContinuousOn (qD H sign D d Δ) (Set.Ioi 1)

Continuity of q_D^± on (1,∞), conditional only on continuity of T̂^±.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.continuousOn_lambda (H : Section13HatLayers) (sign : ErrorSign) (D d ε : ℝ) (hD : 1 < D) (hε : 0 ≤ ε) (hT : Continuous (H.T sign)) : ContinuousOn (lambda H sign D d ε) (Set.Ioi 0)

Continuity of Λ_ε^± on (0,∞), conditional only on continuity of T̂^±.

def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_6_MonotoneLambdaPremise (H : Section13HatLayers) (D d σ : ℝ) : Prop

Analytic Claim 14.6(i), deliberately left as a named premise.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_6_MonotoneLambdaPremise H D d σ = ∀ (sign : MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign) (ε : ℝ), ε = 0 ∨ ε = 1 → AntitoneOn (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.lambda H sign D d ε) (Set.Icc (H.betaHat + sign.epsilon) σ)

def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_6_MonotoneQPremise (H : Section13HatLayers) (D d Δ σ : ℝ) : Prop

Analytic Claim 14.6(ii), deliberately left as a named premise.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_6_MonotoneQPremise H D d Δ σ = ∀ (sign : MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign), AntitoneOn (fun (t : ℝ) => MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.qD H sign.opposite D d Δ t * t) (Set.Ioc (H.betaHat + sign.epsilon) σ)

def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_6_IntegralPremise (H : Section13HatLayers) (D d Δ σ : ℝ) : Prop

Analytic Claim 14.6(iii), deliberately left as a named premise. At κ=1, dt^κ = dt, hence the ordinary interval integral below.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_6_IntegralPremise H D d Δ σ = ∀ (sign : MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign) (s : ℝ), H.betaHat + sign.epsilon ≤ s → s ≤ σ → ∫ (t : ℝ) in s..σ, MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.qD H sign.opposite D d Δ t < (1 - 1 / σ) ^ (1 - Δ) * MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.lambda H sign D d 0 s