Continuous upper Rosser boundary mass

Recursive boundary mass, measurability, the depth-two logarithmic kernel, Lipschitz estimates, and nonnegativity.

noncomputable def MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryMassAux : ℕ → ℝ → ℝ → ℝ → ℝ

The continuous mass of depth-2k upper Rosser boundary chains. The additional argument b is the inherited strict upper bound for the largest remaining coordinate; retaining it makes pair removal exactly recursive.

Equations

• MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryMassAux 0 x✝² x✝¹ x✝ = if 0 ≤ x✝² ∧ x✝² < 3 * x✝¹ then 1 else 0
• MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryMassAux k.succ x✝² x✝¹ x✝ = ∫ (x₀ : ℝ) in Set.Ioo x✝¹ (min x✝ (x✝² / 3)), x₀⁻¹ * ∫ (x₁ : ℝ) in Set.Ioo x✝¹ x₀, x₁⁻¹ * MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryMassAux k (x✝² - x₀ - x₁) x✝¹ x₁

noncomputable def MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryMass (k : ℕ) (s a : ℝ) : ℝ

The continuous depth-2k boundary mass with the global logarithmic cutoff 1.

Equations

• MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryMass k s a = MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryMassAux k s a 1

@[simp]

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryMassAux_zero (s a b : ℝ) : upperRosserBoundaryMassAux 0 s a b = if 0 ≤ s ∧ s < 3 * a then 1 else 0

theorem MathlibNt.SieveTheory.LinearSieve.continuousAt_upperRosserBoundaryMassAux_zero_level {s a b : ℝ} (hs0 : s ≠ 0) (hs3 : s ≠ 3 * a) : ContinuousAt (fun (t : ℝ) => upperRosserBoundaryMassAux 0 t a b) s

The depth-zero residual mass is continuous in its level away from its two affine boundary values.

theorem MathlibNt.SieveTheory.LinearSieve.continuousAt_upperRosserBoundaryMassAux_zero_level_lower {s a b : ℝ} (hs0 : s ≠ 0) (hs3 : s ≠ 3 * a) : ContinuousAt (fun (p : ℝ × ℝ) => upperRosserBoundaryMassAux 0 p.1 p.2 b) (s, a)

The depth-zero residual mass is jointly continuous in its level and lower cutoff away from the two affine jump hypersurfaces. The inherited upper cutoff does not occur at depth zero.

theorem MathlibNt.SieveTheory.LinearSieve.continuousAt_upperRosserBoundaryMassAux_zero_affine_level_lower {s a x₀ x₁ b : ℝ} (hzero : s - x₀ - x₁ ≠ 0) (hterminal : s - x₀ - x₁ ≠ 3 * a) : ContinuousAt (fun (p : ℝ × ℝ) => upperRosserBoundaryMassAux 0 (p.1 - x₀ - x₁) p.2 b) (s, a)

Affine specialization of the joint depth-zero continuity statement used in the inner dominated-convergence step of the recursive Rosser mass.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryMassAux_zero_residual_le_left_add_boundary {s x₀ a l r x : ℝ} (hlx : l ≤ x) (hxr : x ≤ r) : upperRosserBoundaryMassAux 0 (s - x₀ - x) a x ≤ upperRosserBoundaryMassAux 0 (s - x₀ - l) a l + if s - x₀ - 3 * a ∈ Set.Icc l r then 1 else 0

On a cell in the peeled coordinate, the depth-zero residual is bounded by its left-endpoint value except on the unique cell meeting the affine boundary x = s - x₀ - 3a. The other depth-zero jump is downward in this orientation and therefore costs nothing in an upper majorant.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryMassAux_zero_ne_zero_outer_lower {s a x₀ x₁ : ℝ} (hs : 3 / 2 ≤ s) (hx₀ : x₀ ≤ s / 3) (hx₁ : x₁ < x₀) (h : upperRosserBoundaryMassAux 0 (s - x₀ - x₁) a x₁ ≠ 0) : 1 / 6 < a

