Finite geometric difference identity for the Rhin-Viola J1 base integral

Proved

RhinViola.j1FiniteGeometricIdentity

by WillR · Oct 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

arithmetic-bridgefinite-sumgeometric-identityj1lemma-2rhin-viola

For natural a,nu, multiplying the finite sum of reflected powers (1-x)^(a+i), i=0,...,nu-1, by x gives (1-x)^a-(1-x)^(a+nu). This is the finite geometric identity that removes the apparent 1/x singularity in the J1 calculation of Rhin-Viola Lemma 2.

Preamble

import Mathlib.Tactic
open scoped BigOperators

Formal statement

theorem RhinViola.j1FiniteGeometricIdentity
    (a nu : ℕ) (x : ℝ) :
    x * Finset.sum (Finset.range nu) (fun i : ℕ => (1 - x) ^ (a + i)) =
      (1 - x) ^ a - (1 - x) ^ (a + nu) := by sorry

Source

Elementary geometric identity used implicitly in the proof of G. Rhin and C. Viola, On the irrationality measure of zeta(2), Lemma 2, p. 88.

View graph