noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.lemma132HatTailSlack (H : Section13HatLayers) : ℝ

The positive amount removed when the plus hat tail at its closed threshold is rewritten with the shifted weight t - 1.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.lemma132HatTailSlack H = ∫ (t : ℝ) in Set.Ioi 3, H.T MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.minus (t - 1)

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.integral_Ioi_hatTailIntegrand_plus_three {H : Section13HatLayers} (hH : Section13HatSourceContract H) : MeasureTheory.IntegrableOn (hatTailIntegrand H ErrorSign.plus) (Set.Ioi 3) MeasureTheory.volume ∧ ∫ (t : ℝ) in Set.Ioi 3, hatTailIntegrand H ErrorSign.plus t = weightedHat H ErrorSign.plus 3

The Section 13 plus-tail identity remains valid at the closed threshold a = 3. The published open-tail lemma cannot be applied directly there, so we apply the same improper-FTC theorem using continuity at 3 and the DDE on (3,∞).

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.integrableOn_lemma132HatTailSlack {H : Section13HatLayers} (hH : Section13HatSourceContract H) : MeasureTheory.IntegrableOn (fun (t : ℝ) => H.T ErrorSign.minus (t - 1)) (Set.Ioi 3) MeasureTheory.volume

The unweighted delayed minus tail defining lemma132HatTailSlack is finite.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.lemma132HatTailSlack_pos {H : Section13HatLayers} (hH : Section13HatSourceContract H) : 0 < lemma132HatTailSlack H

The endpoint slack is strictly positive.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.lemma132_weightedHat_plus_three_endpoint_slack {H : Section13HatLayers} (hH : Section13HatSourceContract H) : MeasureTheory.IntegrableOn (fun (t : ℝ) => (t - 1) * H.T ErrorSign.minus (t - 1)) (Set.Ioi 3) MeasureTheory.volume ∧ ∫ (t : ℝ) in Set.Ioi 3, (t - 1) * H.T ErrorSign.minus (t - 1) = weightedHat H ErrorSign.plus 3 - lemma132HatTailSlack H ∧ weightedHat H ErrorSign.plus 3 - lemma132HatTailSlack H = 1 - lemma132HatTailSlack H

Closed-threshold decomposition: the shifted weighted tail is exactly the normalized plus hat value minus the strictly positive slack.