[Merged by Bors] - feat(NumberTheory/Harmonic/ZetaAsymp): conjugation symmetry of riemannZeta

[owenpkent]

This PR adds the reflection (conjugation) symmetry of the Riemann zeta function to Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean:

• riemannZeta_conj :riemannZeta (conj s) = conj (riemannZeta s);
• riemannZeta_conj_eq_zero_iff : riemannZeta (conj s) = 0 ↔ riemannZeta s = 0 (the zeros are symmetric under complex conjugation).

This is the natural companion to the functional equation already in Mathlib (riemannZeta_one_sub). Together the two symmetries s ↦ 1 - s and s ↦ conj s generate the quadruple symmetry {ρ, 1 - ρ, conj ρ, 1 - conj ρ} of the nontrivial zeros, and the reflection symmetry alone is a basic, frequently-used fact (it is why the zeros come in conjugate pairs).

Mathematical content: ζ has real Dirichlet coefficients, so on 1 < re s the identity conj (ζ (conj s)) = ζ s holds termwise from zeta_eq_tsum_one_div_nat_cpow and Complex.conj_cpow. The identity principle for analytic functions then propagates it across the connected domain ℂ ∖ {1} (AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq); analyticity of conj ∘ ζ ∘ conj is the anti-holomorphic composition HasDerivAt.conj_conj.

The PR adds two imports (Mathlib.Analysis.Calculus.Deriv.Star, Mathlib.Analysis.Normed.Module.Connected), both confirmed required.

---

AI use disclosure (per Mathlib's contribution guidelines): this result was formalized in a personal research project with the help of an AI coding agent (Claude Code). The agent assisted in developing the original proof and in porting it onto current Mathlib master (transplanting the verified proof, adapting the imports to the new module system, and confirming the build is green with #print axioms clean). The result is standard and the proof uses only existing Mathlib API. I have reviewed and understand the proof, take responsibility for the content, and will respond to review in my own words.

[github-actions]

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

[github-actions]

PR summary e3d37291a5

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.NumberTheory.Harmonic.ZetaAsymp	2985	2996	+11 (+0.37%)

Import changes for all files

Files	Import difference
3 files Mathlib.NumberTheory.LSeries.Nonvanishing Mathlib.NumberTheory.LSeries.PrimesInAP Mathlib.NumberTheory.LSeries.ZetaZeros	2
Mathlib.NumberTheory.Harmonic.ZetaAsymp	11

---

Declarations diff (regex)

+ riemannZeta_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.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit e3d3729).

• +1 new declarations
• −0 removed declarations

+riemannZeta_conj

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit e3d37291a5
Reference commit 9e735227e7

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[wwylele]

If this PR doesn't do better than #39743, I suspect it will be closed as well

[loefflerd]

I agree with Weiyi's comment about s ≠ 1. I'd propose moving this result to the ZetaAsymptotics file so you can use riemannZeta_one. I also left a few suggested refinements.

awaiting-author

[owenpkent]

Thanks for the review! I've made the changes: - Moved the theorem to Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean so it can use riemannZeta_one, and dropped the s != 1 hypothesis entirely (the zero-iff corollary is hypothesis-free now too). - Applied all three inline suggestions (natCast_arg + positivity, the isPreconnected inlining, and hypotheses left of the colon in the have statements). - Retitled the PR to match the new location, and merged master to resolve a conflict with #41205 which touched the same file. Ready for another look.

…

-Owen *This communication, along with any documents, files or attachments, is intended only for the use of the addressee and may contain legally privileged and confidential information. If you are not the intended recipient, you are hereby notified that any dissemination, distribution or copying of any information contained in or attached to this communication is strictly prohibited. If you have received this message in error, please notify the sender immediately and destroy the original communication and its attachments without reading, printing or saving in any manner. *

