Screened residual comparison at arbitrary depth

The full screened residual comparison and continuous outer-mass estimates yield integral majorants for fixed-depth boundary contributions.

All declarations retain the MathlibNt.SieveTheory.SwitchingPrinciple namespace.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserBoundaryScreenedResidualComparison (k : ℕ) (K ρ c s₁ : ℝ) (hK : 1 ≤ K) (hρ : 0 < ρ) (hc : 0 < c) : ∃ (z₀ : ℝ), 2 ≤ z₀ ∧ ∀ (S : BoundingSieve) (z : ℝ) (q : ℕ), z₀ ≤ z → HasDimensionOneLocalProductBound S K → UpperRosserBoundaryScreenedResidualComparison S z q k ρ c s₁

Fixed-depth residual comparisons for every positive screen. Internally a smaller screen below one is used when necessary; strengthening the screen then gives the stated predicate.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserBoundaryChainsFixedDepthDensity_le_boundaryMassAux_add (k : ℕ) (K ρ c s₁ : ℝ) (hK : 1 ≤ K) (hρ : 0 < ρ) (hc : 0 < c) : ∃ (z₀ : ℝ), 2 ≤ z₀ ∧ ∀ (S : BoundingSieve) (z Δ s b : ℝ) (q : ℕ) (P : Finset ℕ), z₀ ≤ z → 0 < Δ → HasDimensionOneLocalProductBound S K → s = Real.log Δ / Real.log z → s ∈ Set.Ioc 0 s₁ → Nat.Prime q → q ∉ P → P ⊆ S.prodPrimes.primeFactors → (∀ p ∈ P, q ≤ p) → (∀ p ∈ P, Real.log ↑p / Real.log z < b) → c ≤ Real.log ↑q / Real.log z → b ≤ 1 → LinearSieve.upperRosserBoundaryChainsFixedDepthDensity (fun (p : ℕ) => S.nu p / (1 - S.nu p)) (⌊Δ⌋₊ + 1) q P k ≤ LinearSieve.upperRosserBoundaryMassAux k s (Real.log ↑q / Real.log z) b + ρ

Uniform fixed-depth comparison on a positive bounded level range. The strict inherited face and its bound by one already force every prime in the carrier below the ambient cutoff z.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserBoundaryChainsFixedDepthDensity_le_boundaryMassAux_add_depth_screen (k : ℕ) (K ρ s₁ : ℝ) (hK : 1 ≤ K) (hρ : 0 < ρ) : ∃ (z₀ : ℝ), 2 ≤ z₀ ∧ ∀ (S : BoundingSieve) (z Δ s b : ℝ) (q : ℕ) (P : Finset ℕ), z₀ ≤ z → 0 < Δ → HasDimensionOneLocalProductBound S K → s = Real.log Δ / Real.log z → s ∈ Set.Ioc 0 s₁ → Nat.Prime q → q ∉ P → P ⊆ S.prodPrimes.primeFactors → (∀ p ∈ P, q ≤ p) → (∀ p ∈ P, Real.log ↑p / Real.log z < b) → 1 / (2 * 3 ^ k) ≤ Real.log ↑q / Real.log z → b ≤ 1 → LinearSieve.upperRosserBoundaryChainsFixedDepthDensity (fun (p : ℕ) => S.nu p / (1 - S.nu p)) (⌊Δ⌋₊ + 1) q P k ≤ LinearSieve.upperRosserBoundaryMassAux k s (Real.log ↑q / Real.log z) b + ρ

Fixed-depth comparison at the lower screen forced by a nonzero outer depth-k contribution.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserBoundaryChainsFixedDepthDensity_le_boundaryMass_add_depth_screen (k : ℕ) (K ρ s₁ : ℝ) (hK : 1 ≤ K) (hρ : 0 < ρ) : ∃ (z₀ : ℝ), 2 ≤ z₀ ∧ ∀ (S : BoundingSieve) (z Δ s : ℝ) (q : ℕ) (P : Finset ℕ), z₀ ≤ z → 0 < Δ → HasDimensionOneLocalProductBound S K → s = Real.log Δ / Real.log z → s ∈ Set.Ioc 0 s₁ → Nat.Prime q → q ∉ P → P ⊆ S.prodPrimes.primeFactors → (∀ p ∈ P, q ≤ p) → (∀ p ∈ P, ↑p ≤ z) → 1 / (2 * 3 ^ k) < Real.log ↑q / Real.log z → LinearSieve.upperRosserBoundaryChainsFixedDepthDensity (fun (p : ℕ) => S.nu p / (1 - S.nu p)) (⌊Δ⌋₊ + 1) q P k ≤ LinearSieve.upperRosserBoundaryMass k s (Real.log ↑q / Real.log z) + ρ

