theorem MathlibNt.SieveTheory.LinearSieve.triangular_integral_swap (F : ℝ → ℝ → ℝ) (b u : ℝ) (hF : MeasureTheory.Integrable (Function.uncurry fun (a x : ℝ) => {p : ℝ × ℝ | p.1 ∈ Set.Ioo 0 b ∧ p.2 ∈ Set.Ioo p.1 u}.indicator (Function.uncurry F) (a, x)) (MeasureTheory.volume.prod MeasureTheory.volume)) : ∫ (a : ℝ) in Set.Ioo 0 b, ∫ (x : ℝ) in Set.Ioo a u, F a x = ∫ (x : ℝ) in Set.Ioo 0 u, ∫ (a : ℝ) in Set.Ioo 0 (min b x), F a x

Fubini reindexing on the open triangular region 0 < a < b, a < x < u. The explicit integrability premise is the exact hypothesis needed before the positive-depth upper Rosser source recursion can be rearranged.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryMassAux_homogeneous (k : ℕ) {c s a b : ℝ} (hc : 0 < c) : upperRosserBoundaryMassAux k (c * s) (c * a) (c * b) = upperRosserBoundaryMassAux k s a b

noncomputable def MathlibNt.SieveTheory.LinearSieve.upperRosserBoundarySourceIntegral (k : ℕ) (s b : ℝ) : ℝ

The packaged source integral with inherited upper face b.

Equations

• MathlibNt.SieveTheory.LinearSieve.upperRosserBoundarySourceIntegral k s b = ∫ (a : ℝ) in Set.Ioo 0 b, a⁻¹ * a⁻¹ * MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryMassAux k s a b

@[simp]

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundarySourceIntegral_one (k : ℕ) (s : ℝ) : upperRosserBoundarySourceIntegral k s 1 = ∫ (a : ℝ) in Set.Ioo 0 1, a⁻¹ * a⁻¹ * upperRosserBoundaryMass k s a

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundarySourceIntegral_homogeneous (k : ℕ) {c s b : ℝ} (hc : 0 < c) : upperRosserBoundarySourceIntegral k (c * s) (c * b) = c⁻¹ * upperRosserBoundarySourceIntegral k s b

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundarySourceIntegral_normalize (k : ℕ) {s b : ℝ} (hb : 0 < b) : upperRosserBoundarySourceIntegral k s b = b⁻¹ * upperRosserBoundarySourceIntegral k (s / b) 1

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundarySourceIntegral_eq_zero_of_upper_le_support (k : ℕ) {s b : ℝ} (hs : 0 ≤ s) (hb : b ≤ s / 3 ^ (k + 1)) : upperRosserBoundarySourceIntegral k s b = 0

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundarySourceIntegral_eq_integral_of_lower_le_support (k : ℕ) {s c b : ℝ} (hs : 0 ≤ s) (hc : 0 ≤ c) (hcs : c ≤ s / 3 ^ (k + 1)) : upperRosserBoundarySourceIntegral k s b = ∫ (a : ℝ) in Set.Ioo c b, a⁻¹ * a⁻¹ * upperRosserBoundaryMassAux k s a b

theorem MathlibNt.SieveTheory.LinearSieve.integrable_outer_triangle_upperRosserBoundaryMassAux (k : ℕ) {s b : ℝ} (hs : 3 / 2 ≤ s) (hb : b ≤ 1) : MeasureTheory.Integrable ({p : ℝ × ℝ | p.1 ∈ Set.Ioo 0 b ∧ p.2 ∈ Set.Ioo p.1 (min b (s / 3))}.indicator (Function.uncurry fun (a x₀ : ℝ) => a⁻¹ * a⁻¹ * (x₀⁻¹ * ∫ (x₁ : ℝ) in Set.Ioo a x₀, x₁⁻¹ * upperRosserBoundaryMassAux k (s - x₀ - x₁) a x₁))) (MeasureTheory.volume.prod MeasureTheory.volume)

