Stieltjes and integral comparisons for alternating pairs

Uniform screened Stieltjes estimates, thickened indicators, and log-ratio integrals transfer weighted prime sums to normalized alternating-pair kernels.

All declarations retain the MathlibNt.SieveTheory.SwitchingPrinciple namespace.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_weighted_sum_nu_div_one_sub_le_integral_add_screened (K ρ B L c : ℝ) (hK : 1 ≤ K) (hρ : 0 < ρ) (hB : 0 ≤ B) (hL : 0 ≤ L) (hc : 0 < c) (hc1 : c < 1) : ∃ (z₀ : ℝ), 2 ≤ z₀ ∧ ∀ (S : BoundingSieve) (z : ℝ) (T : Finset ℕ) (w : ℕ → ℝ) (f : ℝ → ℝ), z₀ ≤ z → HasDimensionOneLocalProductBound S K → T ⊆ S.prodPrimes.primeFactors → (∀ p ∈ T, Real.log ↑p / Real.log z ∈ Set.Icc c 1) → (∀ x ∈ Set.Icc c 1, 0 ≤ f x) → (∀ x ∈ Set.Icc c 1, f x ≤ B) → (∀ x ∈ Set.Icc c 1, ∀ y ∈ Set.Icc c 1, |f x - f y| ≤ L * |x - y|) → MeasureTheory.IntegrableOn (fun (x : ℝ) => x⁻¹ * f x) (Set.Ioo c 1) MeasureTheory.volume → (∀ p ∈ T, 0 ≤ w p ∧ w p ≤ f (Real.log ↑p / Real.log z)) → ∑ p ∈ T, w p * (S.nu p / (1 - S.nu p)) ≤ (∫ (x : ℝ) in Set.Ioo c 1, x⁻¹ * f x) + ρ

Uniform Stieltjes comparison on an arbitrary fixed positive logarithmic screen.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_weighted_sum_nu_div_one_sub_le_integral_add_screened_of_uniform_modulus (K ρ B c δ : ℝ) (hK : 1 ≤ K) (hρ : 0 < ρ) (hB : 0 ≤ B) (hc : 0 < c) (hc1 : c < 1) (hδ : 0 < δ) : ∃ (z₀ : ℝ), 2 ≤ z₀ ∧ ∀ (S : BoundingSieve) (z : ℝ) (T : Finset ℕ) (w : ℕ → ℝ) (f : ℝ → ℝ), z₀ ≤ z → HasDimensionOneLocalProductBound S K → T ⊆ S.prodPrimes.primeFactors → (∀ p ∈ T, Real.log ↑p / Real.log z ∈ Set.Icc c 1) → (∀ x ∈ Set.Icc c 1, 0 ≤ f x) → (∀ x ∈ Set.Icc c 1, f x ≤ B) → (∀ x ∈ Set.Icc c 1, ∀ y ∈ Set.Icc c 1, |x - y| < δ → |f x - f y| < ρ * c / 12) → MeasureTheory.IntegrableOn (fun (x : ℝ) => x⁻¹ * f x) (Set.Ioo c 1) MeasureTheory.volume → (∀ p ∈ T, 0 ≤ w p ∧ w p ≤ f (Real.log ↑p / Real.log z)) → ∑ p ∈ T, w p * (S.nu p / (1 - S.nu p)) ≤ (∫ (x : ℝ) in Set.Ioo c 1, x⁻¹ * f x) + ρ

A common uniform modulus on a positive logarithmic screen is enough for a uniform weighted Stieltjes comparison. Unlike the Lipschitz specialization, this form applies uniformly to compact continuous families.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.integral_thickenedIndicator_mul_le_integral_Ioo_add_screened {c δ u v C : ℝ} (hδ : 0 < δ) (hu : c ≤ u) (huv : u ≤ v) (hv : v ≤ 1) (hC : 0 ≤ C) {g : ℝ → ℝ} (hint : MeasureTheory.IntegrableOn g (Set.Ioo c 1) MeasureTheory.volume) (hg : ∀ x ∈ Set.Ioo c 1, 0 ≤ g x ∧ g x ≤ C) : ∫ (x : ℝ) in Set.Ioo c 1, ↑((thickenedIndicator hδ (Set.Icc u v)) x) * g x ≤ (∫ (x : ℝ) in Set.Ioo u v, g x) + 2 * C * δ