A nonzero depth-zero residual below a peeled Rosser pair retains the depth-two lower support for the outer coordinate. This remains valid for the continuous majorant, independently of whether the pair comes from an exact boundary chain.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryMassAux_succ (k : ℕ) (s a b : ℝ) : upperRosserBoundaryMassAux (k + 1) s a b = ∫ (x₀ : ℝ) in Set.Ioo a (min b (s / 3)), x₀⁻¹ * ∫ (x₁ : ℝ) in Set.Ioo a x₀, x₁⁻¹ * upperRosserBoundaryMassAux k (s - x₀ - x₁) a x₁

@[simp]

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryMass_zero (s a : ℝ) : upperRosserBoundaryMass 0 s a = if 0 ≤ s ∧ s < 3 * a then 1 else 0

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryMass_succ (k : ℕ) (s a : ℝ) : upperRosserBoundaryMass (k + 1) s a = ∫ (x₀ : ℝ) in Set.Ioo a (min 1 (s / 3)), x₀⁻¹ * ∫ (x₁ : ℝ) in Set.Ioo a x₀, x₁⁻¹ * upperRosserBoundaryMassAux k (s - x₀ - x₁) a x₁

theorem MathlibNt.SieveTheory.LinearSieve.stronglyMeasurable_upperRosserBoundaryMassAux (k : ℕ) : MeasureTheory.StronglyMeasurable fun (p : (ℝ × ℝ) × ℝ) => upperRosserBoundaryMassAux k p.1.1 p.1.2 p.2

The finite-depth Rosser boundary mass is jointly strongly measurable in its level, lower cutoff, and inherited upper cutoff.

theorem MathlibNt.SieveTheory.LinearSieve.stronglyMeasurable_integral_inv_mul_upperRosserBoundaryMassAux (k : ℕ) : MeasureTheory.StronglyMeasurable fun (r : (ℝ × ℝ) × ℝ) => ∫ (x : ℝ) in Set.Ioo r.1.2 r.2, x⁻¹ * upperRosserBoundaryMassAux k (r.1.1 - r.2 - x) r.1.2 x

The inner integral appearing in the Rosser pair recursion is strongly measurable jointly in the residual level, lower cutoff, and outer coordinate.

theorem MathlibNt.SieveTheory.LinearSieve.inv_mul_upperRosserBoundaryMassAux_zero_eq_indicator (s a x₀ x₁ : ℝ) : x₁⁻¹ * upperRosserBoundaryMassAux 0 (s - x₀ - x₁) a x₁ = (Set.Ioc (s - x₀ - 3 * a) (s - x₀)).indicator (fun (x : ℝ) => x⁻¹) x₁

At depth zero, the residual factor is exactly the indicator of the moving terminal shell in the peeled coordinate.

theorem MathlibNt.SieveTheory.LinearSieve.integrableOn_inv_mul_upperRosserBoundaryMassAux_zero {s a x₀ : ℝ} (ha : 0 < a) : MeasureTheory.IntegrableOn (fun (x₁ : ℝ) => x₁⁻¹ * upperRosserBoundaryMassAux 0 (s - x₀ - x₁) a x₁) (Set.Ioo a x₀) MeasureTheory.volume

The depth-zero inner integrand is integrable whenever the fixed lower endpoint is positive.

theorem MathlibNt.SieveTheory.LinearSieve.integral_upperRosserBoundaryMassAux_zero_eq_integral_inter {s a x₀ : ℝ} : ∫ (x₁ : ℝ) in Set.Ioo a x₀, x₁⁻¹ * upperRosserBoundaryMassAux 0 (s - x₀ - x₁) a x₁ = ∫ (x₁ : ℝ) in Set.Ioo a x₀ ∩ Set.Ioc (s - x₀ - 3 * a) (s - x₀), x₁⁻¹

Without any ordering assumptions, the depth-zero inner integral is the reciprocal integral over its exact moving shell.

theorem MathlibNt.SieveTheory.LinearSieve.integral_upperRosserBoundaryMassAux_zero_eq_integral_Ioo {s a x₀ : ℝ} (ha : 0 < a) (hx₀s : x₀ < s / 3) : ∫ (x₁ : ℝ) in Set.Ioo a x₀, x₁⁻¹ * upperRosserBoundaryMassAux 0 (s - x₀ - x₁) a x₁ = ∫ (x₁ : ℝ) in Set.Ioo (max a (s - x₀ - 3 * a)) x₀, x₁⁻¹

On the outer Rosser range, the upper edge of the terminal shell is automatic, leaving a reciprocal integral with one moving lower endpoint.