The first positive-depth triangular Fubini kernel is genuinely integrable. The proof uses the exact recursive support cutoff to remove the singular face a = 0, then a uniform finite-depth bound on the remaining compact triangle.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundarySourceIntegral_succ_outer_swap (k : ℕ) {s b : ℝ} (hs : 3 / 2 ≤ s) (hb : b ≤ 1) : upperRosserBoundarySourceIntegral (k + 1) s b = ∫ (x₀ : ℝ) in Set.Ioo 0 (min b (s / 3)), ∫ (a : ℝ) in Set.Ioo 0 (min b x₀), a⁻¹ * a⁻¹ * (x₀⁻¹ * ∫ (x₁ : ℝ) in Set.Ioo a x₀, x₁⁻¹ * upperRosserBoundaryMassAux k (s - x₀ - x₁) a x₁)

The outer source integral after unfolding one Rosser pair, with the first triangular Fubini swap justified by the preceding strict integrability theorem.

theorem MathlibNt.SieveTheory.LinearSieve.integrable_inner_triangle_upperRosserBoundaryMassAux (k : ℕ) {s b x₀ : ℝ} (hs : 3 / 2 ≤ s) (hx₀s : x₀ ≤ s / 3) (hx₀one : x₀ ≤ 1) : MeasureTheory.Integrable ({p : ℝ × ℝ | p.1 ∈ Set.Ioo 0 (min b x₀) ∧ p.2 ∈ Set.Ioo p.1 x₀}.indicator (Function.uncurry fun (a x₁ : ℝ) => a⁻¹ * a⁻¹ * (x₁⁻¹ * upperRosserBoundaryMassAux k (s - x₀ - x₁) a x₁))) (MeasureTheory.volume.prod MeasureTheory.volume)

For every outer coordinate, the remaining (a,x₁) triangle is integrable. This is the strict integrability input for the second Fubini rearrangement.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundarySourceIntegral_succ_second_swap (k : ℕ) {s b : ℝ} (hs : 3 / 2 ≤ s) (hb : b ≤ 1) : upperRosserBoundarySourceIntegral (k + 1) s b = ∫ (x₀ : ℝ) in Set.Ioo 0 (min b (s / 3)), x₀⁻¹ * ∫ (x₁ : ℝ) in Set.Ioo 0 x₀, x₁⁻¹ * upperRosserBoundarySourceIntegral k (s - x₀ - x₁) x₁

After the second Fubini swap, the innermost a-integral is exactly the source package with inherited upper face x₁.

theorem MathlibNt.SieveTheory.LinearSieve.integral_inv_mul_upperRosserBoundarySourceIntegral_change_variables (k : ℕ) {A x₀ : ℝ} (hA : 0 < A) (hx₀ : 0 < x₀) : ∫ (x : ℝ) in Set.Ioo 0 x₀, x⁻¹ * upperRosserBoundarySourceIntegral k (A - x) x = A⁻¹ * ∫ (v : ℝ) in Set.Ioi (A / x₀), upperRosserBoundarySourceIntegral k (v - 1) 1

The first strict reciprocal substitution, after homogeneity normalizes the inherited upper face: v = A / x sends (0,x₀) to (A/x₀,∞).

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundarySourceIntegral_succ_first_change_variables (k : ℕ) {s b : ℝ} (hs : 3 / 2 ≤ s) (hb : b ≤ 1) : upperRosserBoundarySourceIntegral (k + 1) s b = ∫ (x₀ : ℝ) in Set.Ioo 0 (min b (s / 3)), x₀⁻¹ * ((s - x₀)⁻¹ * ∫ (v : ℝ) in Set.Ioi ((s - x₀) / x₀), upperRosserBoundarySourceIntegral k (v - 1) 1)

The successor source after the first strict variable replacement. The remaining inner integrand now has normalized upper face 1, ready for the first κ = 1 Suzuki recursion.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundarySourceIntegral_succ_second_change_variables (k : ℕ) {s : ℝ} (hs : 3 / 2 ≤ s) : upperRosserBoundarySourceIntegral (k + 1) s 1 = s⁻¹ * ∫ (t : ℝ) in Set.Ioi (s / min 1 (s / 3)), (t - 1)⁻¹ * ∫ (v : ℝ) in Set.Ioi (t - 1), upperRosserBoundarySourceIntegral k (v - 1) 1

The second strict reciprocal substitution x₀ = s / t. Together with the preceding v = (s - x₀) / x₁ substitution, this is exactly the two-step κ = 1 Suzuki kernel, before its support is truncated to finite intervals.

