feat(Analysis/Analytic): simple zeros and logarithmic residue by psinary-sketch · Pull Request #36778 · leanprover-community/mathlib4

psinary-sketch · 2026-03-17T20:01:48Z

Three new theorems about simple zeros of analytic functions:

AnalyticAt.analyticOrderAt_eq_one_of_zero_deriv_ne_zero: if f is analytic at z₀, f(z₀) = 0, and f'(z₀) ≠ 0, then analyticOrderAt f z₀ = 1.
AnalyticAt.eventually_ne_of_deriv_ne_zero: under the same hypotheses, f is nonzero in a punctured neighborhood of z₀.
AnalyticAt.tendsto_residue_simple_zero: the logarithmic residue (w - z₀) * f'(w)/f(w) → 1 as w → z₀. Key ingredient for residue computation of meromorphic functions.

github-actions · 2026-03-17T20:01:58Z

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 · 2026-03-17T20:03:05Z

PR summary 1c7e491807

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Analysis.Analytic.SimpleZero` (new file)	2578

Declarations diff

+ AnalyticAt.analyticOrderAt_eq_one_of_zero_deriv_ne_zero
+ AnalyticAt.eventually_ne_of_deriv_ne_zero
+ AnalyticAt.tendsto_residue_simple_zero

You can run this locally as follows

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./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 · 2026-03-17T20:08:12Z

+set_option linter.style.longLine false
+module  -- shake: keep-all


Could you remove this change?

Done, removed the stale lines. Thanks for catching that.

wwylele · 2026-03-17T20:26:32Z

 public import Mathlib.Util.TransImports
 public import Mathlib.Util.WhatsNew
 public import Mathlib.Util.WithWeakNamespace



What's up with these changes?

Sorry, artifact from PowerShell line-ending handling. Let me fix.

Fixed — the trailing changes were an artifact of PowerShell line-ending handling. The diff should now be clean: just the one import line added.

Three new theorems about simple zeros of analytic functions: - AnalyticAt.analyticOrderAt_eq_one_of_zero_deriv_ne_zero: if f is analytic at z₀, f(z₀) = 0, and f'(z₀) ≠ 0, then analyticOrderAt f z₀ = 1. - AnalyticAt.eventually_ne_of_deriv_ne_zero: under the same hypotheses, f is nonzero in a punctured neighborhood of z₀. - AnalyticAt.tendsto_residue_simple_zero: the logarithmic residue (w - z₀) * f'(w)/f(w) → 1 as w → z₀. Key ingredient for residue computation of meromorphic functions.

wwylele

I didn't check the proof body and only commented on statements. But the amount of have suggests there are likely space to simplify the proof

wwylele · 2026-03-18T01:32:36Z

+public section SimpleZero
+
+/-- At a zero with nonvanishing derivative, the analytic order is 1. -/
+theorem AnalyticAt.analyticOrderAt_eq_one_of_zero_deriv_ne_zero


Since this is a direct corollary of AnalyticAt.analyticOrderAt_sub_eq_one_of_deriv_ne_zero, I think it should be moved to that file next to the existing lemma

wwylele · 2026-03-18T01:34:46Z

+  rwa [analyticOrderAt_congr this] at h
+
+/-- At a simple zero, the function is nonzero in a punctured neighborhood. -/
+theorem AnalyticAt.eventually_ne_of_deriv_ne_zero


Same for this one. It should be either in Mathlib.Analysis.Analytic.IsolatedZeros or Mathlib.Analysis.Analytic.Order, whichever is further from the import tree root

wwylele · 2026-03-18T01:41:47Z

+theorem AnalyticAt.tendsto_residue_simple_zero
+    {f : ℂ → ℂ} {z₀ : ℂ} (hf : AnalyticAt ℂ f z₀)
+    (hfz : f z₀ = 0) (hf' : deriv f z₀ ≠ 0) :
+    Tendsto (fun w => (w - z₀) * (deriv f w / f w))


Since logDeriv f x = deriv f x / f x, I think this should be stated with logDeriv and moved to Mathlib.Analysis.Calculus.LogDeriv

Thanks for the detailed review! You're right on all points — these belong in their natural homes rather than a new file. I'll close this PR and split into three smaller ones:

analyticOrderAt_eq_one_of_zero_deriv_ne_zero → added to Order.lean
eventually_ne_of_deriv_ne_zero (without hfz) → added to Order.lean or IsolatedZeros.lean
Residue limit restated with logDeriv → added to LogDeriv.lean

Will also simplify the proofs. Thanks for guiding the placement.

wwylele · 2026-03-18T01:49:30Z

+/-- At a simple zero, the function is nonzero in a punctured neighborhood. -/
+theorem AnalyticAt.eventually_ne_of_deriv_ne_zero
+    {f : ℂ → ℂ} {z₀ : ℂ} (hf : AnalyticAt ℂ f z₀)
+    (hfz : f z₀ = 0) (hf' : deriv f z₀ ≠ 0) :


(hfz : f z₀ = 0) can be dropped, right?

…derivative Add \AnalyticAt.eventually_ne_nhdsWithin_of_deriv_ne_zero\: if f is analytic at x and f'(x) ≠ 0, then f(w) ≠ f(x) in a punctured neighborhood of x. No hypothesis on f(x) needed (per review feedback on leanprover-community#36778). Placed in Order.lean next to \�nalyticOrderAt_sub_eq_one_of_deriv_ne_zero\.

Add \AnalyticAt.tendsto_mul_logDeriv_simple_zero\: if f is analytic at x, f(x) = 0, and f'(x) ≠ 0, then \(w - x) * logDeriv f w → 1\ as \w → x\. Restated with \logDeriv\ and placed in \LogDeriv.lean\ per review feedback on leanprover-community#36778. Split from leanprover-community#36778 (3 of 3).

Add AnalyticAt.tendsto_mul_logDeriv_simple_zero: if f is analytic at x, f(x) = 0, and f'(x) != 0, then (w - x) * logDeriv f w tends to 1 as w tends to x. Restated with logDeriv per review feedback on leanprover-community#36778. Split from leanprover-community#36778 (3 of 3).

psinary-sketch · 2026-03-20T07:18:49Z

Closing in favor of the three split PRs per @wwylele's review:

#36865 (analytic order at zero → Order.lean)
#36871 (eventually ne → Order.lean)
#36881 (logarithmic residue → LogDeriv.lean)

Thanks for the guidance on placement.

…derivative Add \AnalyticAt.eventually_ne_nhdsWithin_of_deriv_ne_zero\: if f is analytic at x and f'(x) ≠ 0, then f(w) ≠ f(x) in a punctured neighborhood of x. No hypothesis on f(x) needed (per review feedback on leanprover-community#36778). Placed in Order.lean next to \�nalyticOrderAt_sub_eq_one_of_deriv_ne_zero\.

@wwylele

Add `AnalyticAt.tendsto_mul_logDeriv_simple_zero`: if f is analytic at x, f(x) = 0, and f'(x) ≠ 0, then `(w - x) * logDeriv f w → 1` as `w → x`. Restated with `logDeriv` and placed in `LogDeriv.lean` per review feedback from @wwylele on #36778. Split from #36778 (3 of 3). Co-authored-by: interleaves <psinary@hotmail.com>

…derivative Add \AnalyticAt.eventually_ne_nhdsWithin_of_deriv_ne_zero\: if f is analytic at x and f'(x) ≠ 0, then f(w) ≠ f(x) in a punctured neighborhood of x. No hypothesis on f(x) needed (per review feedback on leanprover-community#36778). Placed in Order.lean next to \�nalyticOrderAt_sub_eq_one_of_deriv_ne_zero\.

git checkout schwarz-reflection git rebase upstream/master git push origin schwarz-reflection --force-with-lease git stash pop Add AnalyticAt.tendsto_mul_logDeriv_simple_zero: if f is analytic at x, f(x) = 0, and f'(x) != 0, then (w - x) * logDeriv f w tends to 1 as w tends to x. Restated with logDeriv per review feedback on leanprover-community#36778. Split from leanprover-community#36778 (3 of 3).

…derivative Add \AnalyticAt.eventually_ne_nhdsWithin_of_deriv_ne_zero\: if f is analytic at x and f'(x) ≠ 0, then f(w) ≠ f(x) in a punctured neighborhood of x. No hypothesis on f(x) needed (per review feedback on leanprover-community#36778). Placed in Order.lean next to \�nalyticOrderAt_sub_eq_one_of_deriv_ne_zero\.

@wwylele

…ver-community#36881) Add `AnalyticAt.tendsto_mul_logDeriv_simple_zero`: if f is analytic at x, f(x) = 0, and f'(x) ≠ 0, then `(w - x) * logDeriv f w → 1` as `w → x`. Restated with `logDeriv` and placed in `LogDeriv.lean` per review feedback from @wwylele on leanprover-community#36778. Split from leanprover-community#36778 (3 of 3). Co-authored-by: interleaves <psinary@hotmail.com>

…36865) Add AnalyticAt.analyticOrderAt_eq_one_of_zero_deriv_ne_zero: if f is analytic at x, f(x) = 0, and f'(x) ≠ 0, then analyticOrderAt f x = 1. Placed next to analyticOrderAt_sub_eq_one_of_deriv_ne_zero in Order.lean per review feedback on #36778. AI disclosure: Lean code developed with Claude (Anthropic) assistance in workflow. Mathematical content and proof strategies are original. All code verified locally with lake env lean before submission. Co-authored-by: interleaves <psinary@hotmail.com>

…derivative Add \AnalyticAt.eventually_ne_nhdsWithin_of_deriv_ne_zero\: if f is analytic at x and f'(x) ≠ 0, then f(w) ≠ f(x) in a punctured neighborhood of x. No hypothesis on f(x) needed (per review feedback on leanprover-community#36778). Placed in Order.lean next to \�nalyticOrderAt_sub_eq_one_of_deriv_ne_zero\.

github-actions Bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Mar 17, 2026

github-actions Bot added the t-analysis Analysis (normed *, calculus) label Mar 17, 2026

wwylele reviewed Mar 17, 2026

View reviewed changes

psinary-sketch force-pushed the simple-zero-clean branch from b6d71d6 to d33e560 Compare March 17, 2026 20:21

wwylele reviewed Mar 17, 2026

View reviewed changes

psinary-sketch force-pushed the simple-zero-clean branch from d33e560 to 334244a Compare March 17, 2026 20:31

wwylele reviewed Mar 18, 2026

View reviewed changes

psinary-sketch mentioned this pull request Mar 19, 2026

[Merged by Bors] - feat(Analysis/Analytic): analytic order at zero with vanishing value #36865

Closed

psinary-sketch mentioned this pull request Mar 19, 2026

feat(Analysis/Analytic): nonvanishing in punctured neighborhood from derivative #36871

Closed

psinary-sketch mentioned this pull request Mar 20, 2026

[Merged by Bors] - feat(Analysis/Calculus): logarithmic residue at simple zeros #36881

Closed

psinary-sketch closed this Mar 20, 2026

SnirBroshi added the LLM-generated PRs with substantial input from LLMs - review accordingly label Mar 25, 2026

		set_option linter.style.longLine false
		module -- shake: keep-all

Uh oh!

Conversation

psinary-sketch commented Mar 17, 2026

Uh oh!

github-actions Bot commented Mar 17, 2026

Welcome new contributor!

Uh oh!

github-actions Bot commented Mar 17, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 1c7e491807

Import changes for modified files

Declarations diff

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

psinary-sketch Mar 17, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

wwylele left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

psinary-sketch commented Mar 20, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

github-actions Bot commented Mar 17, 2026 •

edited

Loading

psinary-sketch Mar 17, 2026 •

edited

Loading