theorem MathlibNt.SieveTheory.LinearSieve.integral_upperRosserBoundaryMassAux_zero_eq_log {s a x₀ : ℝ} (ha : 0 < a) (hx₀s : x₀ < s / 3) : ∫ (x₁ : ℝ) in Set.Ioo a x₀, x₁⁻¹ * upperRosserBoundaryMassAux 0 (s - x₀ - x₁) a x₁ = if max a (s - x₀ - 3 * a) < x₀ then Real.log (x₀ / max a (s - x₀ - 3 * a)) else 0

Exact logarithmic evaluation of the depth-zero inner integral. The conditional records precisely whether the moving terminal shell is nonempty.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryMass_one_eq_integral_log {s a : ℝ} (ha : 0 < a) : upperRosserBoundaryMass 1 s a = ∫ (x₀ : ℝ) in Set.Ioo a (min 1 (s / 3)), x₀⁻¹ * if max a (s - x₀ - 3 * a) < x₀ then Real.log (x₀ / max a (s - x₀ - 3 * a)) else 0

The first positive boundary depth is therefore an explicit one-dimensional piecewise logarithmic integral.

noncomputable def MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryLogKernel (s a x₀ : ℝ) : ℝ

The conditional logarithm left after evaluating the inner depth-two boundary integral.

Equations

• MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryLogKernel s a x₀ = if max a (s - x₀ - 3 * a) < x₀ then Real.log (x₀ / max a (s - x₀ - 3 * a)) else 0

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryLogKernel_eq_piecewise {s a x₀ : ℝ} (hax₀ : a < x₀) : upperRosserBoundaryLogKernel s a x₀ = if (s - 3 * a) / 2 < x₀ then if s - 4 * a ≤ x₀ then Real.log (x₀ / a) else Real.log (x₀ / (s - x₀ - 3 * a)) else 0

On the ordered region a < x₀, the depth-two logarithmic kernel has only the two affine break loci 2x₀ = s - 3a and x₀ = s - 4a.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryLogKernel_eq_max_log_sub {s a x₀ : ℝ} (ha : 0 < a) (hax₀ : a ≤ x₀) : upperRosserBoundaryLogKernel s a x₀ = max 0 (Real.log x₀ - Real.log (max a (s - x₀ - 3 * a)))

On the positive ordered region, the apparent piecewise kernel is simply the positive part of one continuous logarithmic ratio. Thus its internal affine break loci create no jump discontinuities.

theorem MathlibNt.SieveTheory.LinearSieve.abs_log_sub_log_le_six_of_one_sixth_le {x y : ℝ} (hx : 1 / 6 ≤ x) (hy : 1 / 6 ≤ y) : |Real.log x - Real.log y| ≤ 6 * |x - y|

The logarithm is explicitly Lipschitz on the screened coordinate interval. This controls the oscillation of each smooth branch of the depth-two kernel.

theorem MathlibNt.SieveTheory.LinearSieve.abs_inv_sub_inv_le_thirty_six_of_one_sixth_le {x y : ℝ} (hx : 1 / 6 ≤ x) (hy : 1 / 6 ≤ y) : |x⁻¹ - y⁻¹| ≤ 36 * |x - y|

Reciprocal coordinates are explicitly Lipschitz on the screened interval.

theorem MathlibNt.SieveTheory.LinearSieve.abs_log_div_sub_log_div_le_six_of_one_sixth_le {x a y b : ℝ} (hx : 1 / 6 ≤ x) (ha : 1 / 6 ≤ a) (hy : 1 / 6 ≤ y) (hb : 1 / 6 ≤ b) : |Real.log (x / a) - Real.log (y / b)| ≤ 6 * (|x - y| + |a - b|)

Ratios of screened coordinates have an explicit logarithmic oscillation bound. This is the smooth-cell estimate for both branches of the depth-two kernel.

theorem MathlibNt.SieveTheory.LinearSieve.abs_upperRosserBoundaryLogKernel_sub_le {s a x₀ t b y₀ : ℝ} (ha : 1 / 6 ≤ a) (hax₀ : a ≤ x₀) (hb : 1 / 6 ≤ b) (hby₀ : b ≤ y₀) : |upperRosserBoundaryLogKernel s a x₀ - upperRosserBoundaryLogKernel t b y₀| ≤ 6 * (2 * |x₀ - y₀| + |s - t| + 4 * |a - b|)

