feat: lemmas for the analytic part of the proof of the Gelfond–Schneider theorem (Part 4/5) by mkaratarakis · Pull Request #35316 · leanprover-community/mathlib4

mkaratarakis · 2026-02-14T17:42:36Z

github-actions · 2026-02-14T17:42:47Z

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.

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.

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-02-14T17:43:50Z

PR summary 96eec06566

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.NumberTheory.Transcendental.AnalyticPart` (new file)	2499

Declarations diff

+ analyticOrderAt_deriv_eq_top_iff_of_eq_zero
+ analyticOrderAt_deriv_order_eq_succ
+ analyticOrderAt_eq_nat_iff_iteratedDeriv_eq_zero
+ le_analyticOrderAt_iff_iteratedDeriv_eq_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).

mathlib-dependent-issues · 2026-03-10T15:20:25Z

This PR/issue depends on:

~~[Merged by Bors] - feat: lemmas for the analytic part of the proof of the Gelfond–Schneider theorem (Part 3/5) #35315~~
By Dependent Issues (🤖). Happy coding!

merge master

into analysispart4 pull

merge master

into analysispart4

mkaratarakis · 2026-03-31T08:01:20Z

-awaiting-author

merge master

MichaelStollBayreuth · 2026-04-19T17:59:45Z

+/-!
+Auxiliary lemmata covering the analytic part of the proof of the Gelfond–Schneider theorem.
+Move to appropriate files in Analysis/Complex or Analysis/Analytic and change docstring accordingly.
+-/


Please move the lemmas to Mathlib.Analysis.Analytic.Order (where the other results on analyticOrderAt also reside) and remove this file (don't forget to also remove the import from Mathlib.lean).

MichaelStollBayreuth · 2026-04-19T18:03:41Z

+  | some 0 =>
+    have Hn_zero : analyticOrderAt f z₀ = 0 := Hn'
+    exact hf.analyticOrderAt_eq_zero.mp Hn_zero hzero |>.elim
+  | some (n'' + 1) =>


Why n'' and not simply n (or n', but I don't think there is another n here that would be relevant)?

MichaelStollBayreuth · 2026-04-19T18:06:28Z

+    have Hn_coe : analyticOrderAt f z₀ = ↑(n'' + 1) := Hn'
+    have := horder ▸ analyticOrderAt_deriv_of_pos hf Hn_coe
+    norm_cast at this ⊢
+    have hchar : ringChar ℂ = 0 := by aesop


Suggested change

have hchar : ringChar ℂ = 0 := by aesop

have hchar : ringChar ℂ = 0 := ringChar.eq ℂ 0

MichaelStollBayreuth · 2026-04-19T18:09:43Z

+
+lemma analyticOrderAt_eq_nat_iff_iteratedDeriv_eq_zero {f : ℂ → ℂ} {z₀ : ℂ} {n : ℕ}
+    (hf : AnalyticAt ℂ f z₀) :
+    analyticOrderAt f z₀ = n ↔ (∀ k < n, deriv^[k] f z₀ = 0) ∧ deriv^[n] f z₀ ≠ 0 := by


Why not use iteratedDeriv? Thre is more API (loogle says 169 decls compared to 44) than for deriv^[n].

kebekus · 2026-04-21T11:34:50Z

@MichaelStollBayreuth Will review as requested, but might not be able to do that before the weekend (=25/26Apr). Sorry for being slow.

analytic part

85a6997

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 Feb 14, 2026

github-actions Bot added the t-number-theory Number theory (also use t-algebra or t-analysis to specialize) label Feb 14, 2026

SnirBroshi reviewed Feb 14, 2026

View reviewed changes

Comment thread Mathlib/NumberTheory/Transcendental/AnalyticPart.lean

SnirBroshi reviewed Feb 14, 2026

View reviewed changes

Comment thread Mathlib/NumberTheory/Transcendental/AnalyticPart Outdated

lean extension + docstring

478d987

mathlib-dependent-issues Bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Feb 18, 2026

mkaratarakis mentioned this pull request Feb 25, 2026

feat(NumberTheory): non-vanishing derivative and algebraic lower bound for Gelfond-Schneider #35744

Open

3 tasks

mathlib-dependent-issues Bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Mar 10, 2026

mkaratarakis and others added 11 commits March 16, 2026 18:47

Merge branch 'master' into analysispart4

729f3ef

Merge branch 'master' into analysispart4

0274bc9

merge master

Merge branch 'master' into analysispart4

846543f

merge master

Merge branch 'analysispart4' of https://github.com/mkaratarakis/mathlib4

19d6e7e

into analysispart4 pull

Merge branch 'master' into analysispart4

f006fcc

merge master

Merge branch 'master' into analysispart4

5a5220e

fix errors

ba7ef9a

Merge branch 'analysispart4' of https://github.com/mkaratarakis/mathlib4

6df3bcd

into analysispart4

mk all

e8a9205

Merge branch 'master' into analysispart4

9e4240b

Merge branch 'analysispart4' of https://github.com/mkaratarakis/mathlib4

c130f96

into analysispart4

mathlib-triage Bot assigned MichaelStollBayreuth Mar 27, 2026

MichaelStollBayreuth reviewed Mar 30, 2026

View reviewed changes

MichaelStollBayreuth added the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 30, 2026

reviews

4c96ca4

github-actions Bot removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 31, 2026

Merge branch 'master' into analysispart4

151b61d

merge master

MichaelStollBayreuth reviewed Apr 19, 2026

View reviewed changes

MichaelStollBayreuth requested a review from kebekus April 19, 2026 18:10

MichaelStollBayreuth added the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 19, 2026

	have hchar : ringChar ℂ = 0 := by aesop
	have hchar : ringChar ℂ = 0 := ringChar.eq ℂ 0

Conversation

mkaratarakis commented Feb 14, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Feb 14, 2026

Welcome new contributor!

Uh oh!

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

Uh oh!

PR summary 96eec06566

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

mathlib-dependent-issues Bot commented Mar 10, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

mkaratarakis commented Mar 31, 2026

Uh oh!

MichaelStollBayreuth Apr 19, 2026

Choose a reason for hiding this comment

Uh oh!

MichaelStollBayreuth Apr 19, 2026

Choose a reason for hiding this comment

Uh oh!

MichaelStollBayreuth Apr 19, 2026

Choose a reason for hiding this comment

Uh oh!

MichaelStollBayreuth Apr 19, 2026

Choose a reason for hiding this comment

Uh oh!

kebekus commented Apr 21, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

mkaratarakis commented Feb 14, 2026 •

edited

Loading

github-actions Bot commented Feb 14, 2026 •

edited

Loading