Thickening an interval by δ changes the integral of a nonnegative uniformly bounded function by at most the two boundary strips.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.integral_thickenedIndicator_mul_le_integral_Ioo_add {δ u v C : ℝ} (hδ : 0 < δ) (hu : 1 / 6 ≤ u) (huv : u ≤ v) (hv : v ≤ 1) (hC : 0 ≤ C) {g : ℝ → ℝ} (hint : MeasureTheory.IntegrableOn g (Set.Ioo (1 / 6) 1) MeasureTheory.volume) (hg : ∀ x ∈ Set.Ioo (1 / 6) 1, 0 ≤ g x ∧ g x ≤ C) : ∫ (x : ℝ) in Set.Ioo (1 / 6) 1, ↑((thickenedIndicator hδ (Set.Icc u v)) x) * g x ≤ (∫ (x : ℝ) in Set.Ioo u v, g x) + 2 * C * δ

Compatibility specialization of the thickened-interval estimate to the traditional one-sixth screen.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_weighted_sum_nu_div_one_sub_le_integral_Ioo_add (K ρ B L : ℝ) (hK : 1 ≤ K) (hρ : 0 < ρ) (hB : 0 ≤ B) (hL : 0 ≤ L) : ∃ (z₀ : ℝ), 2 ≤ z₀ ∧ ∀ (S : BoundingSieve) (z : ℝ) (T : Finset ℕ) (w : ℕ → ℝ) (f : ℝ → ℝ) (u v : ℝ), z₀ ≤ z → HasDimensionOneLocalProductBound S K → T ⊆ S.prodPrimes.primeFactors → 1 / 6 ≤ u → u ≤ v → v ≤ 1 → (∀ p ∈ T, Real.log ↑p / Real.log z ∈ Set.Icc u v) → (∀ x ∈ Set.Icc (1 / 6) 1, 0 ≤ f x) → (∀ x ∈ Set.Icc (1 / 6) 1, f x ≤ B) → (∀ x ∈ Set.Icc (1 / 6) 1, ∀ y ∈ Set.Icc (1 / 6) 1, |f x - f y| ≤ L * |x - y|) → MeasureTheory.IntegrableOn (fun (x : ℝ) => x⁻¹ * f x) (Set.Ioo (1 / 6) 1) MeasureTheory.volume → (∀ p ∈ T, 0 ≤ w p ∧ w p ≤ f (Real.log ↑p / Real.log z)) → ∑ p ∈ T, w p * (S.nu p / (1 - S.nu p)) ≤ (∫ (x : ℝ) in Set.Ioo u v, x⁻¹ * f x) + ρ

Uniform weighted Stieltjes comparison on any moving subinterval of the screened box. A thickened indicator absorbs both endpoint atoms without requiring the weight to vanish at the moving endpoints.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_weighted_sum_nu_div_one_sub_le_integral_Ioo_add_screened (K ρ B L c : ℝ) (hK : 1 ≤ K) (hρ : 0 < ρ) (hB : 0 ≤ B) (hL : 0 ≤ L) (hc : 0 < c) (hc1 : c < 1) : ∃ (z₀ : ℝ), 2 ≤ z₀ ∧ ∀ (S : BoundingSieve) (z : ℝ) (T : Finset ℕ) (w : ℕ → ℝ) (f : ℝ → ℝ) (u v : ℝ), z₀ ≤ z → HasDimensionOneLocalProductBound S K → T ⊆ S.prodPrimes.primeFactors → c ≤ u → u ≤ v → v ≤ 1 → (∀ p ∈ T, Real.log ↑p / Real.log z ∈ Set.Icc u v) → (∀ x ∈ Set.Icc c 1, 0 ≤ f x) → (∀ x ∈ Set.Icc c 1, f x ≤ B) → (∀ x ∈ Set.Icc c 1, ∀ y ∈ Set.Icc c 1, |f x - f y| ≤ L * |x - y|) → MeasureTheory.IntegrableOn (fun (x : ℝ) => x⁻¹ * f x) (Set.Ioo c 1) MeasureTheory.volume → (∀ p ∈ T, 0 ≤ w p ∧ w p ≤ f (Real.log ↑p / Real.log z)) → ∑ p ∈ T, w p * (S.nu p / (1 - S.nu p)) ≤ (∫ (x : ℝ) in Set.Ioo u v, x⁻¹ * f x) + ρ