The whole depth-two logarithmic kernel is uniformly Lipschitz on its screened ordered domain. In particular, the two affine branch loci in upperRosserBoundaryLogKernel_eq_piecewise require no exceptional strips.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryMass_one_eq_integral_logKernel {s a : ℝ} (ha : 0 < a) : upperRosserBoundaryMass 1 s a = ∫ (x₀ : ℝ) in Set.Ioo a (min 1 (s / 3)), x₀⁻¹ * upperRosserBoundaryLogKernel s a x₀

The depth-two boundary mass expressed using its named logarithmic kernel.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryMassAux_one_eq_integral_logKernel {s a b : ℝ} (ha : 0 < a) : upperRosserBoundaryMassAux 1 s a b = ∫ (x₀ : ℝ) in Set.Ioo a (min b (s / 3)), x₀⁻¹ * upperRosserBoundaryLogKernel s a x₀

The first positive residual boundary depth has the same logarithmic-kernel description with an arbitrary inherited upper face.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryLogKernel_nonneg {s a x₀ : ℝ} (ha : 0 < a) : 0 ≤ upperRosserBoundaryLogKernel s a x₀

The conditional logarithmic kernel is nonnegative above a positive lower cutoff.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryLogKernel_le_log_six {s a x₀ : ℝ} (ha : 1 / 6 ≤ a) (hx₀ : x₀ ≤ 1) : upperRosserBoundaryLogKernel s a x₀ ≤ Real.log 6

Uniform bound for the explicit conditional logarithmic kernel on the screened box 1 / 6 ≤ a, x₀ ≤ 1. It is independent of s, hence uniform in particular for 3 / 2 ≤ s ≤ 4.

theorem MathlibNt.SieveTheory.LinearSieve.measurable_upperRosserBoundaryLogKernel (s a : ℝ) : Measurable (upperRosserBoundaryLogKernel s a)

theorem MathlibNt.SieveTheory.LinearSieve.inv_mul_upperRosserBoundaryLogKernel_le {s a x₀ : ℝ} (ha : 1 / 6 ≤ a) (hax₀ : a ≤ x₀) (hx₀ : x₀ ≤ 1) : x₀⁻¹ * upperRosserBoundaryLogKernel s a x₀ ≤ 6 * Real.log 6

Including the reciprocal outer density costs at most a further factor 6 on the screened box.

theorem MathlibNt.SieveTheory.LinearSieve.abs_inv_mul_upperRosserBoundaryLogKernel_sub_le {s a x₀ t b y₀ : ℝ} (ha : 1 / 6 ≤ a) (hax₀ : a ≤ x₀) (hb : 1 / 6 ≤ b) (hby₀ : b ≤ y₀) (hy₀ : y₀ ≤ 1) : |x₀⁻¹ * upperRosserBoundaryLogKernel s a x₀ - y₀⁻¹ * upperRosserBoundaryLogKernel t b y₀| ≤ 36 * (2 * |x₀ - y₀| + |s - t| + 4 * |a - b|) + 36 * Real.log 6 * |x₀ - y₀|

The full depth-two integrand, including its reciprocal outer weight, has a uniform modulus of continuity on the screened ordered box.

theorem MathlibNt.SieveTheory.LinearSieve.integrableOn_inv_mul_upperRosserBoundaryLogKernel {s a b : ℝ} (ha : 1 / 6 ≤ a) (hb : b ≤ 1) : MeasureTheory.IntegrableOn (fun (x₀ : ℝ) => x₀⁻¹ * upperRosserBoundaryLogKernel s a x₀) (Set.Ioo a b) MeasureTheory.volume

theorem MathlibNt.SieveTheory.LinearSieve.abs_integral_inv_mul_upperRosserBoundaryLogKernel_sub_le {s t a b : ℝ} (ha : 1 / 6 ≤ a) (hab : a ≤ b) (hb : b ≤ 1) : |(∫ (x₀ : ℝ) in Set.Ioo a b, x₀⁻¹ * upperRosserBoundaryLogKernel s a x₀) - ∫ (x₀ : ℝ) in Set.Ioo a b, x₀⁻¹ * upperRosserBoundaryLogKernel t a x₀| ≤ 36 * |s - t| * (b - a)

