Section 10 DDE reduction for the Proposition 13.1 unit shift

This file deliberately stops the source boundary before Lemma 10.29. The remaining source input is the one-sided conclusion of Lemma 10.28: the logarithmic slope of the decreasing common-majorant envelope is non-positive. The unit-shift estimate and its two-step Section 13 consumer are proved below.

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section10Pairing (R r : ℝ → ℝ) (s : ℝ) : ℝ

The Iwaniec pairing in §10, specialized to the coefficient b = 1.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section10Pairing R r s = s * r s * R s - ∫ (t : ℝ) in s - 1..s, r (t + 1) * R t

structure MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Section10DDEApparatus (R : ℝ → ℝ) (β : ℝ) : Type

Minimal non-circular DDE(2,1,β) apparatus used at κ = 1.

The record contains the original and adjoint equations, positivity, and the vanishing pairing. It contains no adjacent-value estimate.

• adjoint : ℝ → ℝ
• beta_ge_one : 1 ≤ β
• continuous : ContinuousOn R (Set.Ioi (β - 1))
• positive (s : ℝ) : β - 1 < s → 0 < R s
• adjoint_positive (s : ℝ) : β ≤ s → 0 < self.adjoint s
• original_dde (s : ℝ) : β < s → HasDerivAt R (-(2 * R s + R (s - 1)) / s) s
• adjoint_dde (s : ℝ) : 0 < s → HasDerivAt (fun (u : ℝ) => u * self.adjoint u) (2 * self.adjoint s + self.adjoint (s + 1)) s
• pairing_zero (s : ℝ) : β < s → section10Pairing R self.adjoint s = 0

structure MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Section10CommonMajorant (R : ℝ → ℝ) : Type

The common majorant ξ and the decreasing envelope furnished by the one-sided half of source Lemma 10.28. The displayed envelope_slope_nonpos is equation (10.44) after multiplying by the positive quantity s R(s); majorizes_log is the elementary Proposition 10.20 comparison, with bounded initial values absorbed into A.

This is strictly upstream of Lemma 10.29: no statement comparing R(s-1) and R(s) is a field of this record.

• xi : ℝ → ℝ
• cMinus : ℝ
• A : ℝ
• one_le_A : 1 ≤ self.A
• majorizes_log (s : ℝ) : 3 ≤ s → 1 / self.A * Real.log (Real.exp 1 * s) ≤ self.xi s - self.cMinus - 2 / s
• envelope_slope_nonpos (s : ℝ) : 3 ≤ s → -R (s - 1) + s * (self.xi s - self.cMinus - 2 / s) * R s ≤ 0

structure MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSection10Bridge (H : Section13HatLayers) (sign : ErrorSign) : Type

Lemma 10.17 and the Proposition 13.1 construction: Q̂ satisfies the positive DDE(2,1,β) apparatus and is uniformly comparable with each T̂±. No adjacent-value estimate is included.

• Qhat : ℝ → ℝ
• dde : Section10DDEApparatus self.Qhat (2 + sign.epsilon)
• K : ℝ
• one_le_K : 1 ≤ self.K
• hat_le (s : ℝ) : 2 + sign.epsilon ≤ s → H.T sign s ≤ self.K * self.Qhat s
• Q_le (s : ℝ) : 2 + sign.epsilon ≤ s → self.Qhat s ≤ self.K * H.T sign s

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section10_lemma1029_unitShift_one_sided {R : ℝ → ℝ} {β s : ℝ} (hDDE : Section10DDEApparatus R β) (Q : Section10CommonMajorant R) (hβ : β ≤ 3) (hs : 3 ≤ s) : s * Real.log (Real.exp 1 * s) * R s ≤ Q.A * R (s - 1)

The one-sided κ=1 content of Lemma 10.29, now derived from the Lemma-10.28 common envelope rather than postulated as a ratio field.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section10_unitShift_forward {R : ℝ → ℝ} {β s : ℝ} (hDDE : Section10DDEApparatus R β) (Q : Section10CommonMajorant R) (hβ : β ≤ 3) (hs : 3 ≤ s) : R s ≤ Q.A / (s * Real.log (Real.exp 1 * s)) * R (s - 1)

Division form of the one-step bound used twice in Proposition 13.1.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13Hat_unitShift_forward {H : Section13HatLayers} (sign : ErrorSign) (B : Section13HatSection10Bridge H sign) (Q : Section10CommonMajorant B.Qhat) {s : ℝ} (hs : 4 ≤ s) : H.T sign s ≤ B.K ^ 2 * Q.A / (s * Real.log (Real.exp 1 * s)) * H.T sign (s - 1)

Lemma 10.17 transports Lemma 10.29 from the common majorant Q̂ to one hat layer.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13HatAsymptoticContract_of_section10 {H : Section13HatLayers} (hH : Section13HatContract H 2) (bridge : (sign : ErrorSign) → Section13HatSection10Bridge H sign) (majorant : (sign : ErrorSign) → Section10CommonMajorant (bridge sign).Qhat) : Section13HatAsymptoticContract H

Internalized Proposition 13.1(iii) contract. Two one-unit applications of Lemma 10.29 give the required two-unit weighted ratio; elementary monotonicity of s and log(es) supplies a single uniform constant for both signs.