The depth-dependent pointwise comparison at upper face 1 remains valid when the carrier is only known to lie in the closed cutoff p ≤ z. The proof approaches z from above, where the inherited face is strict, and uses positive-depth continuity; depth zero is exact.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_sum_nu_div_one_sub_mul_inv_mul_upperRosserBoundaryMass_succ_le_integral_add (k : ℕ) (K ρ : ℝ) (hK : 1 ≤ K) (hρ : 0 < ρ) : ∃ (z₀ : ℝ), 2 ≤ z₀ ∧ ∀ (S : BoundingSieve) (z s : ℝ) (T : Finset ℕ), z₀ ≤ z → HasDimensionOneLocalProductBound S K → T ⊆ S.prodPrimes.primeFactors → (∀ p ∈ T, Real.log ↑p / Real.log z ∈ Set.Icc (1 / (2 * 3 ^ (k + 1))) 1) → s ∈ Set.Icc (3 / 2) 4 → ∑ p ∈ T, S.nu p / (1 - S.nu p) * ((Real.log ↑p / Real.log z)⁻¹ * LinearSieve.upperRosserBoundaryMass (k + 1) s (Real.log ↑p / Real.log z)) ≤ (∫ (a : ℝ) in Set.Ioo 0 1, a⁻¹ * a⁻¹ * LinearSieve.upperRosserBoundaryMass (k + 1) s a) + ρ

At every positive fixed depth, the continuous outer boundary mass admits a uniform Stieltjes transfer on 3 / 2 ≤ s ≤ 4. Joint continuity on the compact level/cutoff box supplies the common mesh modulus.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_sum_mul_upperRosserBoundaryChainsFixedDepthDensity_succ_le_integral_add_of_three_halves_le (k : ℕ) (K ρ : ℝ) (hK : 1 ≤ K) (hρ : 0 < ρ) : ∃ (z₀ : ℝ), 2 ≤ z₀ ∧ ∀ (S : BoundingSieve) (z Δ s : ℝ), z₀ ≤ z → 0 < Δ → HasDimensionOneLocalProductBound S K → (∀ p ∈ S.prodPrimes.primeFactors, ↑p ≤ z) → s = Real.log Δ / Real.log z → 3 / 2 ≤ s → s ≤ 4 → ∑ q ∈ S.prodPrimes.primeFactors, S.nu q / (1 - S.nu q) * LinearSieve.upperRosserBoundaryChainsFixedDepthDensity (fun (p : ℕ) => S.nu p / (1 - S.nu p)) (⌊Δ⌋₊ + 1) q ({p ∈ S.prodPrimes.primeFactors | q < p}) (k + 1) ≤ (∫ (a : ℝ) in Set.Ioo 0 1, a⁻¹ * a⁻¹ * LinearSieve.upperRosserBoundaryMass (k + 1) s a) + ρ

Every positive fixed-depth complete outer Rosser contribution converges uniformly on the upper-sieve range to its continuous boundary integral.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_sum_nu_div_one_sub_mul_inv_mul_upperRosserBoundaryMass_one_le_integral_add_of_three_halves_le (K ρ : ℝ) (hK : 1 ≤ K) (hρ : 0 < ρ) : ∃ (z₀ : ℝ), 2 ≤ z₀ ∧ ∀ (S : BoundingSieve) (z s : ℝ) (T : Finset ℕ), z₀ ≤ z → HasDimensionOneLocalProductBound S K → T ⊆ S.prodPrimes.primeFactors → (∀ p ∈ T, Real.log ↑p / Real.log z ∈ Set.Icc (1 / 6) 1) → 3 / 2 ≤ s → ∑ p ∈ T, S.nu p / (1 - S.nu p) * ((Real.log ↑p / Real.log z)⁻¹ * LinearSieve.upperRosserBoundaryMass 1 s (Real.log ↑p / Real.log z)) ≤ (∫ (a : ℝ) in Set.Ioo 0 1, a⁻¹ * a⁻¹ * LinearSieve.upperRosserBoundaryMass 1 s a) + ρ

