Documentation

MathlibNt.SieveTheory.LinearSieve.Suzuki.SuzukiLemma144Sigma0UniformityBoundary

Lemma 14.4: the low-prime endpoint and the uniformity boundary #

The discrete object in Claim 14.5 has real cutoff arguments, whereas the actual recurrence has natural cutoff arguments. suzukiActualTReal is the canonical rounded adapter. On the natural arguments occurring in the recurrence it is literally suzukiActualT.

The currently reachable Claim-14.5 interface is pointwise eventual: N, s and the other endpoint data are fixed before its threshold is chosen. In the low-prime sum, however, s = recursiveCoordinate D p, and both that coordinate and the carrier prime vary after the outer D is chosen. Consequently the pointwise theorem does not justify moving its threshold in front of D. ActualSigmaZeroClaim145Uniformity freezes exactly that missing quantifier swap. The final theorem below is only the finite-sum algebra showing that this uniform statement is sufficient; it is not advertised as an internal proof of the missing uniformity.

source
noncomputable def MathlibNt.SieveTheory.suzukiActualTReal (S : BoundingSieve) :
ℕ → ℝ → ℝ → ℝ

Real-argument adapter for the actual natural-valued parity aggregate.

Equations
Instances For
    source
    @[simp]
    theorem MathlibNt.SieveTheory.suzukiActualTReal_natCast (S : BoundingSieve) (N D z : ℕ) :
    suzukiActualTReal S N ↑D ↑z = suzukiActualT S N D z
    source
    noncomputable def MathlibNt.SieveTheory.suzukiSigmaZeroClaim145Budget (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (N D z : ℕ) (d Δ σ K C145 : ℝ) :
    ℝ

    The sum of the pointwise Claim-14.5 budgets at the literal recursive arguments of the low-prime part of (14.9).

    Equations
    Instances For
      source
      def MathlibNt.SieveTheory.ActualSigmaZeroClaim145Uniformity (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (d Δ σ K C145 : ℝ) :
      Prop

      The genuine uniformity needed to apply Claim 14.5 inside Σ₀.

      The threshold is selected before D, N, and the carrier prime. The two coordinate hypotheses are the actual Claim-14.5 domain hypotheses; neither a Claim-14.5 conclusion nor a bound for Σ₀ is hidden among the source data of a purported endpoint theorem.

      Equations
      Instances For
        source
        theorem MathlibNt.SieveTheory.suzukiSigmaZero_eventually_le_claim145Budget_of_uniformity (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {d Δ σ K C145 : ℝ} (huniform : ActualSigmaZeroClaim145Uniformity S H d Δ σ K C145) (hnu : ∀ (z p : ℕ), p ∈ SwitchingPrinciple.suzukiSupportedBelow S z → 0 ≤ S.nu p) (hq2 : ∀ (D N z p : ℕ), 2 ≤ N → p ∈ {q ∈ SwitchingPrinciple.suzukiSupportedBelow S z | ↑q < ↑D ^ (1 / σ)} → 2 ≤ D ⌈/⌉ p) (hdom : ∀ (D N z p : ℕ), 2 ≤ N → p ∈ {q ∈ SwitchingPrinciple.suzukiSupportedBelow S z | ↑q < ↑D ^ (1 / σ)} → SwitchingPrinciple.SuzukiLemma144Equation1410.recursiveCoordinate D p ∈ SuzukiFiniteContinuousLayers.suzukiParityDomainOne 2 (N - 1)) (hcoordσ : ∀ (D N z p : ℕ), 2 ≤ N → p ∈ {q ∈ SwitchingPrinciple.suzukiSupportedBelow S z | ↑q < ↑D ^ (1 / σ)} → SwitchingPrinciple.SuzukiLemma144Equation1410.recursiveCoordinate D p ≤ σ) :
        ∃ (D₀ : ℝ), 1 < D₀ ∧ ∀ (D N z : ℕ), D₀ ≤ ↑D → 2 ≤ N → suzukiSigmaZero S N D z (↑D ^ (1 / σ)) ≤ suzukiSigmaZeroClaim145Budget S H N D z d Δ σ K C145

        Once the genuinely uniform Claim-14.5 statement is available, the endpoint estimate is just monotonicity of the finite low-prime sum. This lemma makes the remaining analytic obligation exact; it does not accept the desired Σ₀ inequality as a premise.