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

Equations

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

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

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.lemma1027AdjointRComparison_of_firstCrossingDDEApparatus {R : ℝ → ℝ} (h : Section10Lemma1028FirstCrossing.FirstCrossingDDEApparatus R 3) (hadj : h.adjoint = explicitLemma1027AdjointPlus) : Section10Equation1056UniformStationary.Lemma1027AdjointRComparison R

Lemma 10.27, internalized from the positive DDE solution, the explicit quadratic adjoint, and pairing zero.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.lemma1027AdjointRComparison_of_firstCrossingDDEApparatus h hadj = { K := 2, cutoff := 5, K_nonneg := MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.lemma1027AdjointRComparison_of_firstCrossingDDEApparatus._proof_3, comparison := ⋯ }

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13Qhat_lemma1027AdjointRComparison {H : Section13HatLayers} (hH : Section13HatSourceContract H) : Section10Equation1056UniformStationary.Lemma1027AdjointRComparison (section13Qhat H)

Section 13 specialization: Qhat satisfies the adjacent comparison without assuming that comparison in its source contract or first-crossing apparatus.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13Qhat_lemma1027AdjointRComparison hH = MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.lemma1027AdjointRComparison_of_firstCrossingDDEApparatus (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Section13QhatMajorantClosure.section13QhatFirstCrossingData hH) ⋯