On Mon, Jun 29, 2026 at 6:43 AM Michael Stoll ***@***.***> wrote: ***@***.**** commented on this pull request. ------------------------------ In Mathlib/NumberTheory/LSeries/RiemannZeta.lean <#41133 (comment)> : > + have hpow : conj ((n : ℂ) ^ (conj z)) = (n : ℂ) ^ z := by + have hcc := Complex.conj_cpow (n : ℂ) z harg + rw [Complex.conj_natCast] at hcc + exact hcc.symm + rw [map_div₀, map_one, hpow] + rw [zeta_eq_tsum_one_div_nat_cpow hcz1, Complex.conj_tsum, + zeta_eq_tsum_one_div_nat_cpow hz1] + exact tsum_congr hterm + -- identity principle on the connected `{1}ᶜ`, anchored at `s = 2` + have hfg : (fun z => conj (riemannZeta (conj z))) =ᶠ[nhds (2 : ℂ)] riemannZeta := + Filter.eventuallyEq_of_mem + ((isOpen_lt continuous_const Complex.continuous_re).mem_nhds (by norm_num)) + (fun z hz => hgz z hz) + have hU : IsPreconnected ({1}ᶜ : Set ℂ) := + (isConnected_compl_singleton_of_one_lt_rank + (by rw [Complex.rank_real_complex]; norm_num) 1).isPreconnected ...and then the proof probably fits on one line. — Reply to this email directly, view it on GitHub <#41133?email_source=notifications&email_token=AE4T73AJ7WVFSO52RZYKHKL5CJQAHA5CNFSNUABKM5UWIORPF5TWS5BNNB2WEL2QOVWGYUTFOF2WK43UKJSXM2LFO4XTINJZGE4TCMBXGYZKM4TFMFZW63VGMF2XI2DPOKSWK5TFNZ2KYZTPN52GK4S7MNWGSY3L#discussion_r3491765182>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AE4T73GW6EDE4CLD3H3DEED5CJQAHAVCNFSNUABFKJSXA33TNF2G64TZHMZTMNJWHE3TIOJTHNEXG43VMU5TINZWGM3DANRYG432C5QC> . You are receiving this because you authored the thread.Message ID: ***@***.***>

[wwylele]

You can write "-awaiting-author" to remove the tag and signal this is ready for review. You can read https://leanprover-community.github.io/contribute/index.html#lifecycle-of-a-pr for more about review cycles

[owenpkent]

-awaiting-author

[owenpkent]

Thanks for the pointer on the review cycle. Removed the tag now that the requested changes are in. Happy to iterate if anything else comes up.

…

-Owen *This communication, along with any documents, files or attachments, is intended only for the use of the addressee and may contain legally privileged and confidential information. If you are not the intended recipient, you are hereby notified that any dissemination, distribution or copying of any information contained in or attached to this communication is strictly prohibited. If you have received this message in error, please notify the sender immediately and destroy the original communication and its attachments without reading, printing or saving in any manner. *

On Fri, Jul 3, 2026 at 2:42 PM Weiyi Wang ***@***.***> wrote: *wwylele* left a comment (leanprover-community/mathlib4#41133) <#41133 (comment)> You can write "-awaiting-author" to remove the tag and signal this is ready for review. You can read https://leanprover-community.github.io/contribute/index.html#lifecycle-of-a-pr for more about review cycles — Reply to this email directly, view it on GitHub <#41133?email_source=notifications&email_token=AE4T73D7YI5T6YLH3NNCHK35DALEHA5CNFSNUABFM5UWIORPF5TWS5BNNB2WEL2JONZXKZKDN5WW2ZLOOQXTIOBXHEZDGOBYGEY2M4TFMFZW63VGMF2XI2DPOKSWK5TFNZ2KYZTPN52GK4S7MNWGSY3L#issuecomment-4879238811>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AE4T73D6GHDTLBHWTWLBQ4T5DALEHAVCNFSNUABFKJSXA33TNF2G64TZHMZTMNJWHE3TIOJTHNEXG43VMU5TINZWGM3DANRYG432C5QC> . You are receiving this because you authored the thread.Message ID: ***@***.***>

[loefflerd]

Thanks for revising this! The main proof is fine now, I just found a couple of trivial golfs.

[owenpkent]

Thanks David, all three addressed in e3d3729:

• Tagged riemannZeta_conj with @[simp] and dropped riemannZeta_conj_eq_zero_iff (the zero-symmetry goal now closes by simp).
• push_cast; rfl -> norm_cast in the s = 1 branch.
• Let the membership goal infer its type: (2 : ℂ) ∈ _.

Module builds and runLinter passes clean (no simpNF issue from the new simp tag).

[loefflerd]

Great, I think this is ready for merging now. I'll send it on to the maintainers for the final decision.

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by loefflerd.

[j-loreaux]

@owenpkent for future reference, please do not let AI write the PR description. GitHub interactions should be human-to-human. (I realize you did this for your responses.) I updated the PR description to remove irrelevant information and reflect the changes made during review.

[j-loreaux]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Post-Build Step
• ci (staging) / Build
• ci (staging) / Lint style
• ci (staging) / Test and lint
• ci (staging) / Post-CI job