Uniform Stieltjes comparison on a moving subinterval of an arbitrary positive logarithmic screen.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_weighted_sum_nu_div_one_sub_le_logRatio_integral_add (K ρ B L R : ℝ) (hK : 1 ≤ K) (hρ : 0 < ρ) (hB : 0 ≤ B) (hL : 0 ≤ L) (hR : 1 < R) : ∃ (Q : ℝ), 2 ≤ Q ∧ ∀ (S : BoundingSieve) (q : ℕ) (T : Finset ℕ) (w : ℕ → ℝ) (f : ℝ → ℝ), Q ≤ ↑q → Nat.Prime q → HasDimensionOneLocalProductBound S K → T ⊆ S.prodPrimes.primeFactors → (∀ p ∈ T, Real.log ↑p / Real.log ↑q ∈ Set.Icc 1 R) → (∀ x ∈ Set.Icc 1 R, 0 ≤ f x) → (∀ x ∈ Set.Icc 1 R, f x ≤ B) → (∀ x ∈ Set.Icc 1 R, ∀ y ∈ Set.Icc 1 R, |f x - f y| ≤ L * |x - y|) → MeasureTheory.IntegrableOn (fun (x : ℝ) => x⁻¹ * f x) (Set.Ioo 1 R) MeasureTheory.volume → (∀ p ∈ T, 0 ≤ w p ∧ w p ≤ f (Real.log ↑p / Real.log ↑q)) → ∑ p ∈ T, w p * (S.nu p / (1 - S.nu p)) ≤ (∫ (x : ℝ) in Set.Ioo 1 R, x⁻¹ * f x) + ρ

Uniform Stieltjes comparison in logarithmic ratios relative to a prime. Rescaling the screened comparison by R turns the base from q into q ^ R; the resulting estimate is uniform in the terminal prime q.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_weighted_sum_nu_div_one_sub_le_logRatio_integral_Ioo_add (K ρ B L R : ℝ) (hK : 1 ≤ K) (hρ : 0 < ρ) (hB : 0 ≤ B) (hL : 0 ≤ L) (hR : 1 < R) : ∃ (Q : ℝ), 2 ≤ Q ∧ ∀ (S : BoundingSieve) (q : ℕ) (T : Finset ℕ) (w : ℕ → ℝ) (f : ℝ → ℝ) (u v : ℝ), Q ≤ ↑q → Nat.Prime q → HasDimensionOneLocalProductBound S K → T ⊆ S.prodPrimes.primeFactors → 1 ≤ u → u ≤ v → v ≤ R → (∀ p ∈ T, Real.log ↑p / Real.log ↑q ∈ Set.Icc u v) → (∀ x ∈ Set.Icc 1 R, 0 ≤ f x) → (∀ x ∈ Set.Icc 1 R, f x ≤ B) → (∀ x ∈ Set.Icc 1 R, ∀ y ∈ Set.Icc 1 R, |f x - f y| ≤ L * |x - y|) → MeasureTheory.IntegrableOn (fun (x : ℝ) => x⁻¹ * f x) (Set.Ioo 1 R) MeasureTheory.volume → (∀ p ∈ T, 0 ≤ w p ∧ w p ≤ f (Real.log ↑p / Real.log ↑q)) → ∑ p ∈ T, w p * (S.nu p / (1 - S.nu p)) ≤ (∫ (x : ℝ) in Set.Ioo u v, x⁻¹ * f x) + ρ

