Uniform Case-I carrier error transport #

The Claim-14.6 source threshold is chosen before D, N, and s. Enlarging one natural global cutoff puts every ceiling quotient above that threshold and also supplies the low-strip logarithmic estimate used by the full coordinate transport theorem.

source

def MathlibNt.SieveTheory.CaseIErrorEnvelopeTransport (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (N D : ℕ) (d σ s : ℝ) :

Prop

The carrierwise error-envelope comparison consumed by the Case-I successor.

Equations

MathlibNt.SieveTheory.CaseIErrorEnvelopeTransport S H N D d σ s = ∀ p ∈ MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier S.prodPrimes.primeFactors D σ s, MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H (N - 1) (↑(D ⌈/⌉ p)) d (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.recursiveCoordinate D p) ≤ MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H (N - 1) (↑(D ⌈/⌉ p)) d (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedCoordinate D p)

Instances For

source

theorem MathlibNt.SieveTheory.exists_caseI_errorEnvelope_transport_quotient_cutoff_uniform_in_S (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {d Δ : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hd1 : 1 < d) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) :

After one global quotient cutoff, full coordinate antitonicity gives the Case-I error transport simultaneously at every carrier. The two coordinate hypotheses are exactly the geometric facts supplied by the Case-I pointwise packet: the inherited point is in the predecessor parity domain and the recursive point is below the quotient's source endpoint.

source

theorem MathlibNt.SieveTheory.exists_caseI_errorEnvelope_transport_quotient_cutoff (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {d Δ : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hd1 : 1 < d) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) :

Compatibility specialization of the sieve-uniform quotient cutoff.

source

theorem MathlibNt.SieveTheory.caseI_carrier_quotient_scale (S : BoundingSieve) {D Dmin : ℕ} {σ s : ℝ} (hDmin : 2 ≤ Dmin) (hD : Dmin ^ 2 ≤ D) (hs : 2 ≤ s) :

SwitchingPrinciple.SuzukiLemma144Equation1410.CarrierQuotientThresholdGeometry S.prodPrimes.primeFactors D Dmin σ s

A square global cutoff puts every Case-I carrier quotient above the threshold.

source

theorem MathlibNt.SieveTheory.eventually_caseI_errorEnvelope_transport_uniform_in_S (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {d Δ : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hd1 : 1 < d) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) :

Eventual form: the square global cutoff and p < D^(1/s), s ≥ 2 put every natural ceiling quotient above the internal Claim-14.6 threshold. The cutoff precedes N and s.

source

theorem MathlibNt.SieveTheory.eventually_caseI_errorEnvelope_transport_uniform (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {d Δ : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hd1 : 1 < d) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) :

Compatibility specialization of the sieve-uniform eventual theorem.

Documentation

MathlibNt.SieveTheory.LinearSieve.Suzuki.SuzukiLemma144CaseIErrorTransportUniform

Uniform Case-I carrier error transport #