theorem MathlibNt.SieveTheory.LinearSieve.finiteAbelSum_range {𝕜 : Type u_1} [CommRing 𝕜] {R H : ℕ → 𝕜} (n : ℕ) : ∑ i ∈ Finset.range n, (R i - R (i + 1)) * H i = R 0 * H 0 - R n * H n + ∑ i ∈ Finset.range n, R (i + 1) * (H (i + 1) - H i)

Finite Abel summation on an initial segment.

theorem MathlibNt.SieveTheory.LinearSieve.finiteAbelSum_Ico {𝕜 : Type u_1} [CommRing 𝕜] {a R H : ℕ → 𝕜} {w z : ℕ} (hwz : w ≤ z) (hdiff : ∀ n ∈ Finset.Ico w z, a n = R n - R (n + 1)) : ∑ n ∈ Finset.Ico w z, a n * H n = R w * H w - R z * H z + ∑ n ∈ Finset.Ico w z, R (n + 1) * (H (n + 1) - H n)

Exact finite Abel identity on the natural interval [w,z). The term R (x+1) is the right-endpoint value in the discrete Stieltjes increment.

theorem MathlibNt.SieveTheory.LinearSieve.suzukiLemma85_finiteAbel {𝕜 : Type u_1} [CommRing 𝕜] {a R H : ℕ → 𝕜} {w z : ℕ} (hwz : w ≤ z) (hRz : R z = 1) (hdiff : ∀ n ∈ Finset.Ico w z, a n = R n - R (n + 1)) : ∑ n ∈ Finset.Ico w z, a n * H n = -H z + R w * H w + ∑ n ∈ Finset.Ico w z, R (n + 1) * (H (n + 1) - H n)

Suzuki Lemma 8.5's exact finite Abel identity, before replacing R by its main term plus error. R z = 1 corresponds to the empty tail at the upper endpoint.

theorem MathlibNt.SieveTheory.LinearSieve.suzukiLemma85_finiteAbel_tail {𝕜 : Type u_1} [CommRing 𝕜] (a H : ℕ → 𝕜) {w z : ℕ} (hwz : w ≤ z) : ∑ n ∈ Finset.Ico w z, a n * H n = -H z + (1 + ∑ p ∈ Finset.Ico w z, a p) * H w + ∑ n ∈ Finset.Ico w z, (1 + ∑ p ∈ Finset.Ico (n + 1) z, a p) * (H (n + 1) - H n)

Fully explicit tail-sum form. A prime sum is obtained by taking a n = 0 off primes. No positivity, monotonicity, continuity, or primality hypothesis is used by this exact finite identity.

def MathlibNt.SieveTheory.LinearSieve.finiteNodeAtomSum {α : Type u_1} {A : Type u_2} [CommRing A] (R g : α → A) : List α → A

Sum (R x - R y) * g x over consecutive nodes x,y of a finite list.

Equations

• MathlibNt.SieveTheory.LinearSieve.finiteNodeAtomSum R g (x_1 :: y :: xs) = (R x_1 - R y) * g x_1 + MathlibNt.SieveTheory.LinearSieve.finiteNodeAtomSum R g (y :: xs)
• MathlibNt.SieveTheory.LinearSieve.finiteNodeAtomSum R g x✝ = 0

def MathlibNt.SieveTheory.LinearSieve.finiteNodeVariationSum {α : Type u_1} {A : Type u_2} [CommRing A] (R g : α → A) : List α → A

Sum R y * (g y - g x) over consecutive nodes x,y of a finite list.

Equations

• MathlibNt.SieveTheory.LinearSieve.finiteNodeVariationSum R g (x_1 :: y :: xs) = R y * (g y - g x_1) + MathlibNt.SieveTheory.LinearSieve.finiteNodeVariationSum R g (y :: xs)
• MathlibNt.SieveTheory.LinearSieve.finiteNodeVariationSum R g x✝ = 0

theorem MathlibNt.SieveTheory.LinearSieve.finiteNodeAbel {α : Type u_1} {A : Type u_2} [CommRing A] (R g : α → A) (w z : α) (interior : List α) : finiteNodeAtomSum R g (w :: interior ++ [z]) = R w * g w - R z * g z + finiteNodeVariationSum R g (w :: interior ++ [z])

Exact finite-node Abel identity. It is intentionally stated for the list w :: interior ++ [z], so the two boundary values remain exactly g w and g z, even when w,z : ℝ are not integers.

Exact main-ratio/error decomposition

The next statements are purely finite algebra. In particular they use no monotonicity, continuity, differentiability, or ordering hypothesis on the nodes. The sign convention makes finiteNodeStieltjesSum F g the left-node sum for -∫ g dF: its increment is F x - F y on an adjacent pair x,y.

def MathlibNt.SieveTheory.LinearSieve.finiteNodeStieltjesSum {α : Type u_1} {A : Type u_2} [CommRing A] (F g : α → A) : List α → A

Left-node finite Stieltjes sum with increments F x - F y.

Equations

• MathlibNt.SieveTheory.LinearSieve.finiteNodeStieltjesSum F g (x_1 :: y :: xs) = g x_1 * (F x_1 - F y) + MathlibNt.SieveTheory.LinearSieve.finiteNodeStieltjesSum F g (y :: xs)
• MathlibNt.SieveTheory.LinearSieve.finiteNodeStieltjesSum F g x✝ = 0