Uniform logarithmic-ratio Stieltjes comparison on moving subintervals. The prime cutoff is independent of the terminal prime and of the endpoints.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserAlternatingPairDiscrete_inner_le_integral_add (K ρ R : ℝ) (hK : 1 ≤ K) (hρ : 0 < ρ) (hR : 3 ≤ R) : ∃ (Q : ℝ), 2 ≤ Q ∧ ∀ (S : BoundingSieve) (q : ℕ) (r y v : ℝ) (T : Finset ℕ), Q ≤ ↑q → Nat.Prime q → HasDimensionOneLocalProductBound S K → 3 ≤ r → y ∈ Set.Icc 1 R → y ≤ v → v ≤ R → T ⊆ S.prodPrimes.primeFactors → (∀ p ∈ T, Real.log ↑p / Real.log ↑q ∈ Set.Icc y v) → ∑ p ∈ T, S.nu p / (1 - S.nu p) * LinearSieve.upperRosserAlternatingPairNormalizedKernel r y (Real.log ↑p / Real.log ↑q) ≤ (∫ (x : ℝ) in Set.Ioo y v, x⁻¹ * LinearSieve.upperRosserAlternatingPairNormalizedKernel r y x) + ρ

One discrete inner reverse-pair sum is uniformly approximated by its continuous logarithmic integral on every fixed ratio window.

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserAlternatingPairNormalizedInnerRaw (r y : ℝ) : ℝ

The explicit normalized mass left after continuously integrating the larger member of one reverse Rosser pair.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserAlternatingPairNormalizedInnerRaw r y = (r ^ 2 / (2 * y ^ 2) + 3 * r / y - 7 / 2 + Real.log ((y + r) / (2 * y))) / r ^ 2

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserAlternatingPairNormalizedInner (r y : ℝ) : ℝ

The nonnegative extension of the normalized inner reverse-pair mass. The raw formula vanishes at y = r and is nonpositive beyond that point.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserAlternatingPairNormalizedInner r y = max 0 (MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserAlternatingPairNormalizedInnerRaw r y)

theorem MathlibNt.SieveTheory.SwitchingPrinciple.integral_upperRosserAlternatingPairNormalizedKernel_inner {r y : ℝ} (_hr : 0 < r) (hy : 0 < y) (hyr : y ≤ r) : ∫ (x : ℝ) in Set.Ioo y ((y + r) / 2), x⁻¹ * LinearSieve.upperRosserAlternatingPairNormalizedKernel r y x = upperRosserAlternatingPairNormalizedInnerRaw r y

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserAlternatingPairNormalizedInner_eq_integral {r y : ℝ} (hr : 0 < r) (hy : 0 < y) (hyr : y ≤ r) : upperRosserAlternatingPairNormalizedInner r y = ∫ (x : ℝ) in Set.Ioo y ((y + r) / 2), x⁻¹ * LinearSieve.upperRosserAlternatingPairNormalizedKernel r y x

theorem MathlibNt.SieveTheory.SwitchingPrinciple.hasDerivAt_upperRosserAlternatingPairNormalizedInnerRaw {r y : ℝ} (hr : 0 < r) (hy : 0 < y) : HasDerivAt (upperRosserAlternatingPairNormalizedInnerRaw r) ((-r ^ 2 / y ^ 3 - 3 * r / y ^ 2 + (1 / (y + r) - 1 / y)) / r ^ 2) y

