Suzuki Lemma 14.4: the actual discrete recurrence and (14.9)

This file works with the source-faithful natural-valued layers suzukiSourceV. The quotient in every recursive layer is therefore literally D ⌈/⌉ p.

noncomputable def MathlibNt.SieveTheory.suzukiActualT (S : BoundingSieve) : ℕ → ℕ → ℕ → ℝ

The actual finite parity aggregate: V_N + V_{N-2} + ..., stopping at V₁ or V₂. In particular depth zero is not inserted into a positive-depth Suzuki sum.

Equations

• MathlibNt.SieveTheory.suzukiActualT S 0 x✝¹ x✝ = 0
• MathlibNt.SieveTheory.suzukiActualT S 1 x✝¹ x✝ = MathlibNt.SieveTheory.suzukiSourceV S 1 x✝¹ x✝
• MathlibNt.SieveTheory.suzukiActualT S n.succ.succ x✝¹ x✝ = MathlibNt.SieveTheory.suzukiSourceV S (n + 2) x✝¹ x✝ + MathlibNt.SieveTheory.suzukiActualT S n x✝¹ x✝

@[simp]

theorem MathlibNt.SieveTheory.suzukiActualT_zero (S : BoundingSieve) (D z : ℕ) : suzukiActualT S 0 D z = 0

@[simp]

theorem MathlibNt.SieveTheory.suzukiActualT_one (S : BoundingSieve) (D z : ℕ) : suzukiActualT S 1 D z = suzukiSourceV S 1 D z

@[simp]

theorem MathlibNt.SieveTheory.suzukiActualT_add_two (S : BoundingSieve) (n D z : ℕ) : suzukiActualT S (n + 2) D z = suzukiSourceV S (n + 2) D z + suzukiActualT S n D z

def MathlibNt.SieveTheory.suzukiActualParityCarrier (N : ℕ) : Finset ℕ

The literal finite carrier 1 ≤ n ≤ N, n ≡ N (mod 2).

Equations

• MathlibNt.SieveTheory.suzukiActualParityCarrier N = {n ∈ Finset.range (N + 1) | 1 ≤ n ∧ n % 2 = N % 2}

theorem MathlibNt.SieveTheory.suzukiActualT_eq_parity_sum (S : BoundingSieve) (N D z : ℕ) : suzukiActualT S N D z = ∑ n ∈ suzukiActualParityCarrier N, suzukiSourceV S n D z

The recursive presentation above is exactly Suzuki's displayed finite parity sum, not an unbounded series or a depth scan.

theorem MathlibNt.SieveTheory.suzukiSourceV_eq_zero_of_pow_le_allDepth (S : BoundingSieve) (n D z : ℕ) (hzD : z ^ (n + 2) ≤ D) : suzukiSourceV S n D z = 0

The elementary support cutoff used to erase Suzuki's lower outer cutoff. It includes the natural boundary with ≤: strictness comes from p < z.

theorem MathlibNt.SieveTheory.suzukiSourceV_succ_eq_unrestricted (S : BoundingSieve) {n D z : ℕ} (hn : 0 < n) (hOddBoundary : Odd (n + 1) → z ^ 3 ≤ D) : suzukiSourceV S (n + 1) D z = ∑ p ∈ SwitchingPrinciple.suzukiSupportedBelow S z, S.nu p * suzukiSourceV S n (D ⌈/⌉ p) p

For a positive predecessor, the lower carrier may be erased by support vanishing. In odd outer depth the Case-I boundary z³ ≤ D also makes the source upper cutoff automatic.

theorem MathlibNt.SieveTheory.suzukiActualT_caseI_recurrence (S : BoundingSieve) {N D z : ℕ} (hN : 2 ≤ N) (hOddBoundary : Odd N → z ^ 3 ≤ D) : suzukiActualT S N D z = ∑ p ∈ SwitchingPrinciple.suzukiSupportedBelow S z, S.nu p * suzukiActualT S (N - 1) (D ⌈/⌉ p) p

Case I's exact discrete recurrence. The hypothesis is needed only in odd parity; for even N it is vacuous. The assumptions 2 ≤ N and the natural ceiling quotient are explicit.

noncomputable def MathlibNt.SieveTheory.suzukiSigmaZero (S : BoundingSieve) (N D z : ℕ) (a : ℝ) : ℝ

The three finite pieces in Suzuki (14.9). The support already contains p < z; a and b are respectively D^(1/σ) and D^(1/τ).

Equations

• MathlibNt.SieveTheory.suzukiSigmaZero S N D z a = ∑ p ∈ MathlibNt.SieveTheory.SwitchingPrinciple.suzukiSupportedBelow S z with ↑p < a, S.nu p * MathlibNt.SieveTheory.suzukiActualT S (N - 1) (D ⌈/⌉ p) p

noncomputable def MathlibNt.SieveTheory.suzukiSigmaOne (S : BoundingSieve) (N D z : ℕ) (a b : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.suzukiSigmaOne S N D z a b = ∑ p ∈ MathlibNt.SieveTheory.SwitchingPrinciple.suzukiSupportedBelow S z with a ≤ ↑p ∧ ↑p < b, S.nu p * MathlibNt.SieveTheory.suzukiActualT S (N - 1) (D ⌈/⌉ p) p

noncomputable def MathlibNt.SieveTheory.suzukiSigmaTwo (S : BoundingSieve) (N D z : ℕ) (b : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.suzukiSigmaTwo S N D z b = ∑ p ∈ MathlibNt.SieveTheory.SwitchingPrinciple.suzukiSupportedBelow S z with b ≤ ↑p, S.nu p * MathlibNt.SieveTheory.suzukiActualT S (N - 1) (D ⌈/⌉ p) p

theorem MathlibNt.SieveTheory.suzuki_equation14_9 (S : BoundingSieve) {N D z : ℕ} (hN : 2 ≤ N) (hOddBoundary : Odd N → z ^ 3 ≤ D) {a b : ℝ} (hab : a ≤ b) : suzukiActualT S N D z = suzukiSigmaZero S N D z a + suzukiSigmaOne S N D z a b + suzukiSigmaTwo S N D z b

Equation (14.9), before substituting the two real-power endpoints. This is an equality of finite sums, including all boundary choices (<, ≤) exactly.