Documentation

MathlibNt.SieveTheory.LinearSieve.Suzuki.SuzukiLemma132EndpointSlack

source
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
Instances For
    source
    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,∞).

    source
    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.

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

    The endpoint slack is strictly positive.

    source
    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.