The outer prime sum weighted by the complete continuous depth-two mass is, uniformly on the upper-sieve range, bounded by the depth-two boundary integral. This is the final one-dimensional Stieltjes step in the depth-two comparison.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_screenedResidualBoundaryMass_le_integral_add_of_three_halves_le (K ρ : ℝ) (hK : 1 ≤ K) (hρ : 0 < ρ) : ∃ (z₀ : ℝ), 2 ≤ z₀ ∧ ∀ (S : BoundingSieve) (z Δ s : ℝ), z₀ ≤ z → 0 < Δ → HasDimensionOneLocalProductBound S K → (∀ p ∈ S.prodPrimes.primeFactors, ↑p ≤ z) → s = Real.log Δ / Real.log z → 3 / 2 ≤ s → s ≤ 4 → ∑ q ∈ S.prodPrimes.primeFactors with 1 / 6 < Real.log ↑q / Real.log z, S.nu q / (1 - S.nu q) * ∑ p₀ ∈ {p ∈ S.prodPrimes.primeFactors | q < p} with 1 / 6 < Real.log ↑p₀ / Real.log z, ∑ p₁ ∈ {p ∈ S.prodPrimes.primeFactors | q < p} with p₁ < p₀ ∧ p₀ ^ 3 < ⌊Δ⌋₊ + 1 ∧ 1 / 6 < Real.log ↑p₁ / Real.log z, S.nu p₀ / (1 - S.nu p₀) * (S.nu p₁ / (1 - S.nu p₁)) * LinearSieve.upperRosserBoundaryMassAux 0 (s - Real.log ↑p₀ / Real.log z - Real.log ↑p₁ / Real.log z) (Real.log ↑q / Real.log z) (Real.log ↑p₁ / Real.log z) ≤ (∫ (a : ℝ) in Set.Ioo 0 1, a⁻¹ * a⁻¹ * LinearSieve.upperRosserBoundaryMass 1 s a) + ρ

The screened depth-two residual prime sum is uniformly bounded by its continuous boundary integral.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_sum_mul_upperRosserBoundaryChainsFixedDepthDensity_one_le_integral_add_of_three_halves_le (K ρ : ℝ) (hK : 1 ≤ K) (hρ : 0 < ρ) : ∃ (z₀ : ℝ), 2 ≤ z₀ ∧ ∀ (S : BoundingSieve) (z Δ s : ℝ), z₀ ≤ z → 0 < Δ → HasDimensionOneLocalProductBound S K → (∀ p ∈ S.prodPrimes.primeFactors, ↑p ≤ z) → s = Real.log Δ / Real.log z → 3 / 2 ≤ s → s ≤ 4 → ∑ q ∈ S.prodPrimes.primeFactors, S.nu q / (1 - S.nu q) * LinearSieve.upperRosserBoundaryChainsFixedDepthDensity (fun (p : ℕ) => S.nu p / (1 - S.nu p)) (⌊Δ⌋₊ + 1) q ({p ∈ S.prodPrimes.primeFactors | q < p}) 1 ≤ (∫ (a : ℝ) in Set.Ioo 0 1, a⁻¹ * a⁻¹ * LinearSieve.upperRosserBoundaryMass 1 s a) + ρ

Uniform depth-two comparison between the explicit finite Rosser boundary sum and its continuous Buchstab integral.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_sum_nu_div_one_sub_mul_upperRosserBoundaryMassAux_zero_le_rpow_partition_Icc_add (ι : Type u_1) [Fintype ι] [DecidableEq ι] (K ρ c : ℝ) (hK : 1 ≤ K) (hρ : 0 < ρ) (hc : 0 < c) : ∃ (z₀ : ℝ), 2 ≤ z₀ ∧ ∀ (S : BoundingSieve) (z s x₀ a : ℝ) (T : Finset ℕ) (cell : ℕ → ι) (u v : ι → ℝ), z₀ ≤ z → HasDimensionOneLocalProductBound S K → (∀ (i : ι), c ≤ u i) → (∀ (i : ι), u i ≤ v i) → T ⊆ S.prodPrimes.primeFactors → (∀ p ∈ T, z ^ u (cell p) ≤ ↑p ∧ ↑p ≤ z ^ v (cell p)) → ∑ p ∈ T, S.nu p / (1 - S.nu p) * LinearSieve.upperRosserBoundaryMassAux 0 (s - x₀ - Real.log ↑p / Real.log z) a (Real.log ↑p / Real.log z) ≤ ∑ i : ι, (v i / u i * (1 + K / (u i * Real.log z)) - 1) + ρ

Fixed-mesh inner depth-two estimate with its closed-face hypothesis discharged uniformly. A common positive lower bound for the mesh supplies the atom cutoff; no additional analytic hypothesis is required.