theorem MathlibNt.SieveTheory.LinearSieve.finiteNodeStieltjesSum_eq_atomSum {α : Type u_1} {A : Type u_2} [CommRing A] (F g : α → A) (nodes : List α) : finiteNodeStieltjesSum F g nodes = finiteNodeAtomSum F g nodes

The atom sum is exactly the finite Stieltjes sum, up to the harmless commutation of the two factors in each summand.

theorem MathlibNt.SieveTheory.LinearSieve.finiteNodeVariationSum_add {α : Type u_1} {A : Type u_2} [CommRing A] (F E g : α → A) (nodes : List α) : finiteNodeVariationSum (fun (x : α) => F x + E x) g nodes = finiteNodeVariationSum F g nodes + finiteNodeVariationSum E g nodes

Variation is additive in the coefficient function.

noncomputable def MathlibNt.SieveTheory.LinearSieve.finiteNodeLogRatio (z x : ℝ) : ℝ

The exact main ratio log z / log x, with no domain convention imposed.

Equations

• MathlibNt.SieveTheory.LinearSieve.finiteNodeLogRatio z x = Real.log z / Real.log x

noncomputable def MathlibNt.SieveTheory.LinearSieve.finiteNodeMainRatioSum (z : ℝ) (g : ℝ → ℝ) (nodes : List ℝ) : ℝ

The main finite Stieltjes sum. Explicitly, each adjacent pair x,y contributes g x * (log z / log x - log z / log y). This is the finite object to compare with the ordinary integral against log z / (x * (log x)^2) dx.

Equations

• MathlibNt.SieveTheory.LinearSieve.finiteNodeMainRatioSum z g nodes = MathlibNt.SieveTheory.LinearSieve.finiteNodeStieltjesSum (MathlibNt.SieveTheory.LinearSieve.finiteNodeLogRatio z) g nodes

theorem MathlibNt.SieveTheory.LinearSieve.finiteNodeMainRatio_boundary_variation (w u z : ℝ) (interior : List ℝ) (g : ℝ → ℝ) : finiteNodeLogRatio z w * g w - finiteNodeLogRatio z u * g u + finiteNodeVariationSum (finiteNodeLogRatio z) g (w :: interior ++ [u]) = finiteNodeMainRatioSum z g (w :: interior ++ [u])

Boundary plus variation of the main ratio telescopes exactly to its finite Stieltjes sum. This is unconditional finite algebra.

theorem MathlibNt.SieveTheory.LinearSieve.finiteNodeAbel_mainRatio_errorVariation (R E g : ℝ → ℝ) (w u z : ℝ) (interior : List ℝ) (hR : ∀ (x : ℝ), R x = finiteNodeLogRatio z x + E x) : finiteNodeAtomSum R g (w :: interior ++ [u]) = finiteNodeMainRatioSum z g (w :: interior ++ [u]) + (E w * g w - E u * g u + finiteNodeVariationSum E g (w :: interior ++ [u]))

Exact finite-node split for R(x) = log z / log x + E(x).

The main boundary and variation terms have been telescoped into the finite Stieltjes sum. Every error contribution is retained explicitly as two endpoint terms plus the finite variation of g; there are no analytic assumptions.

@[simp]

theorem MathlibNt.SieveTheory.LinearSieve.finiteNodeLogRatio_self {z : ℝ} (hz : Real.log z ≠ 0) : finiteNodeLogRatio z z = 1

At a nondegenerate upper endpoint the main ratio has the expected value one, so its upper boundary term is literally -g z.

theorem MathlibNt.SieveTheory.LinearSieve.finiteNodeVariationSum_le_telescope {α : Type u_1} (E g t : α → ℝ) (C : ℝ) (w z : α) (interior : List α) (hedge : List.Pairwise (fun (x y : α) => E y * (g y - g x) ≤ C * (t x - t y)) (w :: interior ++ [z])) : finiteNodeVariationSum E g (w :: interior ++ [z]) ≤ C * (t w - t z)

A finite adjacent-edge majorant telescopes. Pairwise control is stronger than needed, but matches the ordered Suzuki node list.

theorem MathlibNt.SieveTheory.LinearSieve.finiteNodeVariationSum_mono_of_pairwise {α : Type u_1} (E B g : α → ℝ) (nodes : List α) (h : List.Pairwise (fun (x y : α) => E y * (g y - g x) ≤ B y * (g y - g x)) nodes) : finiteNodeVariationSum E g nodes ≤ finiteNodeVariationSum B g nodes

theorem MathlibNt.SieveTheory.LinearSieve.finiteNodeVariationSum_smul_left {α : Type u_1} (C : ℝ) (B g : α → ℝ) (nodes : List α) : finiteNodeVariationSum (fun (x : α) => C * B x) g nodes = C * finiteNodeVariationSum B g nodes

theorem MathlibNt.SieveTheory.LinearSieve.finiteNodeAtomSum_le_telescope {α : Type u_1} (R g t : α → ℝ) (C : ℝ) (w z : α) (interior : List α) (h : List.Pairwise (fun (x y : α) => (R x - R y) * g x ≤ C * (t x - t y)) (w :: interior ++ [z])) : finiteNodeAtomSum R g (w :: interior ++ [z]) ≤ C * (t w - t z)