On a fixed screened interval, changing the sieve parameter changes the depth-two integral by at most 36 |s - t| times the interval length.

theorem MathlibNt.SieveTheory.LinearSieve.integral_inv_mul_upperRosserBoundaryLogKernel_le_length {s a u v : ℝ} (ha : 1 / 6 ≤ a) (hau : a ≤ u) (huv : u ≤ v) (hv : v ≤ 1) : ∫ (x₀ : ℝ) in Set.Ioo u v, x₀⁻¹ * upperRosserBoundaryLogKernel s a x₀ ≤ (v - u) * (6 * Real.log 6)

On any screened interval, the depth-two integrand is bounded by its interval length times the uniform kernel bound.

theorem MathlibNt.SieveTheory.LinearSieve.integral_inv_mul_upperRosserBoundaryLogKernel_moving_strip_le {s a h : ℝ} (ha : 1 / 6 ≤ a) (hh : 0 ≤ h) : ∫ (x₀ : ℝ) in Set.Ioo (max a (s / 3 - h)) (min 1 (s / 3 + h)), x₀⁻¹ * upperRosserBoundaryLogKernel s a x₀ ≤ 12 * h * Real.log 6

The cells meeting the moving outer face x₀ = s / 3 contribute only O(h), uniformly in s. This is the remaining boundary-strip estimate in the depth-two Darboux comparison.

theorem MathlibNt.SieveTheory.LinearSieve.abs_upperRosserBoundaryMass_one_sub_le {s t a : ℝ} (ha : 1 / 6 ≤ a) : |upperRosserBoundaryMass 1 s a - upperRosserBoundaryMass 1 t a| ≤ (36 + 2 * Real.log 6) * |s - t|

The first positive-depth continuous boundary mass is uniformly Lipschitz in the sieve parameter on the screened outer range. The 36 term controls the kernel on the common support, while 2 log 6 is the moving-face strip cost.

theorem MathlibNt.SieveTheory.LinearSieve.abs_upperRosserBoundaryMass_one_sub_le_of_outer {s a b : ℝ} (ha : 1 / 6 ≤ a) (hb : 1 / 6 ≤ b) : |upperRosserBoundaryMass 1 s a - upperRosserBoundaryMass 1 s b| ≤ (144 + 6 * Real.log 6) * |a - b|

The first positive-depth boundary mass is also uniformly Lipschitz in its screened outer cutoff. This is the second coordinate estimate needed for the outer (q,p₀) Darboux mesh.

theorem MathlibNt.SieveTheory.LinearSieve.abs_upperRosserBoundaryMass_one_sub_le_joint {s t a b : ℝ} (ha : 1 / 6 ≤ a) (hb : 1 / 6 ≤ b) : |upperRosserBoundaryMass 1 s a - upperRosserBoundaryMass 1 t b| ≤ (36 + 2 * Real.log 6) * |s - t| + (144 + 6 * Real.log 6) * |a - b|

Joint modulus of continuity for the depth-two boundary mass in its sieve parameter and outer coordinate.

theorem MathlibNt.SieveTheory.LinearSieve.abs_inv_mul_inv_sub_le_four_hundred_thirty_two {a b : ℝ} (ha : 1 / 6 ≤ a) (hb : 1 / 6 ≤ b) : |a⁻¹ * a⁻¹ - b⁻¹ * b⁻¹| ≤ 432 * |a - b|

The square reciprocal outer density is uniformly Lipschitz on [1/6, ∞).

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryMass_one_le_five_mul_log_six {s a : ℝ} (ha : 1 / 6 ≤ a) : upperRosserBoundaryMass 1 s a ≤ 5 * Real.log 6

Uniform depth-two boundary-mass bound on the screened outer range. The factor 5 uses that the outer interval has length at most 1 - 1 / 6.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryMassAux_nonneg (k : ℕ) {s a b : ℝ} (ha : 0 ≤ a) : 0 ≤ upperRosserBoundaryMassAux k s a b

Every finite-depth continuous boundary mass is nonnegative once its terminal coordinate is nonnegative.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryMass_nonneg (k : ℕ) {s a : ℝ} (ha : 0 ≤ a) : 0 ≤ upperRosserBoundaryMass k s a