Logarithmic kernel bounds and residual errors

Quantitative continuity bounds for boundary log kernels control residual-error factors and establish screened comparison below the unit parameter.

All declarations retain the MathlibNt.SieveTheory.SwitchingPrinciple namespace.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.abs_log_sub_log_le_inv_of_lower {c x y : ℝ} (hc : 0 < c) (hx : c ≤ x) (hy : c ≤ y) : |Real.log x - Real.log y| ≤ c⁻¹ * |x - y|

The logarithm is Lipschitz above an arbitrary positive lower screen.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.abs_log_div_sub_log_div_le_inv_of_lower {c x a y b : ℝ} (hc : 0 < c) (hx : c ≤ x) (ha : c ≤ a) (hy : c ≤ y) (hb : c ≤ b) : |Real.log (x / a) - Real.log (y / b)| ≤ c⁻¹ * (|x - y| + |a - b|)

Logarithmic ratios are Lipschitz when all coordinates stay above a positive screen.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.abs_upperRosserBoundaryLogKernel_sub_le_of_lower {c s a x₀ t b y₀ : ℝ} (hc : 0 < c) (ha : c ≤ a) (hax₀ : a ≤ x₀) (hb : c ≤ b) (hby₀ : b ≤ y₀) : |LinearSieve.upperRosserBoundaryLogKernel s a x₀ - LinearSieve.upperRosserBoundaryLogKernel t b y₀| ≤ c⁻¹ * (2 * |x₀ - y₀| + |s - t| + 4 * |a - b|)

The logarithmic boundary kernel is uniformly Lipschitz on any fixed positive screen.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserBoundaryLogKernel_le_log_inv_of_lower {c s a x₀ : ℝ} (hc : 0 < c) (hc1 : c ≤ 1) (ha : c ≤ a) (hx₀ : x₀ ≤ 1) : LinearSieve.upperRosserBoundaryLogKernel s a x₀ ≤ Real.log c⁻¹

The logarithmic boundary kernel is bounded on an arbitrary positive screen.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.abs_upperRosserBoundaryLogKernel_sub_le_of_screen {c s a x y : ℝ} (hc : 0 < c) (ha : c ≤ a) : |LinearSieve.upperRosserBoundaryLogKernel s a x - LinearSieve.upperRosserBoundaryLogKernel s a y| ≤ 2 * c⁻¹ * |x - y|

Extending the logarithmic boundary kernel by zero below its ordered region preserves a Lipschitz bound on an arbitrary positive screen.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.abs_upperRosserBoundaryLogKernel_sub_le_of_one_sixth_le {s a x y : ℝ} (ha : 1 / 6 ≤ a) : |LinearSieve.upperRosserBoundaryLogKernel s a x - LinearSieve.upperRosserBoundaryLogKernel s a y| ≤ 12 * |x - y|

The explicit logarithmic kernel remains uniformly Lipschitz when extended by zero below its ordered region.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserBoundaryChainsFixedDepthDensity_one_le_boundaryMassAux_add_screened (K ρ c : ℝ) (hK : 1 ≤ K) (hρ : 0 < ρ) (hc : 0 < c) (hc1 : c < 1) : ∃ (z₀ : ℝ), 2 ≤ z₀ ∧ ∀ (S : BoundingSieve) (z Δ s b : ℝ) (q : ℕ) (P : Finset ℕ), z₀ ≤ z → 0 < Δ → HasDimensionOneLocalProductBound S K → s = Real.log Δ / Real.log z → 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 1 ≤ LinearSieve.upperRosserBoundaryMassAux 1 s (Real.log ↑q / Real.log z) b + ρ

Uniform two-stage Stieltjes transfer for the first positive residual depth. The distinguished prime is screened away from zero, while the exact inherited upper face b is retained.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserBoundaryChainsFixedDepthDensity_one_le_boundaryMassAux_add (K ρ : ℝ) (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 → Nat.Prime q → q ∉ P → P ⊆ S.prodPrimes.primeFactors → (∀ p ∈ P, q ≤ p) → (∀ p ∈ P, Real.log ↑p / Real.log z < b) → 1 / 6 ≤ Real.log ↑q / Real.log z → b ≤ 1 → LinearSieve.upperRosserBoundaryChainsFixedDepthDensity (fun (p : ℕ) => S.nu p / (1 - S.nu p)) (⌊Δ⌋₊ + 1) q P 1 ≤ LinearSieve.upperRosserBoundaryMassAux 1 s (Real.log ↑q / Real.log z) b + ρ

Compatibility specialization of the depth-one comparison to the traditional one-sixth screen.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserResidualErrorFactor_le (K c : ℝ) (hK : 1 ≤ K) (hc : 0 < c) : ∃ (z₀ : ℝ), 2 ≤ z₀ ∧ ∀ (z : ℝ), z₀ ≤ z → -1 ≤ Real.log (z + 1) / Real.log (z ^ c) * (1 + K / Real.log (z ^ c)) - 1 ∧ Real.log (z + 1) / Real.log (z ^ c) * (1 + K / Real.log (z ^ c)) - 1 ≤ 4 / c

Above a fixed cutoff depending only on the local-product constant and a positive screen, the residual-error factor is uniformly bounded.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserBoundaryChainsFixedDepthDensity_succ_succ_le_boundaryMassAux_add (k : ℕ) (K ρ c s₀ s₁ : ℝ) (hK : 1 ≤ K) (hρ : 0 < ρ) (hc : 0 < c) (hc1 : c < 1) : ∃ (ε : ℝ), 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.Icc s₀ 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 → UpperRosserBoundaryScreenedResidualComparison S z q (k + 1) ε c s₁ → LinearSieve.upperRosserBoundaryChainsFixedDepthDensity (fun (p : ℕ) => S.nu p / (1 - S.nu p)) (⌊Δ⌋₊ + 1) q P (k + 2) ≤ LinearSieve.upperRosserBoundaryMassAux (k + 2) s (Real.log ↑q / Real.log z) b + ρ

A screened positive-depth residual comparison advances by one Rosser pair. The inherited upper face is retained, and every analytic cutoff is uniform on the displayed compact level interval.

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

Fixed-depth screened residual comparisons are uniform above a cutoff that depends only on the depth, the local-product constant, the requested error, and the upper end of the level range. The distinguished prime and inherited face remain arbitrary.