def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13Phat (H : Section13HatLayers) (s : ℝ) : ℝ

Suzuki (13.8): the antisymmetric combination of the two hat solutions.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13Phat H s = H.T MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.plus s - H.T MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.minus s

def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13Qhat (H : Section13HatLayers) (s : ℝ) : ℝ

Suzuki (13.8): the symmetric, positive combination of the two hat solutions.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13Qhat H s = H.T MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.plus s + H.T MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.minus s

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13Hat_hasDerivAt {H : Section13HatLayers} (hH : Section13HatContract H 2) (sign : ErrorSign) {s : ℝ} (hs : 2 + sign.epsilon < s) : HasDerivAt (H.T sign) (-(2 * H.T sign s + H.T sign.opposite (s - 1)) / s) s

The unweighted form of (T3).

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13Qhat_dde {H : Section13HatLayers} (hH : Section13HatContract H 2) {s : ℝ} (hs : 3 < s) : HasDerivAt (section13Qhat H) (-(2 * section13Qhat H s + section13Qhat H (s - 1)) / s) s

The symmetric combination satisfies DDE(2,1,2).

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13Phat_dde {H : Section13HatLayers} (hH : Section13HatContract H 2) {s : ℝ} (hs : 3 < s) : HasDerivAt (section13Phat H) (-(2 * section13Phat H s - section13Phat H (s - 1)) / s) s

The antisymmetric combination satisfies the companion signed DDE.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13Qhat_continuousOn {H : Section13HatLayers} (hH : Section13HatContract H 2) : ContinuousOn (section13Qhat H) (Set.Ioi 0)

Continuity of Q̂ on its natural positive domain.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13Qhat_pos {H : Section13HatLayers} (hH : Section13HatContract H 2) {s : ℝ} (hs : 0 < s) : 0 < section13Qhat H s

Strict positivity of Q̂.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13Qhat_initial {H : Section13HatLayers} (hH : Section13HatContract H 2) {s : ℝ} (hs : 0 < s) (hs2 : s ≤ 2) : section13Qhat H s = 3 / s ^ 2

Initial history of Q̂ on the common interval (0,2].

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13Qhat_weighted_tendsto_zero {H : Section13HatLayers} (hH : Section13HatContract H 2) : Filter.Tendsto (fun (s : ℝ) => s ^ 2 * section13Qhat H s) Filter.atTop (nhds 0)

The weighted symmetric solution tends to zero, directly from (T5).

structure MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Section13QhatCore (Q : ℝ → ℝ) : Prop

The complete Q̂ package obtained internally from Section13HatContract. Unlike the former downstream bridge, it has no adjoint, pairing, or comparison field hidden inside it.

• dde (s : ℝ) : 3 < s → HasDerivAt Q (-(2 * Q s + Q (s - 1)) / s) s
• continuous : ContinuousOn Q (Set.Ioi 0)
• positive (s : ℝ) : 0 < s → 0 < Q s
• initial (s : ℝ) : 0 < s → s ≤ 2 → Q s = 3 / s ^ 2
• weighted_tendsto_zero : Filter.Tendsto (fun (s : ℝ) => s ^ 2 * Q s) Filter.atTop (nhds 0)

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13Qhat_core {H : Section13HatLayers} (hH : Section13HatContract H 2) : Section13QhatCore (section13Qhat H)

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13Pairing (Q q : ℝ → ℝ) (s : ℝ) : ℝ

The Section 10 bilinear concomitant. This is a definition, not an assumed vanishing condition.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13Pairing Q q s = s * q s * Q s - ∫ (t : ℝ) in s - 1..s, q (t + 1) * Q t

structure MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Section10StandardAdjoint (q : ℝ → ℝ) : Prop

Earlier-Section-10 standard-adjoint interface. It deliberately contains no pairing assertion and no comparison between either hat layer and Q̂. The missing construction of this object belongs to the standard-adjoint existence theorem, upstream of Lemma 10.17.

• continuous : Continuous q
• positive (s : ℝ) : 2 ≤ s → 0 < q s
• dde (s : ℝ) : 0 < s → HasDerivAt (fun (u : ℝ) => u * q u) (2 * q s + q (s + 1)) s

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13_T_eq_Q_add_sign_P (H : Section13HatLayers) (sign : ErrorSign) (s : ℝ) : H.T sign s = (section13Qhat H s + if sign = ErrorSign.plus then section13Phat H s else -section13Phat H s) / 2

Algebraic reconstruction of the two hat layers from P̂,Q̂.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13_comparison_of_P_abs_le {H : Section13HatLayers} {ρ s : ℝ} (_hρ0 : 0 ≤ ρ) (_hρ1 : ρ < 1) (hP : |section13Phat H s| ≤ ρ * section13Qhat H s) : (1 - ρ) / 2 * section13Qhat H s ≤ H.T ErrorSign.plus s ∧ H.T ErrorSign.plus s ≤ (1 + ρ) / 2 * section13Qhat H s ∧ (1 - ρ) / 2 * section13Qhat H s ≤ H.T ErrorSign.minus s ∧ H.T ErrorSign.minus s ≤ (1 + ρ) / 2 * section13Qhat H s

The exact order-theoretic last step in the Lemma 10.17 bridge. The hard input is only a strict contraction of P̂ relative to Q̂; no final T̂± ≍ Q̂ conclusion is hidden in a structure field.