feat(NumberTheory/LSeries): add completedRiemannZeta_conj

[sluvec]

Note from the author — AI disclosure (please read first):

I want to be upfront before any further review. I'm not a Lean or analytic-number-theory expert. This PR comes out of an AI-assisted research workflow I'm running on the Riemann hypothesis — a multi-agent system built on Claude (Anthropic) drafts the proofs, helper lemmas, and docstrings; I review the high-level structure, run local builds and linters, and decide what gets upstreamed.

For technical review comments I will route the question back through the agents and respond after consulting them, so my reply turnaround may be longer than usual. If this kind of contribution isn't a fit for mathlib's standards or review workflow, I'm happy to close the PR — please just let me know.

---

What

Adds the Schwarz reflection / conjugation symmetry identities for the completed Riemann zeta function and its entire piece:

theorem completedRiemannZeta_conj (s : ℂ) :
    completedRiemannZeta (conj s) = conj (completedRiemannZeta s)
theorem completedRiemannZeta₀_conj (s : ℂ) :
    completedRiemannZeta₀ (conj s) = conj (completedRiemannZeta₀ s)

These are added to Mathlib/NumberTheory/LSeries/RiemannZeta.lean, next to the functional-equation lemmas completedRiemannZeta_one_sub and completedRiemannZeta₀_one_sub already in that file.

Why

These identities are the conj-equivariance counterpart of the functional equation Λ(1 − s) = Λ(s) already in mathlib. Together they make explicit the full symmetry group of Λ acting on ℂ (the Klein four-group generated by s ↦ 1 − s and s ↦ conj s), which is the standard setup for the Hardy Ξ-function

Ξ(t) = (1/2) · t · (t − 1) · π^(−t/2) · Γ(t/2) · ζ(t)   evaluated on the critical line

Concretely, the two new lemmas mirror Complex.Gamma_conj for Λ (the analogous identity for Gamma) and are used in third-party formalisations involving real-valuedness on the critical line.

Proof strategy

1. On the open half-plane {Re s > 1}, the Dirichlet series for Λ converges absolutely and conjugation commutes term-by-term with the series (Complex.conj_tsum), with Complex.Gamma_conj, and with cpow of the positive real bases π and n : ℕ (via Complex.conj_cpow, using natCast_arg and Complex.arg_ofReal_of_nonneg to discharge the side conditions on arg).
2. Both sides extend to entire functions of s; the identity principle (AnalyticOnNhd.eq_of_eventuallyEq) propagates the equality from the open set {Re s > 1} (a neighborhood of z₀ = 2) to all of ℂ.
3. The pole-decomposition completedRiemannZeta_eq (Λ s = Λ₀ s − 1/s − 1/(1 − s)) transfers the result from Λ₀ (entire) to the full Λ (which has simple poles at s = 0, 1).

Five private lemma helpers encapsulate the per-factor computations:
conj_natCast_cpow, conj_pi_cpow, completedRiemannZeta_conj_of_one_lt_re, completedRiemannZeta₀_conj_of_one_lt_re, differentiable_conj_completedZeta₀_conj.

Note: Following @tb65536's review, a shorter proof using the "completedRiemannZeta is real on the real axis" strategy is being prepared and will replace the current proof.

New imports

Two new public imports are added to RiemannZeta.lean:

• Mathlib.Analysis.Calculus.Deriv.Star — for DifferentiableAt.conj_conj (used in differentiable_conj_completedZeta₀_conj to show s ↦ conj (Λ₀ (conj s)) is entire).
• Mathlib.Analysis.Analytic.Uniqueness — for AnalyticOnNhd.eq_of_eventuallyEq (the identity principle).

Both are needed for the analytic-continuation step. Happy to refactor to use a weaker continuation lemma if either feels too heavy.

Checklist

