noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section10KappaOneAdjointPlus (s : ℝ) : ℝ

The explicit standard adjoint for DDE(2,+1,β) at κ = 1. It is the polynomial standard solution r_{2,1} (up to positive scaling).

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section10KappaOneAdjointPlus s = s ^ 2 - 2 * s + 1 / 2

def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section10KappaOneAdjointMinus (_s : ℝ) : ℝ

The explicit standard adjoint for DDE(2,-1,β) at κ = 1.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section10KappaOneAdjointMinus _s = 1

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section10KappaOneAdjointPlus_dde (s : ℝ) : HasDerivAt (fun (u : ℝ) => u * section10KappaOneAdjointPlus u) (2 * section10KappaOneAdjointPlus s + section10KappaOneAdjointPlus (s + 1)) s

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section10KappaOneAdjointMinus_dde (s : ℝ) : HasDerivAt (fun (u : ℝ) => u * section10KappaOneAdjointMinus u) (2 * section10KappaOneAdjointMinus s - section10KappaOneAdjointMinus (s + 1)) s

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section10KappaOneAdjointPlus_pos {s : ℝ} (hs : 2 ≤ s) : 0 < section10KappaOneAdjointPlus s

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section10KappaOneAdjointMinus_pos (s : ℝ) : 0 < section10KappaOneAdjointMinus s

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section10KappaOneStandardAdjointPlus : Section10StandardAdjoint section10KappaOneAdjointPlus

Thus the previously missing positive standard-adjoint object is explicit at κ=1; no existence or positivity axiom is needed.

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

Signed Iwaniec pairing, retaining the coefficient b.

Equations

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

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section10SignedPairing_hasDerivAt_zero {a b β s : ℝ} {R r : ℝ → ℝ} (hRcont : Continuous R) (hrcont : Continuous r) (_hs : β < s) (hs0 : s ≠ 0) (hR : HasDerivAt R (-(a * R s + b * R (s - 1)) / s) s) (hr : HasDerivAt (fun (u : ℝ) => u * r u) (a * r s + b * r (s + 1)) s) : HasDerivAt (section10SignedPairing b R r) 0 s

Lemma 10.1, pointwise differential form: an original DDE solution paired with an adjoint solution has zero pairing derivative.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section10SignedPairing_eq_of_dde {a b β x y : ℝ} {R r : ℝ → ℝ} (hxy : x ≤ y) (hβ : 1 ≤ β) (hx : β < x) (hRcont : Continuous R) (hrcont : Continuous r) (hR : ∀ (s : ℝ), β < s → HasDerivAt R (-(a * R s + b * R (s - 1)) / s) s) (hr : ∀ (s : ℝ), 0 < s → HasDerivAt (fun (u : ℝ) => u * r u) (a * r s + b * r (s + 1)) s) : section10SignedPairing b R r y = section10SignedPairing b R r x

Lemma 10.1 on an interval. This is the actual comparison-side constancy bridge; pairing vanishing is not assumed.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13QhatAdjointCore {H : Section13HatLayers} (_hH : Section13HatContract H 2) : Section10StandardAdjoint section10KappaOneAdjointPlus

The Q̂ DDE and the explicit positive adjoint are now fully constructed. The only omitted field is pairing-zero itself; unlike the old bridge, this record cannot conceal Lemma 10.17 or an adjacent-value estimate.