theorem MathlibNt.SieveTheory.LinearSieve.div_min_one_div_three_eq_recursionLower_odd (k : ℕ) {s : ℝ} (hs : 3 / 2 ≤ s) (hshi : s ≤ 4) : s / min 1 (s / 3) = SuzukiFiniteContinuousLayers.recursionLower 2 s (2 * (k + 1) + 1)

On the upper fundamental-lemma window, the reciprocal image of the cubic outer face is exactly the lower endpoint in the odd Suzuki recursion.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundarySourceIntegral_succ_two_suzuki_kernel_shape (k : ℕ) {s : ℝ} (hs : 3 / 2 ≤ s) (hshi : s ≤ 4) : upperRosserBoundarySourceIntegral (k + 1) s 1 = s⁻¹ * ∫ (t : ℝ) in Set.Ioi (SuzukiFiniteContinuousLayers.recursionLower 2 s (2 * (k + 1) + 1)), (t - 1)⁻¹ * ∫ (v : ℝ) in Set.Ioi (t - 1), upperRosserBoundarySourceIntegral k (v - 1) 1

The second reciprocal substitution with its lower endpoint written in the literal first suzukiLayer_succ_succ form. The only remaining difference from the twice-recursed Suzuki layer is replacement of the two improper tails by their finite support intervals and identification of the residual source.

theorem MathlibNt.SieveTheory.LinearSieve.suzukiLayer_one_two_odd_succ_two_step_kernel (k : ℕ) (s : ℝ) : SuzukiFiniteContinuousLayers.suzukiLayer 1 2 (2 * (k + 1) + 1) s = (s ^ 1)⁻¹ * ∫ (t : ℝ) in SuzukiFiniteContinuousLayers.recursionLower 2 s (2 * (k + 1) + 1)..2 + ↑(2 * (k + 1) + 1), ((t - 1) ^ 1)⁻¹ * ∫ (v : ℝ) in SuzukiFiniteContinuousLayers.recursionLower 2 (t - 1) (2 * k + 2)..2 + ↑(2 * k + 2), SuzukiFiniteContinuousLayers.suzukiLayer 1 2 (2 * k + 1) (v - 1)

Unfolding the target odd Suzuki layer twice gives the finite-interval kernel which the preceding source formula must match.

def MathlibNt.SieveTheory.LinearSieve.UpperRosserBoundarySourceSuccTailAlignment : Prop

Exact residual after both nonlinear substitutions. It contains only the two support truncations and the predecessor source/layer identification; all Jacobians, endpoints, and Suzuki recursion algebra have already been fixed.

Equations

• MathlibNt.SieveTheory.LinearSieve.UpperRosserBoundarySourceSuccTailAlignment = ∀ (k : ℕ) (s : ℝ), 3 / 2 ≤ s → s ≤ 4 → ∫ (t : ℝ) in Set.Ioi (MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.recursionLower 2 s (2 * (k + 1) + 1)), (t - 1)⁻¹ * ∫ (v : ℝ) in Set.Ioi (t - 1), MathlibNt.SieveTheory.LinearSieve.upperRosserBoundarySourceIntegral k (v - 1) 1 = ∫ (t : ℝ) in MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.recursionLower 2 s (2 * (k + 1) + 1)..2 + ↑(2 * (k + 1) + 1), ((t - 1) ^ 1)⁻¹ * ∫ (v : ℝ) in MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.recursionLower 2 (t - 1) (2 * k + 2)..2 + ↑(2 * k + 2), MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLayer 1 2 (2 * k + 1) (v - 1)

theorem MathlibNt.SieveTheory.LinearSieve.suzukiUpperRosserBoundarySourceSuccLayerIdentity_of_tail_alignment (h : UpperRosserBoundarySourceSuccTailAlignment) : SuzukiUpperRosserBoundarySourceSuccLayerIdentity

The strongest exact assembler at the current boundary: the literal tail alignment above closes the requested successor-layer identity with no sieve or density hypothesis.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundarySourceSuccTailAlignment : UpperRosserBoundarySourceSuccTailAlignment

The tail alignment is unconditional. The predecessor identity used under both improper integrals is supplied by the global positive-source induction; the open lower endpoints are handled only almost everywhere.

theorem MathlibNt.SieveTheory.LinearSieve.suzukiUpperRosserBoundarySourceSuccLayerIdentity : SuzukiUpperRosserBoundarySourceSuccLayerIdentity

Unconditional successor-layer identity.