Documentation

MathlibNt.SieveTheory.LinearSieve.Suzuki.SuzukiMovingSigmaCompactHead

Corrected-sign compact-head margin #

For κ = 1 we take Δ₀ = 1 and θ = (Δ₀ - Δ) / 2 = (1 - Δ) / 2. Thus the positive exponent is Δ₀ - Δ, not the reversed (and negative) printed sign Δ - Δ₀.

source
noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.compactHeadTheta (Δ : ℝ) :
ℝ

The corrected positive half-gap exponent for the κ = 1 compact head.

Equations
Instances For
    source
    noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.compactHeadCoefficient (Δ M : ℝ) :
    ℝ

    The coefficient at the fixed splitting point M corresponding to the half-gap exponent.

    Equations
    Instances For
      source
      noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.compactHeadMargin (Δ M : ℝ) :
      ℝ

      The explicit coefficient margin between the half-gap coefficient and the full source exponent Δ₀ - Δ = 1 - Δ.

      Equations
      Instances For
        source
        theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.corrected_deltaGap_pos {Δ : ℝ} (hΔ : Δ < 1) :
        0 < 1 - Δ
        source
        theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.compactHeadTheta_pos {Δ : ℝ} (hΔ : Δ < 1) :
        0 < compactHeadTheta Δ
        source
        theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.compactHeadMargin_pos {Δ M : ℝ} (hΔ : Δ < 1) (hM : 1 < M) :
        0 < compactHeadMargin Δ M

        The corrected sign gives a genuinely positive, completely explicit margin at every fixed M > 1.

        source
        theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.compactHead_weightedTail_strict {H : Section13HatLayers} (hH : Section13HatContract H 2) (sign : ErrorSign) {Δ M : ℝ} (hΔ : Δ < 1) (hM : 3 ≤ M) :
        ∫ (t : ℝ) in 3..M, ((t - 1) / t) ^ compactHeadTheta Δ * hatTailIntegrand H sign t < weightedHat H sign 3

        Direct Lemma-13.3 witness with the corrected positive exponent. This is the strict compactness input behind the quantitative margin.

        source
        theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.eventually_compactHead_le_coefficient_sub_margin {H : Section13HatLayers} (hH : Section13HatContract H 2) (sign : ErrorSign) {d Δ M : ℝ} (hd : 0 ≤ d) (hΔ : Δ < 1) (hM : 3 ≤ M) :
        0 < compactHeadMargin Δ M ∧ ∃ (D₀ : ℝ), 1 < D₀ ∧ ∀ (D : ℝ), D₀ ≤ D → ∫ (t : ℝ) in 3..M, qD H sign.opposite D d Δ t ≤ (compactHeadCoefficient Δ M - compactHeadMargin Δ M) * lambda H sign D d 0 3

        Explicit positive-margin form of the fixed compact head. The established DDE/FTC compact-head estimate actually has the stronger coefficient (1 - 1/M)^(1-Δ). Rewriting that coefficient as compactHeadCoefficient - compactHeadMargin exposes a fixed positive amount which is available for absorbing the moving tail.

        The threshold is fixed after M; no fixed-endpoint theorem is diagonalized at a moving source cutoff.