Documentation

MathlibNt.SieveTheory.LinearSieve.Suzuki.SuzukiMovingSigmaClaim146SourceAssembly

Source-faithful moving assembly of Claim 14.6(iii) #

The source splits at the fixed point M + 2. The compact head is controlled by Lemma 13.3/(14.2), whereas the moving tail is controlled by the large-s DDE argument. Proposition 13.1(iii) is used only to make the endpoint value at M + 2 be O(M⁻²) relative to every starting value in the compact range.

Section13HatContract contains only qualitative convergence weightedHat → 0; it has no quantitative rate from which this M⁻² estimate can be selected. Accordingly the first definition below is the minimal extra DDE-tail interface. It is not Claim 14.6(iii), and it is independent of D, d, Δ, sourceSigma, and the qD integral.

source
def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Proposition131TailDecayContract (H : Section13HatLayers) :
Prop

Minimal quantitative consequence of Proposition 13.1(iii) needed in the moving proof. The source gives the stronger (M log (eM))⁻² decay; only its weaker C M⁻² consequence, together with the monotone comparison back to every 3 ≤ s ≤ M, is retained here.

Equations
Instances For
    source
    def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.FixedCompactPerturbationContract (d M : ℝ) :
    Prop

    The fixed-compact perturbation factors tend uniformly to one. This tiny interface records only the factor 2 needed to transfer Proposition 13.1(iii) from weightedHat to lambda; it is elementary and separate from the DDE.

    Equations
    Instances For
      source
      def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Lemma133WeightedHeadContract (H : Section13HatLayers) (d Δ gap M : ℝ) :
      Prop

      Source Lemma 13.3/(14.2), after the fixed compact prefactors have been absorbed. The positive first-order saving is deliberately gap/(4M); here gap = Δ₀-Δ, correcting the reversed sign in the last two displays on printed p. 92. This is a head estimate, not the final moving claim.

      Equations
      Instances For
        source
        def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.MovingDDEWeightedTailContract (H : Section13HatLayers) (d Δ M : ℝ) :
        Prop

        The already established large-s differential/DDE tail, uniform up to the actual moving source cutoff. Its left endpoint is fixed before D is chosen.

        Equations
        Instances For
          source
          noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.claim146iiiFixedM (C gap : ℝ) :
          ℝ

          A fixed cutoff chosen solely from the Proposition-13.1 constant and the positive source gap. The 16 leaves twice the margin actually needed below.

          Equations
          Instances For
            source
            theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.claim146iiiFixedM_margin {C gap : ℝ} (hC : 0 ≤ C) (hgap : 0 < gap) :
            have M := claim146iiiFixedM C gap; 4 ≤ M ∧ 2 * C / M ^ 2 < gap / (4 * M)
            source
            theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.tendsto_source_weight (gap : ℝ) :
            Filter.Tendsto (fun (σ : ℝ) => (1 - 1 / σ) ^ gap) Filter.atTop (nhds 1)

            The source weight tends to one for every fixed real exponent.

            source
            theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.lambda_pos_of_source_range {H : Section13HatLayers} (hH : Section13HatContract H 2) (sign : ErrorSign) {D d s : ℝ} (hD : 1 < D) (hs : 2 + sign.epsilon ≤ s) :
            0 < lambda H sign D d 0 s

            The perturbed layer is positive throughout the parity-dependent source range.

            source
            theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.lambda_fixed_endpoint_decay {H : Section13HatLayers} {d C M D s : ℝ} (sign : ErrorSign) (hM : 4 ≤ M) (hD : 1 < D) (hs : 2 + sign.epsilon ≤ s) (h131 : weightedHat H sign (M + 2) ≤ C / M ^ 2 * weightedHat H sign s) (hpert : perturbation D d 0 (M + 2) ≤ 2 * perturbation D d 0 s) (hpos : ∀ (sign : ErrorSign) (t : ℝ), 0 < t → 0 < H.T sign t) :
            lambda H sign D d 0 (M + 2) ≤ 2 * C / M ^ 2 * lambda H sign D d 0 s

            Proposition 13.1(iii), plus the harmless fixed-compact perturbation bound, turns the DDE tail endpoint into the required O(M⁻²) multiple of the value at any compact-range starting point.

            source
            theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.moving_claim14_6_iii_of_source_contracts {H : Section13HatLayers} (hH : Section13HatContract H 2) {d Δ gap : ℝ} (_hΔ : Δ < 1) (hgap : 0 < gap) (h131 : Proposition131TailDecayContract H) (hpertAll : ∀ (C : ℝ), 0 ≤ C → FixedCompactPerturbationContract d (claim146iiiFixedM C gap)) (hheadAll : ∀ (C : ℝ), 0 ≤ C → Lemma133WeightedHeadContract H d Δ gap (claim146iiiFixedM C gap)) (htailAll : ∀ (C : ℝ), 0 ≤ C → MovingDDEWeightedTailContract H d Δ (claim146iiiFixedM C gap)) :
            ∃ (D₀ : ℝ), 1 < D₀ ∧ ∀ (D : ℝ), D₀ ≤ D → ∀ (sign : ErrorSign) (s : ℝ), 2 + sign.epsilon ≤ s → s ≤ sourceSigma D d → ∫ (t : ℝ) in s..sourceSigma D d, qD H sign.opposite D d Δ t < (1 - 1 / sourceSigma D d) ^ (1 - Δ) * lambda H sign D d 0 s

            Source-faithful head+tail assembly of moving Claim 14.6(iii).

            The cutoff is fixed as M = max 4 (16 C / gap + 1) before any D threshold is chosen. Consequently the tail coefficient 2C/M² is strictly smaller than the head saving gap/(4M). The theorem does not package its own conclusion as a premise: its four inputs are respectively Proposition 13.1 quantitative decay, elementary compact perturbation, Lemma 13.3 weighted head, and the large-range DDE tail.