Commit 2026-03-11 01:46 82ff5788

feat(Mathlib/Analysis/Polynomial/MahlerMeasure): Mahler Measure estimate in terms of supNorm (#35280) The Mahler measure of a polynomial is bounded above by √(p.natDegree + 1) * p.supNorm. This is a tighter estimate than (p.natDegree + 1) * p.supNorm, which is implied by mahlerMeasure_le_sum_norm_coeff. AI Usage: Claude Code (Opus 4.6) provided first drafts for several sorries in the main calc block. Gemini Pro was used for one-off looks ups of lemma names like ae_restrict_iff'. The final code was edited by me.