feat(Mathlib/Analysis/Polynomial/MahlerMeasure): Mahler Measure for other rings by khwilson · Pull Request #33463 · leanprover-community/mathlib4

khwilson · 2026-01-01T17:56:37Z

Define mahlerMeasure' which allows you specify a norm preserving map v from any NormedRing A (or more general) to ℂ. Also provide wrappers around the main mahlerMeasure lemmas that are used for estimation.

…ther rings Define `mahlerMeasure'` which allows you specify a norm preserving map `v` from any `NormedRing A` (or more general) to `ℂ`. Also provide wrappers around the main `mahlerMeasure` lemmas that are used for estimation.

github-actions · 2026-01-01T17:57:42Z

PR summary 5fbb6779b0

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ Monic.one_le_mapMahlerMeasure
+ leadingCoeff_le_mahlerMeasure
+ leadingCoeff_le_mapMahlerMeasure
+ mapMahlerMeasure
+ mapMahlerMeasure_const
+ mapMahlerMeasure_eq
+ mapMahlerMeasure_le_sum_norm_coeff
+ mapMahlerMeasure_mul
+ mapMahlerMeasure_nonneg
+ mapMahlerMeasure_one
+ mapMahlerMeasure_pos_of_ne_zero
+ mapMahlerMeasure_zero
+ norm_coeff_le_choose_mul_mapMahlerMeasure

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/Analysis/Polynomial/MahlerMeasure.lean

Co-authored-by: Aaron Liu <[email protected]>

Mathlib/Analysis/Polynomial/MahlerMeasure.lean

Co-authored-by: Vlad Tsyrklevich <[email protected]>

khwilson · 2026-01-02T00:18:53Z

Thanks for the simplicifications!

Mathlib/Analysis/Polynomial/MahlerMeasure.lean

Co-authored-by: Vlad Tsyrklevich <[email protected]>

Add a comment on the definition of `mahlerMeasure'`

j-loreaux · 2026-02-10T18:15:10Z

@khwilson the build on this PR is failing, so it is not on the queue. That's why it is not being reviewed. Please fix the build. 😃

khwilson · 2026-02-10T21:05:19Z

@j-loreaux I think it was just a linting error. Builds locally now and we'll see if it runs!

j-loreaux

I'm not totally convinced we need this, but it's not my area, so I'll review it as if we do and trust you on that, and then let another maintainer have the final say.

Mathlib/Analysis/Polynomial/MahlerMeasure.lean

khwilson · 2026-02-10T21:59:02Z

Ah, yes, sorry it's been a bit. I now recall that I needed to reopen this conversation on Zulip as there was a bit of a debate about how to package this API appropriately. I had deferred until some of the easier PRs were done :-)

kim-em

A few minor suggestions (on top of Jireh's structural ones, which I agree with).

Also: line 221 has a stray semicolon after by_cases hp : p = 0;.

Mathlib/Analysis/Polynomial/MahlerMeasure.lean

khwilson · 2026-04-03T13:35:35Z

-awaiting-author

j-loreaux

maintainer delegate

Mathlib/Analysis/Polynomial/MahlerMeasure.lean

github-actions · 2026-04-03T16:04:07Z

🚀 Pull request has been placed on the maintainer queue by j-loreaux.

khwilson · 2026-04-03T20:55:58Z

Cleaned up some extra have s that were unnecessary with the dot notation being accessible

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 Jan 1, 2026

plp127 reviewed Jan 1, 2026

View reviewed changes

Mathlib/Analysis/Polynomial/MahlerMeasure.lean Outdated Show resolved Hide resolved

Update Mathlib/Analysis/Polynomial/MahlerMeasure.lean

8e34373

Co-authored-by: Aaron Liu <[email protected]>

vlad902 reviewed Jan 2, 2026

View reviewed changes

khwilson and others added 3 commits January 1, 2026 19:16

Update Mathlib/Analysis/Polynomial/MahlerMeasure.lean

796e094

Co-authored-by: Vlad Tsyrklevich <[email protected]>

Update Mathlib/Analysis/Polynomial/MahlerMeasure.lean

fa38f9f

Co-authored-by: Vlad Tsyrklevich <[email protected]>

Update Mathlib/Analysis/Polynomial/MahlerMeasure.lean

31e0ace

Co-authored-by: Vlad Tsyrklevich <[email protected]>

khwilson added 2 commits January 2, 2026 14:17

add deprecation

ffa2a78

Merge branch 'master' into extend-mahler-measure

597f86b

vlad902 reviewed Jan 2, 2026

View reviewed changes

khwilson and others added 6 commits January 3, 2026 10:44

Update Mathlib/Analysis/Polynomial/MahlerMeasure.lean

a3f90a1

Co-authored-by: Vlad Tsyrklevich <[email protected]>

Update Mathlib/Analysis/Polynomial/MahlerMeasure.lean

8de2fb3

Co-authored-by: Vlad Tsyrklevich <[email protected]>

Update Mathlib/Analysis/Polynomial/MahlerMeasure.lean

96beaf9

Co-authored-by: Vlad Tsyrklevich <[email protected]>

Update Mathlib/Analysis/Polynomial/MahlerMeasure.lean

5206394

Co-authored-by: Vlad Tsyrklevich <[email protected]>

Update MahlerMeasure.lean

5be68bb

Add a comment on the definition of `mahlerMeasure'`

[pre-commit.ci lite] apply automatic fixes

8ad70a2

joneugster added the t-analysis Analysis (normed *, calculus) label Feb 1, 2026

khwilson added 2 commits February 10, 2026 16:01

Merge branch 'master' into extend-mahler-measure

6cd28c3

deal with deprecations

48129cf

j-loreaux reviewed Feb 10, 2026

View reviewed changes

Mathlib/Analysis/Polynomial/MahlerMeasure.lean Outdated Show resolved Hide resolved

Mathlib/Analysis/Polynomial/MahlerMeasure.lean Outdated Show resolved Hide resolved

j-loreaux added the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 10, 2026

kim-em reviewed Mar 30, 2026

View reviewed changes

khwilson added 2 commits March 31, 2026 21:31

Merge branch 'master' into extend-mahler-measure

ab8a361

fixing comments

73a77f1

Merge branch 'master' into extend-mahler-measure

088c6ae

github-actions bot removed the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 3, 2026

j-loreaux reviewed Apr 3, 2026

View reviewed changes

mathlib-triage bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Apr 3, 2026

further cleaning and comments from j-loreaux

b7beac8

Merge branch 'master' into extend-mahler-measure

7494643

Conversation

khwilson commented Jan 1, 2026

Uh oh!

github-actions bot commented Jan 1, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 5fbb6779b0

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

khwilson commented Jan 2, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

j-loreaux commented Feb 10, 2026

Uh oh!

khwilson commented Feb 10, 2026

Uh oh!

j-loreaux left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

khwilson commented Feb 10, 2026

Uh oh!

kim-em left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

khwilson commented Apr 3, 2026

Uh oh!

j-loreaux left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

github-actions bot commented Apr 3, 2026

Uh oh!

khwilson commented Apr 3, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

github-actions bot commented Jan 1, 2026 •

edited

Loading