theorem MathlibNt.SieveTheory.SwitchingPrinciple.abs_upperRosserAlternatingPairNormalizedInnerRaw_deriv_le {r y : ℝ} (hr : 3 ≤ r) (hy : 1 ≤ y) : |(-r ^ 2 / y ^ 3 - 3 * r / y ^ 2 + (1 / (y + r) - 1 / y)) / r ^ 2| ≤ 3

theorem MathlibNt.SieveTheory.SwitchingPrinciple.abs_upperRosserAlternatingPairNormalizedInner_sub_le {r u v R : ℝ} (hr : 3 ≤ r) (hu : u ∈ Set.Icc 1 R) (hv : v ∈ Set.Icc 1 R) : |upperRosserAlternatingPairNormalizedInner r u - upperRosserAlternatingPairNormalizedInner r v| ≤ 3 * |u - v|

The explicit normalized inner mass is uniformly Lipschitz on every positive ratio interval, independently of the reverse-chain state.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserAlternatingPairNormalizedInner_nonneg (r y : ℝ) : 0 ≤ upperRosserAlternatingPairNormalizedInner r y

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserAlternatingPairNormalizedInnerRaw_le_two {r y : ℝ} (hr : 3 ≤ r) (hy : 1 ≤ y) : upperRosserAlternatingPairNormalizedInnerRaw r y ≤ 2

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserAlternatingPairNormalizedInner_le_two {r y : ℝ} (hr : 3 ≤ r) (hy : 1 ≤ y) : upperRosserAlternatingPairNormalizedInner r y ≤ 2

theorem MathlibNt.SieveTheory.SwitchingPrinciple.integrableOn_inv_mul_upperRosserAlternatingPairNormalizedInner {r R : ℝ} (hr : 3 ≤ r) (hR : 1 ≤ R) : MeasureTheory.IntegrableOn (fun (y : ℝ) => y⁻¹ * upperRosserAlternatingPairNormalizedInner r y) (Set.Ioo 1 R) MeasureTheory.volume

theorem MathlibNt.SieveTheory.SwitchingPrinciple.integral_inv_mul_upperRosserAlternatingPairNormalizedInner_le {r v : ℝ} (hr : 3 ≤ r) (_hv : 1 ≤ v) (hvr : v ≤ r) : ∫ (y : ℝ) in Set.Ioo 1 v, y⁻¹ * upperRosserAlternatingPairNormalizedInner r y ≤ 4 / 5

theorem MathlibNt.SieveTheory.SwitchingPrinciple.integral_upperRosserAlternatingPairNormalizedKernel_Ioo_le_inner {r y v : ℝ} (hr : 3 ≤ r) (hy : 1 ≤ y) (hyv : y ≤ v) (hv : v ≤ (y + r) / 2) : ∫ (x : ℝ) in Set.Ioo y v, x⁻¹ * LinearSieve.upperRosserAlternatingPairNormalizedKernel r y x ≤ upperRosserAlternatingPairNormalizedInner r y

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserAlternatingPairDiscrete_outer_le_integral_add (K ρ R : ℝ) (hK : 1 ≤ K) (hρ : 0 < ρ) (hR : 3 ≤ R) : ∃ (Q : ℝ), 2 ≤ Q ∧ ∀ (S : BoundingSieve) (q : ℕ) (r u v : ℝ) (T : Finset ℕ), Q ≤ ↑q → Nat.Prime q → HasDimensionOneLocalProductBound S K → 3 ≤ r → 1 ≤ u → u ≤ v → v ≤ R → T ⊆ S.prodPrimes.primeFactors → (∀ p ∈ T, Real.log ↑p / Real.log ↑q ∈ Set.Icc u v) → ∑ p ∈ T, S.nu p / (1 - S.nu p) * upperRosserAlternatingPairNormalizedInner r (Real.log ↑p / Real.log ↑q) ≤ (∫ (y : ℝ) in Set.Ioo u v, y⁻¹ * upperRosserAlternatingPairNormalizedInner r y) + ρ

The outer member of a compact reverse Rosser pair admits a second uniform Stieltjes transfer after the inner prime has been integrated out.