• Theorem names follow the existing mathlib *_conj convention (Gamma_conj, GammaIntegral_conj, cpow_conj, log_conj, arg_conj).
• Module docstring updated under ## Main results to list the two new theorems.
• Module-level open scoped updated: added ComplexConjugate (needed for conj notation; the rest of the file did not need it).
• private lemma for all helpers (none are exposed as part of the public API).
• No new sorry.
• lake build Mathlib.NumberTheory.LSeries.RiemannZeta passes locally on master (toolchain leanprover/lean4:v4.30.0-rc2).
• lake exe runLinter Mathlib.NumberTheory.LSeries.RiemannZeta passes locally (no warnings).
• Commit signed-off (DCO).
• No file moves, no deletions, no changes to Mathlib.lean (added to an existing file).
• AI usage disclosed (see top of description).

LLM-generated

[github-actions]

PR summary d52548d112

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.NumberTheory.LSeries.RiemannZeta	2735	2737	+2 (+0.07%)

Import changes for all files

Files	Import difference
12 files Mathlib.NumberTheory.ModularForms.CuspFormSubmodule Mathlib.NumberTheory.ModularForms.DedekindEta Mathlib.NumberTheory.ModularForms.Delta Mathlib.NumberTheory.ModularForms.Derivative Mathlib.NumberTheory.ModularForms.DimensionFormulas.LevelOne Mathlib.NumberTheory.ModularForms.Discriminant Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.MDifferentiable Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing	1
11 files Mathlib.NumberTheory.EulerProduct.DirichletLSeries Mathlib.NumberTheory.Harmonic.ZetaAsymp Mathlib.NumberTheory.LSeries.DirichletContinuation Mathlib.NumberTheory.LSeries.Dirichlet Mathlib.NumberTheory.LSeries.HurwitzZetaValues Mathlib.NumberTheory.LSeries.Nonvanishing Mathlib.NumberTheory.LSeries.PrimesInAP Mathlib.NumberTheory.LSeries.RiemannZeta Mathlib.NumberTheory.LSeries.ZMod Mathlib.NumberTheory.LSeries.ZetaZeros Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs	2

---

Declarations diff

+ completedRiemannZeta_conj
+ completedRiemannZeta_conj_of_one_lt_re
+ completedRiemannZeta₀_conj
+ completedRiemannZeta₀_conj_of_one_lt_re
+ conj_natCast_cpow
+ conj_pi_cpow
+ differentiable_conj_completedZeta₀_conj

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to strong technical debt.

No changes to weak technical debt.

[tb65536]

Can you instead prove this from the fact that completedRiemannZeta is real on the real axis?

[sluvec]

Thank you, working on revised version. PS - the PR was AI generated - I'll update/tag where necessary.

[tb65536]

Btw, there was a similar PR a while back: #36324

[grunweg]

I want to be upfront before any further review. I'm not a Lean or analytic-number-theory expert. This PR comes out of an AI-assisted research workflow I'm running on the Riemann hypothesis — a multi-agent system built on Claude (Anthropic) drafts the proofs, helper lemmas, and docstrings; I review the high-level structure, run local builds and linters, and decide what gets upstreamed.

For technical review comments I will route the question back through the agents and respond after consulting them, so my reply turnaround may be longer than usual. If this kind of contribution isn't a fit for mathlib's standards or review workflow, I'm happy to close the PR — please just let me know.

This kind of contribution is not fit for mathlib's standards. (We have a general rule about this: in general, this requires a much larger investment of reviewer time than more traditional contributions, and review time is already a very scarce resource we have to prioritise judiciously.)
For this reason, I'm closing this PR. Thanks for your understanding!

[sluvec]

I want to be upfront before any further review. I'm not a Lean or analytic-number-theory expert. This PR comes out of an AI-assisted research workflow I'm running on the Riemann hypothesis — a multi-agent system built on Claude (Anthropic) drafts the proofs, helper lemmas, and docstrings; I review the high-level structure, run local builds and linters, and decide what gets upstreamed.
For technical review comments I will route the question back through the agents and respond after consulting them, so my reply turnaround may be longer than usual. If this kind of contribution isn't a fit for mathlib's standards or review workflow, I'm happy to close the PR — please just let me know.

This kind of contribution is not fit for mathlib's standards. (We have a general rule about this: in general, this requires a much larger investment of reviewer time than more traditional contributions, and review time is already a very scarce resource we have to prioritise judiciously.) For this reason, I'm closing this PR. Thanks for your understanding!

Thank you for the clarity, fully understood. I'll continue the project locally.