Special functions

The Lean Pool projects whose card's first MSC2020 code is in class 33, Special functions: 2 articles, one per card.

TheoremCarlson special functions and complex Dirichlet averages#

Formalizes Carlson special functions through complex Dirichlet averages, with simplex measures, Gamma-regularized analytic continuation, Euler inversion, Euler–Poisson equations, and quadratic transformations. Includes the complete supporting several-complex-variable and special-function libraries.

Quoted from the card LeanPool/projects/lean-codes.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 2 main results, each with its informal statement quoted from the card. The scan finds 2 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanPalomarSnapshot.r_first_quadratic · PalomarSnapshot.joint_average_continuation

TheoremPolylogarithms and sixteen log-trigonometric integral identities#

Formalizes the sixteen A-series identities from rainrzk's PolyLog Integrals tutorial, together with reusable real and complex polylogarithm series, absolute convergence on the closed unit disk, differentiation, duplication, Euler reflection and Landen identities, logarithmic moments, Fubini kernels and radial integration machinery. The formulas involve Catalan's constant, zeta(3), Li_4(1/2) and Im Li_3((1+i)/2). These are classical identities, not new informal results. A004 uses the corrected factor pi^2/24; A014 uses a proved expression entirely inside the unit disk, replacing the tutorial's invalid series expansion. A015 uses radial differentiation instead of a half-disc contour integral. The formalization was materially completed on 2026-10-01 at 00:01:57 UTC. The 2022 informal tutorial is older; the eligibility date is that of the completed Lean proofs.

