theorem
MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13Qhat_normalizedPlusSlope_bddBelow
{H : Section13HatLayers}
(hH : Section13HatSourceContract H)
:
∃ (B : ℝ),
∀ u ∈ Set.Icc 3 (Real.exp 2 + 1),
-Section10Lemma1028FirstCrossing.normalizedMinusBase (section13Qhat H) Section10CanonicalXi.xi u ≤ B
The normalized plus slope for Qhat is bounded below on the fixed initial
interval used by the first-crossing argument.
theorem
MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13Qhat_reverseEnvelopeEdge
{H : Section13HatLayers}
(hH : Section13HatSourceContract H)
:
Lemma 10.28, increasing-envelope half, for the canonical Section-13
solution Qhat. The proof uses the genuine first crossing and the internal
(10.53)/(10.55) integration-by-parts estimate; neither a derivative sign nor a
unit-shift ratio is assumed.