Prove2Me

Partial fractions, reflection symmetry, and residue cancellation for RnR_n

Proved
ZudilinZeta.zudilin_partial_fraction_data_exists

by tomasz · Oct 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

number-theorypartial-fractionszeta-values

For every admissible parameter system PP and every integer n>0n>0, the rational function RnR_n admits a partial-fraction datum as defined in ZudilinZetaPartialFractions:

∃(cs,k)∈QN×N,Rn(t)=∑s=1q−r∑k=hr+1h0−hr+1cs,k(t+k)s(t>−1).\exists (c_{s,k})\in\mathbb Q^{\mathbb N\times\mathbb N},\quad R_n(t)=\sum_{s=1}^{q-r}\sum_{k=h_{r+1}}^{h_0-h_{r+1}}\frac{c_{s,k}}{(t+k)^s}\qquad(t>-1).

The datum additionally satisfies

cs,h0−k=(−1)s+1cs,k(1≤s≤q−r, hr+1≤k≤h0−hr+1),∑k=hr+1h0−hr+1c1,k=0.c_{s,h_0-k}=(-1)^{s+1}c_{s,k}\quad(1\le s\le q-r,\ h_{r+1}\le k\le h_0-h_{r+1}), \qquad \sum_{k=h_{r+1}}^{h_0-h_{r+1}}c_{1,k}=0.

This is the finite algebraic input for expressing the derivative series as a linear form in odd zeta values. The function RnR_n and all parameter conditions are those of the 2001 note, including the factor h0+2th_0+2t.

Preamble
import Definitions.Def_ZudilinZetaPartialFractions
Formal statement
namespace ZudilinZeta

theorem zudilin_partial_fraction_data_exists (P : Params) (n : ℕ) (hn : 0 < n) :
    Nonempty (PartialFractionData P n) := by sorry

end ZudilinZeta
Source
W. Zudilin, One of the numbers ζ(5), ζ(7), ζ(9), ζ(11) is irrational, Russian Math. Surveys 56 (2001), pp. 774–775, definition of R_n and Lemma 1, https://www.math.ru.nl/~zudilin/PS/zeta5-11%24.pdf; W. Zudilin, Arithmetic of linear forms involving odd zeta values, https://arxiv.org/abs/math/0206176, Lemma 19 and its proof, pp. 31–33, equations (8.10)–(8.12).

View graph