Quoted from the card LeanPool/projects/polylog-integrals.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 21 main results, each with its informal statement quoted from the card. The scan finds 21 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

  • LeanPolyLog.Proofs.A001 (theorem), declared in LeanPool/PolylogIntegrals/Proofs/A001.lean, line 25: “Li_2(i) equals -pi^2/48 plus i times Catalan's constant.” Its source, as the card gives it: “Upstream Statements.lean and Proofs/A001.lean at the pinned commit; README prior-appearance table and blueprint/ERRATA.md label classical sources and corrections. Lean proofs were written with Claude assistance and reviewed by rainrzk; the informal tutorial is rainrzk (2022).”
  • LeanPolyLog.Proofs.A002 (theorem), declared in LeanPool/PolylogIntegrals/Proofs/A002.lean, line 27: “Li_2(1/(1+i)) equals 5 pi^2/96 - log^2(2)/8 plus i times (pi log(2)/8 - G).” Its source, as the card gives it: “Upstream Statements.lean and Proofs/A002.lean at the pinned commit; README prior-appearance table and blueprint/ERRATA.md label classical sources and corrections. Lean proofs were written with Claude assistance and reviewed by rainrzk; the informal tutorial is rainrzk (2022).”
  • LeanPolyLog.Proofs.A003 (theorem), declared in LeanPool/PolylogIntegrals/Proofs/A003.lean, line 27: “Li_2((sqrt(5)-1)/2) equals pi^2/10 - log^2((1+sqrt(5))/2).” Its source, as the card gives it: “Upstream Statements.lean and Proofs/A003.lean at the pinned commit; README prior-appearance table and blueprint/ERRATA.md label classical sources and corrections. Lean proofs were written with Claude assistance and reviewed by rainrzk; the informal tutorial is rainrzk (2022).”
  • LeanPolyLog.Proofs.A004 (theorem), declared in LeanPool/PolylogIntegrals/Proofs/A004.lean, line 27: “The integral from 0 to 1 of log(1+x^2)/x equals pi^2/24, correcting the tutorial's factor of two.” Its source, as the card gives it: “Upstream Statements.lean and Proofs/A004.lean at the pinned commit; README prior-appearance table and blueprint/ERRATA.md label classical sources and corrections. Lean proofs were written with Claude assistance and reviewed by rainrzk; the informal tutorial is rainrzk (2022).”
  • LeanPolyLog.Proofs.A005 (theorem), declared in LeanPool/PolylogIntegrals/Proofs/A005.lean, line 71: “The integral from 0 to 1 of log^2(1+x^2)/x^3 equals pi^2/12 - log^2(2).” Its source, as the card gives it: “Upstream Statements.lean and Proofs/A005.lean at the pinned commit; README prior-appearance table and blueprint/ERRATA.md label classical sources and corrections. Lean proofs were written with Claude assistance and reviewed by rainrzk; the informal tutorial is rainrzk (2022).”
  • LeanPolyLog.Proofs.A006_cos (theorem), declared in LeanPool/PolylogIntegrals/Proofs/A006.lean, line 27: “The integral from 0 to pi/4 of log(cos x) equals G/2 - (pi/4) log(2).” Its source, as the card gives it: “Upstream Statements.lean and Proofs/A006.lean at the pinned commit; README prior-appearance table and blueprint/ERRATA.md label classical sources and corrections. Lean proofs were written with Claude assistance and reviewed by rainrzk; the informal tutorial is rainrzk (2022).”
  • LeanPolyLog.Proofs.A006_sin (theorem), declared in LeanPool/PolylogIntegrals/Proofs/A006.lean, line 34: “The integral from 0 to pi/4 of log(sin x) equals -G/2 - (pi/4) log(2).” Its source, as the card gives it: “Upstream Statements.lean and Proofs/A006.lean at the pinned commit; README prior-appearance table and blueprint/ERRATA.md label classical sources and corrections. Lean proofs were written with Claude assistance and reviewed by rainrzk; the informal tutorial is rainrzk (2022).”
  • LeanPolyLog.Proofs.A007 (theorem), declared in LeanPool/PolylogIntegrals/Proofs/A007.lean, line 25: “The integral from 0 to pi/4 of x log(cos x) equals pi G/8 - pi^2 log(2)/32 - 21 zeta(3)/128.” Its source, as the card gives it: “Upstream Statements.lean and Proofs/A007.lean at the pinned commit; README prior-appearance table and blueprint/ERRATA.md label classical sources and corrections. Lean proofs were written with Claude assistance and reviewed by rainrzk; the informal tutorial is rainrzk (2022).”
  • LeanPolyLog.Proofs.A008 (theorem), declared in LeanPool/PolylogIntegrals/Proofs/A008.lean, line 27: “The integral from 0 to pi/4 of x log(1+tan x) equals pi^2 log(2)/64 - pi G/8 + 21 zeta(3)/64.” Its source, as the card gives it: “Upstream Statements.lean and Proofs/A008.lean at the pinned commit; README prior-appearance table and blueprint/ERRATA.md label classical sources and corrections. Lean proofs were written with Claude assistance and reviewed by rainrzk; the informal tutorial is rainrzk (2022).”
  • LeanPolyLog.Proofs.A009 (theorem), declared in LeanPool/PolylogIntegrals/Proofs/A009.lean, line 151: “The integral from 0 to pi/2 of x^2 cot x equals pi^2 log(2)/4 - 7 zeta(3)/8.” Its source, as the card gives it: “Upstream Statements.lean and Proofs/A009.lean at the pinned commit; README prior-appearance table and blueprint/ERRATA.md label classical sources and corrections. Lean proofs were written with Claude assistance and reviewed by rainrzk; the informal tutorial is rainrzk (2022).”
  • LeanPolyLog.Proofs.A010 (theorem), declared in LeanPool/PolylogIntegrals/Proofs/A010.lean, line 24: “The integral from 0 to pi/4 of x^2 tan^2 x equals -G + pi^2/16 - pi^3/192 + pi log(2)/4.” Its source, as the card gives it: “Upstream Statements.lean and Proofs/A010.lean at the pinned commit; README prior-appearance table and blueprint/ERRATA.md label classical sources and corrections. Lean proofs were written with Claude assistance and reviewed by rainrzk; the informal tutorial is rainrzk (2022).”
  • LeanPolyLog.Proofs.A011 (theorem), declared in LeanPool/PolylogIntegrals/Proofs/A011.lean, line 26: “The integral from 0 to 1 of Li_2(x)/(x sqrt(1-x^2)) equals 3 pi^2 log(2)/8 - 7 zeta(3)/16.” Its source, as the card gives it: “Upstream Statements.lean and Proofs/A011.lean at the pinned commit; README prior-appearance table and blueprint/ERRATA.md label classical sources and corrections. Lean proofs were written with Claude assistance and reviewed by rainrzk; the informal tutorial is rainrzk (2022).”
  • LeanPolyLog.Proofs.A012 (theorem), declared in LeanPool/PolylogIntegrals/Proofs/A012.lean, line 32: “The integral from 0 to 1 of arctan(x) log(x)/(1+x) equals -pi^3/64 + G log(2)/2.” Its source, as the card gives it: “Upstream Statements.lean and Proofs/A012.lean at the pinned commit; README prior-appearance table and blueprint/ERRATA.md label classical sources and corrections. Lean proofs were written with Claude assistance and reviewed by rainrzk; the informal tutorial is rainrzk (2022).”
  • LeanPolyLog.Proofs.A013 (theorem), declared in LeanPool/PolylogIntegrals/Proofs/A013.lean, line 35: “The integral from 0 to 1 of arctan(x) log^2(x)/(1+x) equals -pi^2 G/24 - pi^3 log(2)/32 + 21 pi zeta(3)/64.” Its source, as the card gives it: “Upstream Statements.lean and Proofs/A013.lean at the pinned commit; README prior-appearance table and blueprint/ERRATA.md label classical sources and corrections. Lean proofs were written with Claude assistance and reviewed by rainrzk; the informal tutorial is rainrzk (2022).”
  • LeanPolyLog.Proofs.A014 (theorem), declared in LeanPool/PolylogIntegrals/Proofs/A014.lean, line 34: “The integral from 0 to 1 of log(x) log(1+x)/(1+x^2) equals 11 pi^3/128 + 3 pi log^2(2)/32 - 2 G log(2) - 3 Im Li_3((1+i)/2).” Its source, as the card gives it: “Upstream Statements.lean and Proofs/A014.lean at the pinned commit; README prior-appearance table and blueprint/ERRATA.md label classical sources and corrections. Lean proofs were written with Claude assistance and reviewed by rainrzk; the informal tutorial is rainrzk (2022).”
  • LeanPolyLog.Proofs.A015 (theorem), declared in LeanPool/PolylogIntegrals/Proofs/A015.lean, line 64: “The integral from 0 to pi/2 of x log^2(sin x) equals Li_4(1/2) - 19 pi^4/2880 + log^4(2)/24 + pi^2 log^2(2)/12.” Its source, as the card gives it: “Upstream Statements.lean and Proofs/A015.lean at the pinned commit; README prior-appearance table and blueprint/ERRATA.md label classical sources and corrections. Lean proofs were written with Claude assistance and reviewed by rainrzk; the informal tutorial is rainrzk (2022).”
  • LeanPolyLog.Proofs.A016 (theorem; a main declaration), declared in LeanPool/PolylogIntegrals/Proofs/A016.lean, line 26: “The integral from 0 to 1 of Li_3(x)/(x sqrt(1-x^2)) equals Li_4(1/2)/2 + 41 pi^4/5760 + log^4(2)/48 + pi^2 log^2(2)/6.” Its source, as the card gives it: “Upstream Statements.lean and Proofs/A016.lean at the pinned commit; README prior-appearance table and blueprint/ERRATA.md label classical sources and corrections. Lean proofs were written with Claude assistance and reviewed by rainrzk; the informal tutorial is rainrzk (2022).”
  • LeanPolyLog.Dilog.hasDerivAt_Li_succ (theorem), declared in LeanPool/PolylogIntegrals/Lemmas/DilogComplex.lean, line 69: “For every natural s and nonzero complex z in the open unit disk, Li_(s+1) has derivative Li_s(z)/z at z.” Its source, as the card gives it: “Upstream Lemmas/DilogComplex.lean, termwise differentiation.”
  • LeanPolyLog.Dilog.Li_two_add_Li_two_div_sub_one (theorem), declared in LeanPool/PolylogIntegrals/Lemmas/DilogComplex.lean, line 130: “For complex z of norm at most 1 and real part at most 1/2, Li_2(z) + Li_2(z/(z-1)) = -log^2(1-z)/2, with the principal logarithm.” Its source, as the card gives it: “Upstream Lemmas/DilogComplex.lean, complex Landen identity.”
  • LeanPolyLog.Arcsin.integral_Lir_div_mul_sqrt (theorem), declared in LeanPool/PolylogIntegrals/Lemmas/Arcsin.lean, line 325: “For s at least 2 and a measurable nonnegative weight w on (0,1] with integrable moments equal to 1/(n+1)^s, the integral from 0 to 1 of Li_s(x)/(x sqrt(1-x^2)) equals the integral from 0 to pi/2 of w(sin t) times (pi/2+t).” Its source, as the card gives it: “Upstream Lemmas/Arcsin.lean, moment representation and Fubini.”
  • LeanPolyLog.Radial.integral_im_logCube (theorem), declared in LeanPool/PolylogIntegrals/Lemmas/Radial.lean, line 339: “If (log^3((1+r)/2)-log^3((1-r)/2))/r is interval integrable from 0 to 1, its integral equals the integral from 0 to pi of the imaginary part of the cube of the principal complex logarithm of (1+exp(i t))/2.” Its source, as the card gives it: “Upstream Lemmas/Radial.lean, radial differentiation and domination.”
Project
Sources
LeanLeanPolyLog.Proofs.A016

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.