Scale-faithful quantitative joint diagonal for the upper Rosser density

This module records the minimal quantifier-correct strengthening of the current fixed-depth mesh and absolute aggregate-tail producers. Both estimates retain the ambient Euler product. In particular, no cancellation or division by that product is used.

The current fixed-depth proof does not itself provide the two contracts below. Its depth-k+1 screen is c = 1 / (2 * 3^(k+1)), its displayed majorant is B = c⁻¹ * (c⁻¹ * c⁻¹)^(k+1), and its uniform-continuity modulus is selected nonquantitatively. Thus the source currently exposes no bound for z₀(k, ε) that can be checked at a moving depth such as k ≍ log log z.

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserRelativePrefix (S : BoundingSieve) (Δ : ℝ) (T : ℕ) : ℝ

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserRelativePrefix S Δ T = ∑ q ∈ S.prodPrimes.primeFactors, S.nu q / (1 - S.nu q) * ∑ k ∈ Finset.range T, MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryChainsFixedDepthRelativeDensity (⇑S.nu) (⌊Δ⌋₊ + 1) q ({p ∈ S.prodPrimes.primeFactors | q < p}) k

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserRelativeTail (S : BoundingSieve) (Δ : ℝ) (T : ℕ) : ℝ

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserRelativeTail S Δ T = ∑ q ∈ S.prodPrimes.primeFactors, S.nu q / (1 - S.nu q) * ∑ j ∈ Finset.range (S.prodPrimes.primeFactors.card + 1 - T), MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryChainsFixedDepthRelativeDensity (⇑S.nu) (⌊Δ⌋₊ + 1) q ({p ∈ S.prodPrimes.primeFactors | q < p}) (T + j)

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserEulerScale (S : BoundingSieve) : ℝ

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserEulerScale S = AnalyticNumberTheory.Sieve.sieveProductPrimeFactors S

def MathlibNt.SieveTheory.SwitchingPrinciple.UpperRosserScaledFixedDepthPrefixProducer (H : SuzukiLemma144KappaOne.Section13HatLayers) (_hH : SuzukiLemma144KappaOne.Section13HatSourceContract H) : Prop

Fixed-depth prefix comparison in the exact relative coordinates of the finite decomposition. The threshold may depend on the selected depth, but is chosen before the varying sieve and endpoint.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.UpperRosserScaledFixedDepthPrefixProducer H _hH = ∀ (K ε : ℝ), 1 < K → 0 < ε → ∀ (T : ℕ), ∃ (z₀ : ℝ), ∀ (S : BoundingSieve) (z Δ s : ℝ), z₀ ≤ z → 2 ≤ z → 0 < Δ → MathlibNt.SieveTheory.SwitchingPrinciple.HasDimensionOneLocalProductBound S K → (∀ p ∈ S.prodPrimes.primeFactors, ↑p ≤ z) → s = Real.log Δ / Real.log z → 3 / 2 ≤ s → s ≤ 4 → have T' := min T (S.prodPrimes.primeFactors.card + 1); (1 + MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserRelativePrefix S Δ T') * MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserEulerScale S ≤ (MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertUpperLinearSieveFactor s + ε) * MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserEulerScale S

def MathlibNt.SieveTheory.SwitchingPrinciple.UpperRosserScaledRelativeTailProducer : Prop

Uniform relative-tail producer. Unlike the existing absolute estimate tail * V ≤ τ(T), this conclusion is already at the required ε * V scale. The same fixed depth works for every later sieve and endpoint.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.UpperRosserScaledRelativeTailProducer = ∀ (K ε : ℝ), 1 < K → 0 < ε → ∃ (T : ℕ) (z₀ : ℝ), ∀ (S : BoundingSieve) (z Δ s : ℝ), z₀ ≤ z → 2 ≤ z → 0 < Δ → MathlibNt.SieveTheory.SwitchingPrinciple.HasDimensionOneLocalProductBound S K → (∀ p ∈ S.prodPrimes.primeFactors, ↑p ≤ z) → s = Real.log Δ / Real.log z → 3 / 2 ≤ s → s ≤ 4 → have T' := min T (S.prodPrimes.primeFactors.card + 1); MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserRelativeTail S Δ T' * MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserEulerScale S ≤ ε * MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserEulerScale S

theorem MathlibNt.SieveTheory.SwitchingPrinciple.UpperRosserScaledPrefixTailComparison.of_scaleFaithfulProducers (H : SuzukiLemma144KappaOne.Section13HatLayers) (hH : SuzukiLemma144KappaOne.Section13HatSourceContract H) (hprefix : UpperRosserScaledFixedDepthPrefixProducer H hH) (htail : UpperRosserScaledRelativeTailProducer) : UpperRosserScaledPrefixTailComparison H hH

The two scale-faithful producers close the frozen final interface. The tail chooses the depth first; the fixed-depth prefix theorem is then invoked at that same depth, and the two endpoint thresholds are joined by a maximum.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.absoluteTailBound_does_not_imply_relativeScale (τ : ℝ) : 0 < τ → ∃ (V : ℝ) (E : ℝ), 0 < V ∧ 0 ≤ E ∧ E ≤ τ ∧ ¬E ≤ V

An arbitrarily small absolute error does not pay the same relative error at an independently shrinking positive scale. Taking V = τ/2 and E = τ models exactly why E ≤ τ cannot be promoted to E ≤ V uniformly.