LiSwaps.lean

Declarations

Source

/-
NguyenRH1/LiSwaps.lean — tier ii′ sub-stage ii′-2 (D-064 §4 R2):
the two elementary swaps.

**R2(i)** (`liCoeff_eq_sum_sigma`): the Keiper–Li coefficient as the binomial
sum of paired zero power sums,
  λ_n = Σ_{j=1}^n (−1)^{j+1} C(n,j) σ_j,
where σ_j := Σ′_ρ (mult(ρ)/2)((1/ρ)^j + (1/ρ̄)^j) — the pairing makes each
slice absolutely summable for j ≥ 1 (j = 1 via Re(1/ρ) = Re(ρ)/|ρ|² with
0 < Re ρ < 1; j ≥ 2 by |ρ|^{−j} ≤ |ρ|^{−2} for ‖ρ‖ ≥ 2; the finite ball
{‖ρ‖ < 2} by compactness/discreteness — the ii′-1a skeleton).

**R2(ii)** (`sInfty_eq_sum`): the archimedean term as the binomial sum of
Lagarias's a_j (D-037 §3, Lagarias (4.11)),
  S_∞(n) = Σ_{j=1}^n (−1)^j C(n,j) a_j,   n ≥ 1,
where a₁ = (log 4π + γ)/2 and a_j = Σ_{m odd ≥ 1} m^{−j} (encoded as
1 + the odd ≥ 3 tsum over SInfty's own subtype). The double-sum swap is
D-037 §3's absolute-convergence argument: each j ≥ 2 slice is dominated by
the convergent p-series Σ 1/m².

Together with ii′-1b's `ResW1_eq_sum` these set up the crux identity
S_∞ + 1 − λ_n = Res₁ (its (4.10) input is ii′-3).

Archive references: D-037 §3, D-064 (R2), journal-017.
-/
import Mathlib
import NguyenRH1.LiSkeleton

open Zeta23 Complex Filter Topology
open scoped Nat

noncomputable section

namespace NguyenRH1

/-! ## 0. Shared helpers -/

/-- Sum over Icc 1 n as a range sum (bespoke, via sum_bij). -/
lemma sum_Icc_one_eq_sum_range {M : Type*} [AddCommMonoid M] (n : ℕ) (f : ℕ → M) :
    ∑ j ∈ Finset.Icc 1 n, f j = ∑ k ∈ Finset.range n, f (k + 1) := by
  apply Finset.sum_bij (fun j _ => j - 1)
  · intro j hj
    rw [Finset.mem_Icc] at hj
    rw [Finset.mem_range]
    omega
  · intro a₁ ha₁ a₂ ha₂ h
    rw [Finset.mem_Icc] at ha₁ ha₂
    omega
  · intro k hk
    rw [Finset.mem_range] at hk
    exact ⟨k + 1, by rw [Finset.mem_Icc]; omega, by omega⟩
  · intro j hj
    rw [Finset.mem_Icc] at hj
    congr 1
    omega

/-- Sum over Icc 2 n as a range sum (bespoke, via sum_bij). -/
lemma sum_Icc_two_eq_sum_range {M : Type*} [AddCommMonoid M] (n : ℕ) (f : ℕ → M) :
    ∑ j ∈ Finset.Icc 2 n, f j = ∑ k ∈ Finset.range (n - 1), f (k + 2) := by
  apply Finset.sum_bij (fun j _ => j - 2)
  · intro j hj
    rw [Finset.mem_Icc] at hj
    rw [Finset.mem_range]
    omega
  · intro a₁ ha₁ a₂ ha₂ h
    rw [Finset.mem_Icc] at ha₁ ha₂
    omega
  · intro k hk
    rw [Finset.mem_range] at hk
    exact ⟨k + 2, by rw [Finset.mem_Icc]; omega, by omega⟩
  · intro j hj
    rw [Finset.mem_Icc] at hj
    congr 1
    omega

/-- Peel the j = 1 term off an Icc 1 n sum. -/
lemma sum_Icc_one_eq_add_sum_Icc_two {M : Type*} [AddCommMonoid M] (n : ℕ) (hn : 1 ≤ n)
    (f : ℕ → M) :
    ∑ j ∈ Finset.Icc 1 n, f j = f 1 + ∑ j ∈ Finset.Icc 2 n, f j := by
  rw [sum_Icc_one_eq_sum_range n f, sum_Icc_two_eq_sum_range n f]
  have hn' : n - 1 + 1 = n := Nat.sub_add_cancel hn
  have h := Finset.sum_range_succ' (fun k => f (k + 1)) (n - 1)
  rw [hn'] at h
  rw [h]
  have h2 : ∀ k : ℕ, f (k + 1 + 1) = f (k + 2) := fun k => by
    have e : k + 1 + 1 = k + 2 := rfl
    rw [e]
  rw [Finset.sum_congr rfl (fun k _ => h2 k)]
  exact add_comm _ _

/-- The binomial expansion of 1 − (1−x)ⁿ over any commutative ring:
1 − (1−x)ⁿ = Σ_{j=1}^n (−1)^{j+1} C(n,j) x^j. -/
lemma one_sub_one_sub_pow {R : Type*} [CommRing R] (n : ℕ) (x : R) :
    1 - (1 - x) ^ n = ∑ j ∈ Finset.Icc 1 n, (-1 : R) ^ (j + 1) * (n.choose j : R) * x ^ j := by
  have hexp : (1 - x) ^ n =
      1 + ∑ k ∈ Finset.range n, (-x) ^ (k + 1) * (n.choose (k + 1) : R) := by
    rw [show (1 : R) - x = -x + 1 from by ring, add_pow, Finset.sum_range_succ']
    simp only [pow_zero, one_pow, Nat.choose_zero_right, Nat.cast_one, mul_one, Nat.sub_zero]
    rw [add_comm]
  rw [hexp]
  have h : (1 : R) - (1 + ∑ k ∈ Finset.range n, (-x) ^ (k + 1) * (n.choose (k + 1) : R)) =
      -(∑ k ∈ Finset.range n, (-x) ^ (k + 1) * (n.choose (k + 1) : R)) := by ring
  rw [h, ← Finset.sum_neg_distrib, sum_Icc_one_eq_sum_range]
  apply Finset.sum_congr rfl
  intro k hk
  have e1 : (-x) ^ (k + 1) = (-1 : R) ^ (k + 1) * x ^ (k + 1) := neg_pow x (k + 1)
  have e2 : (-1 : R) ^ ((k + 1) + 1) = -((-1 : R) ^ (k + 1)) := by
    rw [pow_succ]
    ring
  rw [e1, e2]
  ring

/-! ## 1. R2(i): λ_n as the binomial sum of paired zero power sums -/

/-- The j-th paired power-sum slice over the zeros:
(mult/2)·((1/ρ)^j + (1/ρ̄)^j). -/
def sigmaSlice (j : ℕ) (ρ : {ρ : ℂ // IsNontrivialZero ρ}) : ℂ :=
  (zeroMult ρ : ℂ) / 2 * ((1 / (ρ : ℂ)) ^ j + (1 / ((starRingEnd ℂ) (ρ : ℂ))) ^ j)

/-- σ_j: the paired power sum over the nontrivial zeros
(`sigmaSlice_summable` for j ≥ 1). -/
def sigmaP (j : ℕ) : ℂ := ∑' ρ : {ρ : ℂ // IsNontrivialZero ρ}, sigmaSlice j ρ

/-- The slice bound: for 2 ≤ ‖ρ‖, ‖sigmaSlice j ρ‖ ≤ mult·(1/‖ρ‖²)
(j = 1 via the paired exactness Re(1/ρ) = Re(ρ)/|ρ|²; j ≥ 2 by
|ρ|^{−j} ≤ |ρ|^{−2}), then ≤ (9/4)·mult/(1+‖γ_ρ‖²) by ii′-1a's comparison. -/
lemma sigmaSlice_norm_le {j : ℕ} (hj : 1 ≤ j) (ρ : {ρ : ℂ // IsNontrivialZero ρ})
    (hρ : (2 : ℝ) ≤ ‖(ρ : ℂ)‖) :
    ‖sigmaSlice j ρ‖ ≤
      (9 / 4) * (zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf (ρ : ℂ))) := by
  have hz := ρ.2
  have hre0 : 0 ≤ (ρ : ℂ).re := hz.2.1.le
  have hre1 : (ρ : ℂ).re ≤ 1 := hz.2.2.le
  have hcomp : 1 + Complex.normSq (gammaOf (ρ : ℂ)) ≤ 9 / 4 * ‖(ρ : ℂ)‖ ^ 2 :=
    normSq_gammaOf_le_mul_norm_sq (n := 1) le_rfl hre0 hre1 (by simpa using hρ)
  have hz0 : (0 : ℝ) < ‖(ρ : ℂ)‖ := lt_of_lt_of_le (by norm_num) hρ
  have hz0' : ‖(ρ : ℂ)‖ ≠ 0 := ne_of_gt hz0
  have hρ0 : (ρ : ℂ) ≠ 0 := norm_pos_iff.mp hz0
  have hg0 : (0 : ℝ) < 1 + Complex.normSq (gammaOf (ρ : ℂ)) := by
    have h := Complex.normSq_nonneg (gammaOf (ρ : ℂ))
    linarith
  have hcore : ‖sigmaSlice j ρ‖ ≤ (zeroMult ρ : ℝ) / ‖(ρ : ℂ)‖ ^ 2 := by
    by_cases hj1 : j = 1
    · subst hj1
      have heq : sigmaSlice 1 ρ = (zeroMult ρ : ℂ) * (((1 / (ρ : ℂ)).re) : ℂ) := by
        rw [sigmaSlice]
        have hconj : (1 / ((starRingEnd ℂ) (ρ : ℂ))) = (starRingEnd ℂ) (1 / (ρ : ℂ)) := by
          rw [map_div₀, map_one]
        rw [hconj, pow_one, pow_one]
        have hac : ∀ z : ℂ, z + (starRingEnd ℂ) z = ((2 * z.re : ℝ) : ℂ) :=
          fun z => Complex.add_conj z
        rw [hac]
        push_cast
        ring
      rw [heq, norm_mul, RCLike.norm_natCast, Complex.norm_real, Real.norm_eq_abs]
      have hre : ((1 / (ρ : ℂ)).re) = (ρ : ℂ).re / Complex.normSq (ρ : ℂ) := by
        rw [one_div, Complex.inv_re]
      rw [hre]
      have hnn : (0 : ℝ) < Complex.normSq (ρ : ℂ) := Complex.normSq_pos.mpr hρ0
      have habs : |(ρ : ℂ).re / Complex.normSq (ρ : ℂ)| ≤ 1 / Complex.normSq (ρ : ℂ) := by
        rw [abs_div, abs_of_nonneg (Complex.normSq_nonneg _)]
        have hre1' : |(ρ : ℂ).re| ≤ 1 := abs_le.mpr ⟨by linarith, hre1⟩
        exact (div_le_div_iff_of_pos_right hnn).mpr hre1'
      calc (zeroMult ρ : ℝ) * |(ρ : ℂ).re / Complex.normSq (ρ : ℂ)|
          ≤ (zeroMult ρ : ℝ) * (1 / Complex.normSq (ρ : ℂ)) :=
            mul_le_mul_of_nonneg_left habs (Nat.cast_nonneg _)
        _ = (zeroMult ρ : ℝ) / ‖(ρ : ℂ)‖ ^ 2 := by
            rw [Complex.normSq_eq_norm_sq]
            ring
    · have hj2 : 2 ≤ j := by omega
      have hnormρ : ‖(1 / (ρ : ℂ)) ^ j‖ = 1 / ‖(ρ : ℂ)‖ ^ j := by
        rw [norm_pow, norm_div, norm_one, div_pow, one_pow]
      have hnormρ' : ‖(1 / ((starRingEnd ℂ) (ρ : ℂ))) ^ j‖ = 1 / ‖(ρ : ℂ)‖ ^ j := by
        rw [norm_pow, starRingEnd_apply, norm_div, norm_one, norm_star, div_pow, one_pow]
      have hcast : ‖((zeroMult ρ : ℂ) / 2)‖ = (zeroMult ρ : ℝ) / 2 := by
        rw [norm_div, RCLike.norm_natCast]
        norm_num
      have h1 : ‖sigmaSlice j ρ‖ ≤
          (zeroMult ρ : ℝ) / 2 * (1 / ‖(ρ : ℂ)‖ ^ j + 1 / ‖(ρ : ℂ)‖ ^ j) := by
        rw [sigmaSlice, norm_mul, hcast]
        apply mul_le_mul_of_nonneg_left _ (by positivity : (0 : ℝ) ≤ (zeroMult ρ : ℝ) / 2)
        refine (norm_add_le _ _).trans ?_
        rw [hnormρ, hnormρ']
      have h2 : (zeroMult ρ : ℝ) / 2 * (1 / ‖(ρ : ℂ)‖ ^ j + 1 / ‖(ρ : ℂ)‖ ^ j) =
          (zeroMult ρ : ℝ) / ‖(ρ : ℂ)‖ ^ j := by ring
      have h3 : (zeroMult ρ : ℝ) / ‖(ρ : ℂ)‖ ^ j ≤ (zeroMult ρ : ℝ) / ‖(ρ : ℂ)‖ ^ 2 := by
        have hpow : ‖(ρ : ℂ)‖ ^ 2 ≤ ‖(ρ : ℂ)‖ ^ j :=
          pow_le_pow_right₀ (by linarith : (1 : ℝ) ≤ ‖(ρ : ℂ)‖) hj2
        have h4 : 1 / ‖(ρ : ℂ)‖ ^ j ≤ 1 / ‖(ρ : ℂ)‖ ^ 2 :=
          one_div_le_one_div_of_le (pow_pos hz0 2) hpow
        calc (zeroMult ρ : ℝ) / ‖(ρ : ℂ)‖ ^ j = (zeroMult ρ : ℝ) * (1 / ‖(ρ : ℂ)‖ ^ j) := by
              ring
          _ ≤ (zeroMult ρ : ℝ) * (1 / ‖(ρ : ℂ)‖ ^ 2) :=
            mul_le_mul_of_nonneg_left h4 (Nat.cast_nonneg _)
          _ = (zeroMult ρ : ℝ) / ‖(ρ : ℂ)‖ ^ 2 := by ring
      rw [h2] at h1
      exact h1.trans h3
  have key : (zeroMult ρ : ℝ) / ‖(ρ : ℂ)‖ ^ 2 ≤
      (9 / 4) * (zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf (ρ : ℂ))) := by
    rw [le_div_iff₀ hg0]
    have hbound : (zeroMult ρ : ℝ) / ‖(ρ : ℂ)‖ ^ 2 *
          (1 + Complex.normSq (gammaOf (ρ : ℂ)))
        ≤ (zeroMult ρ : ℝ) / ‖(ρ : ℂ)‖ ^ 2 * ((9 / 4) * ‖(ρ : ℂ)‖ ^ 2) :=
      mul_le_mul_of_nonneg_left hcomp (by positivity)
    have heq : (zeroMult ρ : ℝ) / ‖(ρ : ℂ)‖ ^ 2 * ((9 / 4) * ‖(ρ : ℂ)‖ ^ 2) =
        (9 / 4) * (zeroMult ρ : ℝ) := by
      field_simp
    exact hbound.trans (le_of_eq heq)
  exact hcore.trans key

/-- Each power-sum slice is absolutely summable over the zeros (j ≥ 1).
Same skeleton as `liSummable` (ii′-1a), with the fixed radius 2. -/
theorem sigmaSlice_summable (j : ℕ) (hj : 1 ≤ j) : Summable (sigmaSlice j) := by
  have hbase : Summable (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>
      (9 / 4) * ((zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf ρ)))) :=
    (WeilEF.zero_sum_inv_sq zetaSeam).mul_left (9 / 4)
  set D : {ρ : ℂ // IsNontrivialZero ρ} → ℝ := fun ρ =>
    if (2 : ℝ) ≤ ‖(ρ : ℂ)‖ then
      (9 / 4) * (zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf ρ))
    else ‖sigmaSlice j ρ‖ with hDdef
  have hfin : {ρ : {ρ // IsNontrivialZero ρ} | ¬ ((2 : ℝ) ≤ ‖(ρ : ℂ)‖)}.Finite := by
    have hcomp : IsCompact (Metric.closedBall (0 : ℂ) 2) := isCompact_closedBall _ _
    have hzeros : (Metric.closedBall (0 : ℂ) 2) ∩ {ρ : ℂ | IsNontrivialZero ρ}
        ⊆ (Metric.closedBall (0 : ℂ) 2) ∩ riemannZetaZeros := by
      intro z hz
      exact ⟨hz.1, hz.2.1⟩
    have hfin2 := (hcomp.inter_riemannZetaZeros_finite).subset hzeros
    have himg : (Subtype.val '' {ρ : {ρ // IsNontrivialZero ρ} |
        ¬ ((2 : ℝ) ≤ ‖(ρ : ℂ)‖)}).Finite := by
      apply hfin2.subset
      rintro z ⟨ρ, hρ, rfl⟩
      refine ⟨?_, ρ.2⟩
      simp only [Metric.mem_closedBall, dist_zero_right]
      exact le_of_lt (lt_of_not_ge hρ)
    exact Set.Finite.of_finite_image himg (Subtype.val_injective.injOn)
  have hE : Summable (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>
      D ρ - (9 / 4) * ((zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf ρ)))) := by
    apply summable_of_hasFiniteSupport
    apply hfin.subset
    intro ρ hρ
    simp only [Function.mem_support, ne_eq] at hρ
    by_contra hball
    apply hρ
    have hball' : (2 : ℝ) ≤ ‖(ρ : ℂ)‖ := not_not.mp hball
    simp only [D, if_pos hball']
    ring
  have hD : Summable D := by
    have hsum := hbase.add hE
    have heq : (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>
        (9 / 4) * ((zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf ρ))) +
          (D ρ - (9 / 4) * ((zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf ρ))))) = D := by
      funext ρ
      ring
    rw [heq] at hsum
    exact hsum
  refine Summable.of_norm_bounded hD (fun ρ => ?_)
  by_cases hρ : (2 : ℝ) ≤ ‖(ρ : ℂ)‖
  · simp only [D, if_pos hρ]
    exact sigmaSlice_norm_le hj ρ hρ
  · simp only [D, if_neg hρ, le_refl]

/-- The Li summand as a finite sum of power-sum slices (binomial theorem). -/
lemma liSummand_eq_sum_slices (n : ℕ) (ρ : {ρ : ℂ // IsNontrivialZero ρ}) :
    liSummand n ρ =
      ∑ j ∈ Finset.Icc 1 n, (-1 : ℂ) ^ (j + 1) * (n.choose j : ℂ) * sigmaSlice j ρ := by
  rw [liSummand, one_sub_one_sub_pow n (1 / (ρ : ℂ)),
    one_sub_one_sub_pow n (1 / ((starRingEnd ℂ) (ρ : ℂ)))]
  rw [mul_add, Finset.mul_sum, Finset.mul_sum, ← Finset.sum_add_distrib]
  apply Finset.sum_congr rfl
  intro j hj
  rw [sigmaSlice]
  ring

/-- **R2(i)**: the Keiper–Li coefficient as the binomial sum of the paired
zero power sums: λ_n = Σ_{j=1}^n (−1)^{j+1} C(n,j) σ_j. -/
theorem liCoeff_eq_sum_sigma (n : ℕ) :
    liCoeff n = ∑ j ∈ Finset.Icc 1 n, (-1 : ℂ) ^ (j + 1) * (n.choose j : ℂ) * sigmaP j := by
  unfold liCoeff sigmaP
  rw [tsum_congr (fun ρ => liSummand_eq_sum_slices n ρ)]
  rw [Summable.tsum_finsetSum (fun j hj => ?_)]
  · apply Finset.sum_congr rfl
    intro j hj
    rw [tsum_mul_left]
  · rw [Finset.mem_Icc] at hj
    exact (sigmaSlice_summable j hj.1).mul_left _

/-! ## 2. R2(ii): S_∞ as the binomial sum of Lagarias's a_j -/

/-- Lagarias's a_j (D-037 §3): a₁ = (log 4π + γ)/2; for j ≥ 2,
a_j = Σ_{m odd ≥ 1} m^{−j}, encoded as 1 (the m = 1 term) plus the odd ≥ 3
tail over SInfty's own subtype. The identification with (1−2^{−j})ζ(j) is
ii′-3 territory. -/
def lagariasA (j : ℕ) : ℝ :=
  if j = 1 then lagariasA1
  else 1 + ∑' m : {m : ℕ // Odd m ∧ 3 ≤ m}, (1 / (m : ℝ)) ^ j

/-- The j ≥ 2 odd-m slices are summable (dominated by the p-series Σ 1/m²,
restriction of `summable_one_div_nat_pow` to the odd ≥ 3 subtype). -/
lemma oddSlice_summable (j : ℕ) (hj : 2 ≤ j) :
    Summable (fun m : {m : ℕ // Odd m ∧ 3 ≤ m} => (1 / (m : ℝ)) ^ j) := by
  have hconv : (fun m : {m : ℕ // Odd m ∧ 3 ≤ m} => (1 / (m : ℝ)) ^ j) =
      (fun m : {m : ℕ // Odd m ∧ 3 ≤ m} => 1 / (m : ℝ) ^ j) := by
    funext m
    rw [div_pow, one_pow]
  rw [hconv]
  have hbase : Summable (fun m : {m : ℕ // Odd m ∧ 3 ≤ m} => 1 / (m : ℝ) ^ 2) := by
    have h := Real.summable_one_div_nat_pow.mpr (show 1 < 2 from by norm_num)
    exact h.subtype (fun m => Odd m ∧ 3 ≤ m)
  apply Summable.of_nonneg_of_le (f := fun m : {m : ℕ // Odd m ∧ 3 ≤ m} => 1 / (m : ℝ) ^ 2)
    _ _ hbase
  · intro m
    positivity
  · intro m
    have hm3 : (3 : ℝ) ≤ (m : ℝ) := by exact_mod_cast m.2.2
    have hm1 : (1 : ℝ) ≤ (m : ℝ) := by linarith
    have hm0 : (0 : ℝ) < (m : ℝ) := by linarith
    have hpow : (m : ℝ) ^ 2 ≤ (m : ℝ) ^ j := pow_le_pow_right₀ hm1 hj
    exact one_div_le_one_div_of_le (pow_pos hm0 2) hpow

/-- The SInfty summand as the j ≥ 2 binomial tail (the j = 1 term cancels
n/m exactly; D-037 §3). -/
lemma sInfty_summand_eq (n : ℕ) (hn : 1 ≤ n) (m : {m : ℕ // Odd m ∧ 3 ≤ m}) :
    (1 - 1 / (m : ℝ)) ^ n - 1 + (n : ℝ) / (m : ℝ) =
      ∑ j ∈ Finset.Icc 2 n, (-1 : ℝ) ^ j * (n.choose j : ℝ) * (1 / (m : ℝ)) ^ j := by
  have h1 := one_sub_one_sub_pow (R := ℝ) n (1 / (m : ℝ))
  have h2 : (1 - 1 / (m : ℝ)) ^ n - 1 =
      ∑ j ∈ Finset.Icc 1 n, (-1 : ℝ) ^ j * (n.choose j : ℝ) * (1 / (m : ℝ)) ^ j := by
    have e : (1 - 1 / (m : ℝ)) ^ n - 1 = -(1 - (1 - 1 / (m : ℝ)) ^ n) := by ring
    rw [e, h1, ← Finset.sum_neg_distrib]
    apply Finset.sum_congr rfl
    intro j hj
    have e2 : (-1 : ℝ) ^ (j + 1) = -((-1 : ℝ) ^ j) := by
      rw [pow_succ]
      ring
    rw [e2]
    ring
  rw [h2, sum_Icc_one_eq_add_sum_Icc_two n hn
    (fun j => (-1 : ℝ) ^ j * (n.choose j : ℝ) * (1 / (m : ℝ)) ^ j)]
  have h3 : (-1 : ℝ) ^ 1 * (n.choose 1 : ℝ) * (1 / (m : ℝ)) ^ 1 =
      -(n : ℝ) / (m : ℝ) := by
    rw [pow_one, pow_one, Nat.choose_one_right]
    ring
  rw [h3]
  ring

/-- The alternating binomial identity: Σ_{j=2}^n (−1)^j C(n,j) = n − 1
(n ≥ 1). -/
lemma sum_Icc_two_neg_one_choose (n : ℕ) (hn : 1 ≤ n) :
    ∑ j ∈ Finset.Icc 2 n, (-1 : ℝ) ^ j * (n.choose j : ℝ) = (n : ℝ) - 1 := by
  have h0 : (0 : ℝ) = ∑ k ∈ Finset.range (n + 1), (-1 : ℝ) ^ k * (n.choose k : ℝ) := by
    have h := add_pow (-1 : ℝ) (1 : ℝ) n
    rw [neg_add_cancel, zero_pow (by omega : n ≠ 0)] at h
    have hconv : (∑ k ∈ Finset.range (n + 1), (-1 : ℝ) ^ k * 1 ^ (n - k) *
        (n.choose k : ℝ)) = ∑ k ∈ Finset.range (n + 1), (-1 : ℝ) ^ k * (n.choose k : ℝ) := by
      apply Finset.sum_congr rfl
      intro k hk
      simp
    rw [hconv] at h
    exact h
  rw [Finset.sum_range_succ'] at h0
  have hn' : n - 1 + 1 = n := Nat.sub_add_cancel hn
  have h1 := Finset.sum_range_succ' (fun k => (-1 : ℝ) ^ (k + 1) * (n.choose (k + 1) : ℝ))
    (n - 1)
  rw [hn'] at h1
  rw [h1] at h0
  simp only [pow_zero, Nat.choose_zero_right, Nat.cast_one, one_mul, Nat.zero_add, pow_one,
    Nat.choose_one_right, neg_one_mul] at h0
  rw [sum_Icc_two_eq_sum_range n (fun j => (-1 : ℝ) ^ j * (n.choose j : ℝ))]
  have h2 : ∀ k : ℕ, (-1 : ℝ) ^ (k + 1 + 1) * (n.choose (k + 1 + 1) : ℝ) =
      (-1 : ℝ) ^ (k + 2) * (n.choose (k + 2) : ℝ) := fun k => by
    have e : k + 1 + 1 = k + 2 := rfl
    rw [e]
  rw [Finset.sum_congr rfl (fun k _ => h2 k)] at h0
  linarith

/-- **R2(ii)**: the archimedean term as the binomial sum of Lagarias's a_j
(D-037 §3, Lagarias (4.11)): S_∞(n) = Σ_{j=1}^n (−1)^j C(n,j) a_j (n ≥ 1). -/
theorem sInfty_eq_sum (n : ℕ) (hn : 1 ≤ n) :
    SInfty n = ∑ j ∈ Finset.Icc 1 n, (-1 : ℝ) ^ j * (n.choose j : ℝ) * lagariasA j := by
  have hswap : (∑' m : {m : ℕ // Odd m ∧ 3 ≤ m},
        ((1 - 1 / (m : ℝ)) ^ n - 1 + (n : ℝ) / (m : ℝ))) =
      ∑ j ∈ Finset.Icc 2 n, (-1 : ℝ) ^ j * (n.choose j : ℝ) * (lagariasA j - 1) := by
    rw [tsum_congr (fun m => sInfty_summand_eq n hn m)]
    rw [Summable.tsum_finsetSum (fun j hj => ?_)]
    · apply Finset.sum_congr rfl
      intro j hj
      rw [Finset.mem_Icc] at hj
      have hj1 : j ≠ 1 := by omega
      rw [tsum_mul_left]
      congr 1
      rw [lagariasA, if_neg hj1]
      ring
    · rw [Finset.mem_Icc] at hj
      exact (oddSlice_summable j hj.1).mul_left _
  unfold SInfty
  rw [hswap]
  rw [sum_Icc_one_eq_add_sum_Icc_two n hn
    (fun j => (-1 : ℝ) ^ j * (n.choose j : ℝ) * lagariasA j)]
  have hsplit : ∑ j ∈ Finset.Icc 2 n, (-1 : ℝ) ^ j * (n.choose j : ℝ) * (lagariasA j - 1) =
      ∑ j ∈ Finset.Icc 2 n, (-1 : ℝ) ^ j * (n.choose j : ℝ) * lagariasA j -
        ∑ j ∈ Finset.Icc 2 n, (-1 : ℝ) ^ j * (n.choose j : ℝ) := by
    rw [← Finset.sum_sub_distrib]
    apply Finset.sum_congr rfl
    intro j hj
    ring
  rw [hsplit, sum_Icc_two_neg_one_choose n hn]
  have h1t : (-1 : ℝ) ^ 1 * (n.choose 1 : ℝ) * lagariasA 1 = -(n : ℝ) * lagariasA1 := by
    rw [lagariasA, if_pos rfl, pow_one, Nat.choose_one_right]
    ring
  rw [h1t]
  ring

end NguyenRH1