From a96955c67607fbfe429e8452bc88ff62ea4690ea Mon Sep 17 00:00:00 2001 From: fbarroero Date: Tue, 14 Oct 2025 16:25:23 +0200 Subject: [PATCH 01/11] First commit --- .../Analysis/Polynomial/MahlerMeasure.lean | 152 +++++++++++++++++- .../Analysis/SpecialFunctions/Log/Basic.lean | 20 ++- 2 files changed, 165 insertions(+), 7 deletions(-) diff --git a/Mathlib/Analysis/Polynomial/MahlerMeasure.lean b/Mathlib/Analysis/Polynomial/MahlerMeasure.lean index a0f458219a05ed..a6c769cd703d0f 100644 --- a/Mathlib/Analysis/Polynomial/MahlerMeasure.lean +++ b/Mathlib/Analysis/Polynomial/MahlerMeasure.lean @@ -4,10 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Barroero -/ +import Mathlib.Algebra.Lie.OfAssociative import Mathlib.Analysis.Analytic.Polynomial import Mathlib.Analysis.CStarAlgebra.Classes -import Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic -import Mathlib.MeasureTheory.Integral.CircleAverage +import Mathlib.Analysis.Complex.JensenFormula +import Mathlib.Analysis.Complex.Polynomial.Basic +import Mathlib.RingTheory.SimpleRing.Principal /-! # Mahler measure of complex polynomials @@ -141,4 +143,150 @@ theorem logMahlerMeasure_mul_eq_add_logMahelerMeasure {p q : ℂ[X]} (hpq : p * (p * q).logMahlerMeasure = p.logMahlerMeasure + q.logMahlerMeasure := by simp_all [logMahlerMeasure_eq_log_MahlerMeasure, mahlerMeasure_mul, log_mul] + +theorem logMahlerMeasure_C_mul {a : ℂ} (ha : a ≠ 0) {p : ℂ[X]} (hp : p ≠ 0) : + (C a * p).logMahlerMeasure = log ‖a‖ + p.logMahlerMeasure := by + rw [logMahlerMeasure_mul_eq_add_logMahelerMeasure (by simp [ha, hp]), logMahlerMeasure_const] + +open MeromorphicOn Metric in +/-- The logarithmic Mahler measure of `X - C z` is `log⁺` of the absolute value of `z`. -/ +@[simp] +theorem logMahlerMeasure_X_sub_C (z : ℂ) : (X - C z).logMahlerMeasure = log⁺ ‖z‖ := by + by_cases hz₀ : z = 0 + · simp [hz₀, posLog_def] + have hmeroOn (U : Set ℂ) : MeromorphicOn (fun x ↦ x - z) U := + (MeromorphicOn.id).sub <| const z + have hmeroAt (u : ℂ) : MeromorphicAt (fun x ↦ x - z) u := hmeroOn (Eq u) u rfl + have hmeroBall : MeromorphicOn (fun x ↦ x - z) (closedBall 0 |1|) := + hmeroOn (closedBall 0 |1|) + have : MeromorphicOn (fun x ↦ (X - C z).eval x) (closedBall 0 |1|) := + (analyticOnNhd_id.aeval_polynomial (X - C z)).meromorphicOn + rw [logMahlerMeasure_def, circleAverage_log_norm zero_ne_one.symm this] + --get rid of the `meromorphicTrailingCoeffAt` + have : meromorphicTrailingCoeffAt (fun x ↦ (X - C z).eval x) 0 = -z := by + rw [(AnalyticAt.aeval_polynomial analyticAt_id (X - C z)).meromorphicTrailingCoeffAt_of_ne_zero + (by simp [hz₀])] + simp + rw [this] + simp only [eval_sub, eval_X, eval_C, zero_sub, norm_neg, one_mul, log_inv, mul_neg, log_one, + mul_zero, add_zero] + -- divisor computations + let B := closedBall (0 : ℂ) |1| + have hdiv0 {u : ℂ} (hu : u ≠ z) : divisor (fun x ↦ x - z) B u = 0 := by + by_cases hu' : u ∈ B + · rw [divisor_apply (hmeroOn B) hu', ← WithTop.untop₀_coe 0] + congr + rw [meromorphicOrderAt_eq_int_iff (hmeroAt u)] + use fun x ↦ x - z + simp only [zpow_zero, smul_eq_mul, one_mul, Filter.eventually_true, and_true] + exact ⟨analyticAt_id.fun_sub analyticAt_const, sub_ne_zero_of_ne hu⟩ + · simp_all + have hzdiv1 (h : z ∈ B) : (divisor (fun x ↦ x - z) B) z = 1 := by + simp_all only [eval_sub, eval_X, eval_C, divisor_apply] + rw [← WithTop.untop₀_coe 1] + congr + rw [meromorphicOrderAt_eq_int_iff (hmeroAt z)] + simp only [ne_eq, zpow_one, smul_eq_mul] + use fun x ↦ 1 + simpa using analyticAt_const + rw [← finsum_mem_support] + --separate cases depending on whether z in in the open ball 0 |1| or not + by_cases hzBall : z ∈ ball 0 |1|; + · have : ‖z‖ < 1 := by rwa [mem_ball, dist_zero_right, abs_one] at hzBall + have : ‖z‖ ≤ 1 := le_of_lt this + have hzcb : z ∈ B := Set.mem_of_mem_of_subset hzBall ball_subset_closedBall + + have : (fun u ↦ -((divisor (fun x ↦ x - z) (closedBall 0 |1|) u) * log ‖u‖)).support = {z} := by + rw [Function.support_eq_iff] + constructor + · simp only [ne_eq, neg_eq_zero, mul_eq_zero, Int.cast_eq_zero, log_eq_zero, norm_eq_zero] + grind [norm_nonneg, ne_of_lt] + · intro _ hu + rw [Set.mem_singleton_iff] at hu + rw [hdiv0 hu] + simp + simp only [this, Set.mem_singleton_iff, finsum_cond_eq_left] + rw [hzdiv1 hzcb] + grind [log_nonpos , norm_nonneg, posLog_def] + · have h1lez : 1 ≤ ‖z‖ := by grind [mem_ball, dist_zero_right, abs_one] + have : (fun u ↦ -((divisor (fun x ↦ x - z) (closedBall 0 |1|) u) * log ‖u‖)).support = ∅ := by + rw [Function.support_eq_empty_iff] + ext x + simp only [Pi.zero_apply, neg_eq_zero, mul_eq_zero, Int.cast_eq_zero, log_eq_zero, + norm_eq_zero] + rw [or_iff_not_imp_right] + simp only [not_or, and_imp] + intro _ h _ + by_cases hx : x = z + · rw [hx] at h ⊢ + apply Function.locallyFinsuppWithin.apply_eq_zero_of_notMem + (divisor (fun x ↦ x - z) (closedBall 0 |1|)) + grind [abs_one, mem_closedBall, dist_zero_right] + · exact hdiv0 hx + simp [this, posLog_eq_log_max_one <| norm_nonneg z, h1lez] + +@[simp] +theorem logMahlerMeasure_X_add_C (z : ℂ) : (X + C z).logMahlerMeasure = log⁺ ‖z‖ := by + simp [← sub_neg_eq_add, ← map_neg] + +theorem logMahlerMeasure_C_mul_X_add_C {a : ℂ} (b : ℂ) (ha : a ≠ 0) : + (C a * X + C b).logMahlerMeasure = log ‖a‖ + log⁺ ‖a⁻¹ * b‖ := by + rw [show C a * X + C b = C a * (X + C (a⁻¹ * b)) by simp [mul_add, ← map_mul, ha], + logMahlerMeasure_C_mul ha (X_add_C_ne_zero (a⁻¹ * b)), logMahlerMeasure_X_add_C] + +theorem logMahlerMeasure_degree_eq_one {p : ℂ[X]} (h : p.degree = 1) : p.logMahlerMeasure = + log ‖p.coeff 1‖ + log⁺ ‖(p.coeff 1)⁻¹ * p.coeff 0‖ := by + rw [eq_X_add_C_of_degree_le_one (le_of_eq h)] + simp [logMahlerMeasure_C_mul_X_add_C _ (show p.coeff 1 ≠ 0 by exact coeff_ne_zero_of_eq_degree h)] + +/-- The Mahler measure of `X - C z` equals `max 1 ‖z‖`. -/ +@[simp] +theorem mahlerMeasure_X_sub_C (z : ℂ) : (X - C z).mahlerMeasure = max 1 ‖z‖ := by + have := logMahlerMeasure_X_sub_C z + rw [logMahlerMeasure_eq_log_MahlerMeasure] at this + apply_fun exp at this + rwa [posLog_eq_log_max_one (norm_nonneg z), + exp_log (mahlerMeasure_pos_of_ne_zero <| X_sub_C_ne_zero z), + exp_log (lt_of_lt_of_le zero_lt_one <| le_max_left 1 ‖z‖)] at this + +@[simp] +theorem mahlerMeasure_X_add_C (z : ℂ) : (X + C z).mahlerMeasure = max 1 ‖z‖ := by + simp [← sub_neg_eq_add, ← map_neg] + +theorem mahlerMeasure_C_mul_X_add_C {a : ℂ} (b : ℂ) (ha : a ≠ 0) : + (C a * X + C b).mahlerMeasure = ‖a‖ * max 1 ‖a⁻¹ * b‖ := by + simp [show C a * X + C b = C a * (X + C (a⁻¹ * b)) by simp [mul_add, ← map_mul, ha], + mahlerMeasure_mul, -map_mul] + +theorem mahlerMeasure_degree_eq_one {p : ℂ[X]} (h : p.degree = 1) : p.mahlerMeasure = + ‖p.coeff 1‖ * max 1 ‖(p.coeff 1)⁻¹ * p.coeff 0‖ := by + rw [eq_X_add_C_of_degree_le_one (le_of_eq h)] + simp [mahlerMeasure_C_mul_X_add_C _ (show p.coeff 1 ≠ 0 by exact coeff_ne_zero_of_eq_degree h)] + +/-- The logarithmic Mahler measure of `p` is the `log` of the absolute value of its leading + coefficient plus the sum of the `log`s of the absolute values of its roots lying outside the unit + disk. -/ +theorem logMahlerMeasure_eq_log_leadingCoeff_add_sum_log_roots (p : ℂ[X]) : p.logMahlerMeasure = + log ‖p.leadingCoeff‖ + ((p.roots).map (fun a ↦ log⁺ ‖a‖)).sum := by + by_cases hp : p = 0 + · simp [hp] + have : ∀ x ∈ Multiset.map (fun x ↦ max 1 ‖x‖) p.roots, x ≠ 0 := by grind [Multiset.mem_map] + nth_rw 1 [eq_prod_roots_of_splits_id (IsAlgClosed.splits p)] + rw [logMahlerMeasure_mul_eq_add_logMahelerMeasure (by simp [hp, X_sub_C_ne_zero])] + simp [posLog_eq_log_max_one,logMahlerMeasure_eq_log_MahlerMeasure, + prod_mahlerMeasure_eq_mahlerMeasure_prod, log_prod_eq_sum_log this] + +/-- The Mahler measure of `p` is the the absolute value of its leading coefficient times the product + absolute values of its roots lying outside the unit disk. -/ +theorem mahlerMeasure_eq_leadingCoeff_mul_prod_roots (p : ℂ[X]) : p.mahlerMeasure = + ‖p.leadingCoeff‖ * ((p.roots).map (fun a ↦ max 1 ‖a‖)).prod := by + by_cases hp : p = 0; + · simp [hp] + have := logMahlerMeasure_eq_log_leadingCoeff_add_sum_log_roots p + rw [logMahlerMeasure_eq_log_MahlerMeasure] at this + apply_fun exp at this + rw [exp_add, exp_log <| mahlerMeasure_pos_of_ne_zero hp, + exp_log <|norm_pos_iff.mpr <| leadingCoeff_ne_zero.mpr hp] at this + simp [this, exp_multiset_sum, posLog_eq_log_max_one, exp_log] + end Polynomial diff --git a/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean b/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean index 562fb9fdca2b1d..b6facc8c63fb23 100644 --- a/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean +++ b/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean @@ -363,13 +363,23 @@ theorem continuousAt_log_iff : ContinuousAt log x ↔ x ≠ 0 := by exact not_tendsto_nhds_of_tendsto_atBot tendsto_log_nhdsNE_zero _ <| h.tendsto.mono_left nhdsWithin_le_nhds +open Multiset in +lemma log_prod_eq_sum_log {s : Multiset ℝ} (h : ∀ x ∈ s, x ≠ 0) : + log s.prod = (s.map (fun x ↦ log x)).sum := by + induction s using Multiset.induction_on with + | empty => simp + | cons a s ih => + simp_all only [ne_eq, mem_cons, or_true, not_false_eq_true, implies_true, forall_const, + forall_eq_or_imp, prod_cons, map_cons, sum_cons] + have : s.prod ≠ 0 := by + apply prod_ne_zero + grind + rw [log_mul h.1 this, add_right_inj, ih] + theorem log_prod {α : Type*} (s : Finset α) (f : α → ℝ) (hf : ∀ x ∈ s, f x ≠ 0) : log (∏ i ∈ s, f i) = ∑ i ∈ s, log (f i) := by - induction s using Finset.cons_induction_on with - | empty => simp - | cons a s ha ih => - rw [Finset.forall_mem_cons] at hf - simp [ih hf.2, log_mul hf.1 (Finset.prod_ne_zero_iff.2 hf.2)] + rw [Finset.prod, log_prod_eq_sum_log (by simp_all)] + simp protected theorem _root_.Finsupp.log_prod {α β : Type*} [Zero β] (f : α →₀ β) (g : α → β → ℝ) (hg : ∀ a, g a (f a) = 0 → f a = 0) : log (f.prod g) = f.sum fun a b ↦ log (g a b) := From 284c048ddf8c23130f7ba503664e3b67f179cf13 Mon Sep 17 00:00:00 2001 From: fbarroero Date: Tue, 14 Oct 2025 16:29:54 +0200 Subject: [PATCH 02/11] erase space --- Mathlib/Analysis/Polynomial/MahlerMeasure.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Mathlib/Analysis/Polynomial/MahlerMeasure.lean b/Mathlib/Analysis/Polynomial/MahlerMeasure.lean index a6c769cd703d0f..958604c3760b0a 100644 --- a/Mathlib/Analysis/Polynomial/MahlerMeasure.lean +++ b/Mathlib/Analysis/Polynomial/MahlerMeasure.lean @@ -195,7 +195,6 @@ theorem logMahlerMeasure_X_sub_C (z : ℂ) : (X - C z).logMahlerMeasure = log⁺ · have : ‖z‖ < 1 := by rwa [mem_ball, dist_zero_right, abs_one] at hzBall have : ‖z‖ ≤ 1 := le_of_lt this have hzcb : z ∈ B := Set.mem_of_mem_of_subset hzBall ball_subset_closedBall - have : (fun u ↦ -((divisor (fun x ↦ x - z) (closedBall 0 |1|) u) * log ‖u‖)).support = {z} := by rw [Function.support_eq_iff] constructor From 0b525f95f0bd98069db2b2c16346e1997de9c4db Mon Sep 17 00:00:00 2001 From: fbarroero Date: Tue, 14 Oct 2025 20:22:47 +0200 Subject: [PATCH 03/11] Esthetics --- Mathlib/Analysis/Polynomial/MahlerMeasure.lean | 15 +++++---------- 1 file changed, 5 insertions(+), 10 deletions(-) diff --git a/Mathlib/Analysis/Polynomial/MahlerMeasure.lean b/Mathlib/Analysis/Polynomial/MahlerMeasure.lean index 958604c3760b0a..d03e65a5b5414e 100644 --- a/Mathlib/Analysis/Polynomial/MahlerMeasure.lean +++ b/Mathlib/Analysis/Polynomial/MahlerMeasure.lean @@ -149,16 +149,14 @@ theorem logMahlerMeasure_C_mul {a : ℂ} (ha : a ≠ 0) {p : ℂ[X]} (hp : p ≠ rw [logMahlerMeasure_mul_eq_add_logMahelerMeasure (by simp [ha, hp]), logMahlerMeasure_const] open MeromorphicOn Metric in -/-- The logarithmic Mahler measure of `X - C z` is `log⁺` of the absolute value of `z`. -/ +/-- The logarithmic Mahler measure of `X - C z` is the `log⁺` of the absolute value of `z`. -/ @[simp] theorem logMahlerMeasure_X_sub_C (z : ℂ) : (X - C z).logMahlerMeasure = log⁺ ‖z‖ := by by_cases hz₀ : z = 0 · simp [hz₀, posLog_def] - have hmeroOn (U : Set ℂ) : MeromorphicOn (fun x ↦ x - z) U := - (MeromorphicOn.id).sub <| const z + have hmeroOn (U : Set ℂ) : MeromorphicOn (fun x ↦ x - z) U := MeromorphicOn.id.sub <| const z have hmeroAt (u : ℂ) : MeromorphicAt (fun x ↦ x - z) u := hmeroOn (Eq u) u rfl - have hmeroBall : MeromorphicOn (fun x ↦ x - z) (closedBall 0 |1|) := - hmeroOn (closedBall 0 |1|) + have hmeroBall : MeromorphicOn (fun x ↦ x - z) (closedBall 0 |1|) := hmeroOn (closedBall 0 |1|) have : MeromorphicOn (fun x ↦ (X - C z).eval x) (closedBall 0 |1|) := (analyticOnNhd_id.aeval_polynomial (X - C z)).meromorphicOn rw [logMahlerMeasure_def, circleAverage_log_norm zero_ne_one.symm this] @@ -186,7 +184,6 @@ theorem logMahlerMeasure_X_sub_C (z : ℂ) : (X - C z).logMahlerMeasure = log⁺ rw [← WithTop.untop₀_coe 1] congr rw [meromorphicOrderAt_eq_int_iff (hmeroAt z)] - simp only [ne_eq, zpow_one, smul_eq_mul] use fun x ↦ 1 simpa using analyticAt_const rw [← finsum_mem_support] @@ -211,10 +208,8 @@ theorem logMahlerMeasure_X_sub_C (z : ℂ) : (X - C z).logMahlerMeasure = log⁺ have : (fun u ↦ -((divisor (fun x ↦ x - z) (closedBall 0 |1|) u) * log ‖u‖)).support = ∅ := by rw [Function.support_eq_empty_iff] ext x - simp only [Pi.zero_apply, neg_eq_zero, mul_eq_zero, Int.cast_eq_zero, log_eq_zero, - norm_eq_zero] - rw [or_iff_not_imp_right] - simp only [not_or, and_imp] + simp only [Pi.ofNat_apply, neg_eq_zero, mul_eq_zero, Int.cast_eq_zero, log_eq_zero, + norm_eq_zero, or_iff_not_imp_right, Classical.not_imp, and_imp] intro _ h _ by_cases hx : x = z · rw [hx] at h ⊢ From 471a79ce9c8f9fd1d2b29265ba8be53a35f82387 Mon Sep 17 00:00:00 2001 From: fbarroero Date: Tue, 14 Oct 2025 20:34:19 +0200 Subject: [PATCH 04/11] doc --- Mathlib/Analysis/Polynomial/MahlerMeasure.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/Analysis/Polynomial/MahlerMeasure.lean b/Mathlib/Analysis/Polynomial/MahlerMeasure.lean index d03e65a5b5414e..98e3d9e478cb19 100644 --- a/Mathlib/Analysis/Polynomial/MahlerMeasure.lean +++ b/Mathlib/Analysis/Polynomial/MahlerMeasure.lean @@ -257,7 +257,7 @@ theorem mahlerMeasure_degree_eq_one {p : ℂ[X]} (h : p.degree = 1) : p.mahlerMe rw [eq_X_add_C_of_degree_le_one (le_of_eq h)] simp [mahlerMeasure_C_mul_X_add_C _ (show p.coeff 1 ≠ 0 by exact coeff_ne_zero_of_eq_degree h)] -/-- The logarithmic Mahler measure of `p` is the `log` of the absolute value of its leading +/-- The logarithmic Mahler measure of a polynomial is the `log` of the absolute value of its leading coefficient plus the sum of the `log`s of the absolute values of its roots lying outside the unit disk. -/ theorem logMahlerMeasure_eq_log_leadingCoeff_add_sum_log_roots (p : ℂ[X]) : p.logMahlerMeasure = @@ -270,8 +270,8 @@ theorem logMahlerMeasure_eq_log_leadingCoeff_add_sum_log_roots (p : ℂ[X]) : p. simp [posLog_eq_log_max_one,logMahlerMeasure_eq_log_MahlerMeasure, prod_mahlerMeasure_eq_mahlerMeasure_prod, log_prod_eq_sum_log this] -/-- The Mahler measure of `p` is the the absolute value of its leading coefficient times the product - absolute values of its roots lying outside the unit disk. -/ +/-- The Mahler measure of a polynomial is the the absolute value of its leading coefficient times + the product of the absolute values of its roots lying outside the unit disk. -/ theorem mahlerMeasure_eq_leadingCoeff_mul_prod_roots (p : ℂ[X]) : p.mahlerMeasure = ‖p.leadingCoeff‖ * ((p.roots).map (fun a ↦ max 1 ‖a‖)).prod := by by_cases hp : p = 0; From 1d88466d6c3adb9b4822de8ab132012152dcf9ba Mon Sep 17 00:00:00 2001 From: fbarroero Date: Sun, 19 Oct 2025 12:31:49 +0200 Subject: [PATCH 05/11] log_prod_eq_sum_log with function --- .../Analysis/SpecialFunctions/Log/Basic.lean | 18 +++++++----------- 1 file changed, 7 insertions(+), 11 deletions(-) diff --git a/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean b/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean index fe5d7a42ad7b79..4a93796e419db1 100644 --- a/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean +++ b/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean @@ -364,22 +364,18 @@ theorem continuousAt_log_iff : ContinuousAt log x ↔ x ≠ 0 := by h.tendsto.mono_left nhdsWithin_le_nhds open Multiset in -lemma log_prod_eq_sum_log {s : Multiset ℝ} (h : ∀ x ∈ s, x ≠ 0) : - log s.prod = (s.map (fun x ↦ log x)).sum := by +lemma log_prod_eq_sum_log {α : Type*} {s : Multiset α} {f : α → ℝ} (hf : ∀ x ∈ s, f x ≠ 0) : + log (s.map f).prod = (s.map (fun x ↦ log (f x))).sum := by induction s using Multiset.induction_on with | empty => simp | cons a s ih => - simp_all only [ne_eq, mem_cons, or_true, not_false_eq_true, implies_true, forall_const, - forall_eq_or_imp, prod_cons, map_cons, sum_cons] - have : s.prod ≠ 0 := by - apply prod_ne_zero - grind - rw [log_mul h.1 this, add_right_inj, ih] + simp_all only [ne_eq, mem_cons, or_true, not_false_eq_true, forall_const, forall_eq_or_imp, + prod_cons, map_cons, sum_cons] + have : (s.map f).prod ≠ 0 := by simpa using hf.2 + rw [log_mul hf.1 this, add_right_inj, ih] theorem log_prod {α : Type*} (s : Finset α) (f : α → ℝ) (hf : ∀ x ∈ s, f x ≠ 0) : - log (∏ i ∈ s, f i) = ∑ i ∈ s, log (f i) := by - rw [Finset.prod, log_prod_eq_sum_log (by simp_all)] - simp + log (∏ i ∈ s, f i) = ∑ i ∈ s, log (f i) := log_prod_eq_sum_log hf protected theorem _root_.Finsupp.log_prod {α β : Type*} [Zero β] (f : α →₀ β) (g : α → β → ℝ) (hg : ∀ a, g a (f a) = 0 → f a = 0) : log (f.prod g) = f.sum fun a b ↦ log (g a b) := From 33694cd54955e197fa291a2a63adf57f56082c49 Mon Sep 17 00:00:00 2001 From: fbarroero Date: Sun, 19 Oct 2025 16:45:46 +0200 Subject: [PATCH 06/11] First commit --- .../Meromorphic/FactorizedRational.lean | 4 ++-- .../Analysis/SpecialFunctions/Log/Basic.lean | 20 ++++++++++++------- .../CanonicalEmbedding/NormLeOne.lean | 2 +- Mathlib/Probability/Moments/Basic.lean | 2 +- 4 files changed, 17 insertions(+), 11 deletions(-) diff --git a/Mathlib/Analysis/Meromorphic/FactorizedRational.lean b/Mathlib/Analysis/Meromorphic/FactorizedRational.lean index 0f8f3f5e155e90..f780b25956d74c 100644 --- a/Mathlib/Analysis/Meromorphic/FactorizedRational.lean +++ b/Mathlib/Analysis/Meromorphic/FactorizedRational.lean @@ -253,7 +253,7 @@ theorem log_norm_meromorphicTrailingCoeffAt {d : 𝕜 → ℤ} {x : 𝕜} (h : d · rw [h] simp_all · simp_all [zpow_ne_zero, sub_ne_zero] - rw [norm_prod, log_prod _ _ this] + rw [norm_prod, log_prod this] have : (fun u ↦ (d u) * log ‖x - u‖).support ⊆ h.toFinset := by intro u contrapose @@ -373,7 +373,7 @@ theorem MeromorphicOn.extract_zeros_poles_log {f g : 𝕜 → E} {D : Function.l apply ne_of_apply_ne D rwa [h₂z] simp only [Pi.smul_apply', Finset.prod_apply, Pi.pow_apply, norm_smul, norm_prod, norm_zpow] - rw [log_mul (Finset.prod_ne_zero_iff.2 this) (by simp [hg ⟨z, h₃z⟩]), log_prod _ _ this] + rw [log_mul (Finset.prod_ne_zero_iff.2 this) (by simp [hg ⟨z, h₃z⟩]), log_prod' this] simp [log_zpow] open Classical in diff --git a/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean b/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean index d506ba37ca1061..fe11373e9416db 100644 --- a/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean +++ b/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean @@ -363,17 +363,23 @@ theorem continuousAt_log_iff : ContinuousAt log x ↔ x ≠ 0 := by exact not_tendsto_nhds_of_tendsto_atBot tendsto_log_nhdsNE_zero _ <| h.tendsto.mono_left nhdsWithin_le_nhds -theorem log_prod {α : Type*} (s : Finset α) (f : α → ℝ) (hf : ∀ x ∈ s, f x ≠ 0) : - log (∏ i ∈ s, f i) = ∑ i ∈ s, log (f i) := by - induction s using Finset.cons_induction_on with +open Multiset in +lemma log_prod' {α : Type*} {s : Multiset α} {f : α → ℝ} (hf : ∀ x ∈ s, f x ≠ 0) : + log (s.map f).prod = (s.map (fun x ↦ log (f x))).sum := by + induction s using Multiset.induction_on with | empty => simp - | cons a s ha ih => - rw [Finset.forall_mem_cons] at hf - simp [ih hf.2, log_mul hf.1 (Finset.prod_ne_zero_iff.2 hf.2)] + | cons a s ih => + simp_all only [ne_eq, mem_cons, or_true, not_false_eq_true, forall_const, forall_eq_or_imp, + prod_cons, map_cons, sum_cons] + have : (s.map f).prod ≠ 0 := by simpa using hf.2 + rw [log_mul hf.1 this, add_right_inj, ih] + +theorem log_prod {α : Type*} {s : Finset α} {f : α → ℝ} (hf : ∀ x ∈ s, f x ≠ 0) : + log (∏ i ∈ s, f i) = ∑ i ∈ s, log (f i) := log_prod' hf protected theorem _root_.Finsupp.log_prod {α β : Type*} [Zero β] (f : α →₀ β) (g : α → β → ℝ) (hg : ∀ a, g a (f a) = 0 → f a = 0) : log (f.prod g) = f.sum fun a b ↦ log (g a b) := - log_prod _ _ fun _x hx h₀ ↦ Finsupp.mem_support_iff.1 hx <| hg _ h₀ + log_prod fun _x hx h₀ ↦ Finsupp.mem_support_iff.1 hx <| hg _ h₀ theorem log_nat_eq_sum_factorization (n : ℕ) : log n = n.factorization.sum fun p t => t * log p := by diff --git a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLeOne.lean b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLeOne.lean index a8a5f98f97d28c..14bb9a63a62fb8 100644 --- a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLeOne.lean +++ b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLeOne.lean @@ -300,7 +300,7 @@ theorem logMap_expMap {x : realSpace K} theorem sum_expMap_symm_apply {x : K} (hx : x ≠ 0) : ∑ w : InfinitePlace K, expMap.symm ((normAtAllPlaces (mixedEmbedding K x))) w = Real.log (|Algebra.norm ℚ x| : ℚ) := by - simp_rw [← prod_eq_abs_norm, Real.log_prod _ _ (fun _ _ ↦ pow_ne_zero _ ((map_ne_zero _).mpr hx)), + simp_rw [← prod_eq_abs_norm, Real.log_prod (fun _ _ ↦ pow_ne_zero _ ((map_ne_zero _).mpr hx)), Real.log_pow, expMap_symm_apply, normAtAllPlaces_mixedEmbedding] /-- diff --git a/Mathlib/Probability/Moments/Basic.lean b/Mathlib/Probability/Moments/Basic.lean index 99c3e21a917e4d..d9a7735183a977 100644 --- a/Mathlib/Probability/Moments/Basic.lean +++ b/Mathlib/Probability/Moments/Basic.lean @@ -372,7 +372,7 @@ theorem iIndepFun.cgf_sum {X : ι → Ω → ℝ} cgf (∑ i ∈ s, X i) μ t = ∑ i ∈ s, cgf (X i) μ t := by have : IsProbabilityMeasure μ := h_indep.isProbabilityMeasure simp_rw [cgf] - rw [← log_prod _ _ fun j hj => ?_] + rw [← log_prod fun j hj => ?_] · rw [h_indep.mgf_sum h_meas] · exact (mgf_pos (h_int j hj)).ne' From 48638da79ec788ce0b1a1c9c88c458e2f2d0b2a5 Mon Sep 17 00:00:00 2001 From: fbarroero Date: Sun, 19 Oct 2025 17:07:21 +0200 Subject: [PATCH 07/11] fix --- Mathlib/Analysis/Meromorphic/FactorizedRational.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Analysis/Meromorphic/FactorizedRational.lean b/Mathlib/Analysis/Meromorphic/FactorizedRational.lean index f780b25956d74c..dbab9e79b8c657 100644 --- a/Mathlib/Analysis/Meromorphic/FactorizedRational.lean +++ b/Mathlib/Analysis/Meromorphic/FactorizedRational.lean @@ -373,7 +373,7 @@ theorem MeromorphicOn.extract_zeros_poles_log {f g : 𝕜 → E} {D : Function.l apply ne_of_apply_ne D rwa [h₂z] simp only [Pi.smul_apply', Finset.prod_apply, Pi.pow_apply, norm_smul, norm_prod, norm_zpow] - rw [log_mul (Finset.prod_ne_zero_iff.2 this) (by simp [hg ⟨z, h₃z⟩]), log_prod' this] + rw [log_mul (Finset.prod_ne_zero_iff.2 this) (by simp [hg ⟨z, h₃z⟩]), log_prod this] simp [log_zpow] open Classical in From d0c348b5bf11de88f8ce323bc116367f38f77922 Mon Sep 17 00:00:00 2001 From: fbarroero Date: Sun, 19 Oct 2025 17:25:22 +0200 Subject: [PATCH 08/11] log_prod' --- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean b/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean index 4a93796e419db1..fe11373e9416db 100644 --- a/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean +++ b/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean @@ -364,7 +364,7 @@ theorem continuousAt_log_iff : ContinuousAt log x ↔ x ≠ 0 := by h.tendsto.mono_left nhdsWithin_le_nhds open Multiset in -lemma log_prod_eq_sum_log {α : Type*} {s : Multiset α} {f : α → ℝ} (hf : ∀ x ∈ s, f x ≠ 0) : +lemma log_prod' {α : Type*} {s : Multiset α} {f : α → ℝ} (hf : ∀ x ∈ s, f x ≠ 0) : log (s.map f).prod = (s.map (fun x ↦ log (f x))).sum := by induction s using Multiset.induction_on with | empty => simp @@ -374,12 +374,12 @@ lemma log_prod_eq_sum_log {α : Type*} {s : Multiset α} {f : α → ℝ} (hf : have : (s.map f).prod ≠ 0 := by simpa using hf.2 rw [log_mul hf.1 this, add_right_inj, ih] -theorem log_prod {α : Type*} (s : Finset α) (f : α → ℝ) (hf : ∀ x ∈ s, f x ≠ 0) : - log (∏ i ∈ s, f i) = ∑ i ∈ s, log (f i) := log_prod_eq_sum_log hf +theorem log_prod {α : Type*} {s : Finset α} {f : α → ℝ} (hf : ∀ x ∈ s, f x ≠ 0) : + log (∏ i ∈ s, f i) = ∑ i ∈ s, log (f i) := log_prod' hf protected theorem _root_.Finsupp.log_prod {α β : Type*} [Zero β] (f : α →₀ β) (g : α → β → ℝ) (hg : ∀ a, g a (f a) = 0 → f a = 0) : log (f.prod g) = f.sum fun a b ↦ log (g a b) := - log_prod _ _ fun _x hx h₀ ↦ Finsupp.mem_support_iff.1 hx <| hg _ h₀ + log_prod fun _x hx h₀ ↦ Finsupp.mem_support_iff.1 hx <| hg _ h₀ theorem log_nat_eq_sum_factorization (n : ℕ) : log n = n.factorization.sum fun p t => t * log p := by From b35e64a4e6fac97413e1061b59a1446793f3edf1 Mon Sep 17 00:00:00 2001 From: fbarroero Date: Sun, 19 Oct 2025 17:39:33 +0200 Subject: [PATCH 09/11] fix --- Mathlib/Analysis/Polynomial/MahlerMeasure.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/Analysis/Polynomial/MahlerMeasure.lean b/Mathlib/Analysis/Polynomial/MahlerMeasure.lean index 98e3d9e478cb19..5a9e7cb0423ff9 100644 --- a/Mathlib/Analysis/Polynomial/MahlerMeasure.lean +++ b/Mathlib/Analysis/Polynomial/MahlerMeasure.lean @@ -264,11 +264,11 @@ theorem logMahlerMeasure_eq_log_leadingCoeff_add_sum_log_roots (p : ℂ[X]) : p. log ‖p.leadingCoeff‖ + ((p.roots).map (fun a ↦ log⁺ ‖a‖)).sum := by by_cases hp : p = 0 · simp [hp] - have : ∀ x ∈ Multiset.map (fun x ↦ max 1 ‖x‖) p.roots, x ≠ 0 := by grind [Multiset.mem_map] + have : ∀ x ∈ p.roots, max 1 ‖x‖ ≠ 0 := by grind nth_rw 1 [eq_prod_roots_of_splits_id (IsAlgClosed.splits p)] rw [logMahlerMeasure_mul_eq_add_logMahelerMeasure (by simp [hp, X_sub_C_ne_zero])] - simp [posLog_eq_log_max_one,logMahlerMeasure_eq_log_MahlerMeasure, - prod_mahlerMeasure_eq_mahlerMeasure_prod, log_prod_eq_sum_log this] + simp [posLog_eq_log_max_one, logMahlerMeasure_eq_log_MahlerMeasure, + prod_mahlerMeasure_eq_mahlerMeasure_prod, log_prod' this] /-- The Mahler measure of a polynomial is the the absolute value of its leading coefficient times the product of the absolute values of its roots lying outside the unit disk. -/ From fe7e2e35147122b7a32d6e0ff299c15ba381ca84 Mon Sep 17 00:00:00 2001 From: fbarroero Date: Thu, 23 Oct 2025 00:39:48 +0200 Subject: [PATCH 10/11] log_multiset_prod --- Mathlib/Analysis/Polynomial/MahlerMeasure.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Analysis/Polynomial/MahlerMeasure.lean b/Mathlib/Analysis/Polynomial/MahlerMeasure.lean index 5a9e7cb0423ff9..100c97886efed3 100644 --- a/Mathlib/Analysis/Polynomial/MahlerMeasure.lean +++ b/Mathlib/Analysis/Polynomial/MahlerMeasure.lean @@ -264,11 +264,11 @@ theorem logMahlerMeasure_eq_log_leadingCoeff_add_sum_log_roots (p : ℂ[X]) : p. log ‖p.leadingCoeff‖ + ((p.roots).map (fun a ↦ log⁺ ‖a‖)).sum := by by_cases hp : p = 0 · simp [hp] - have : ∀ x ∈ p.roots, max 1 ‖x‖ ≠ 0 := by grind + have : ∀ x ∈ Multiset.map (fun x ↦ max 1 ‖x‖) p.roots, x ≠ 0 := by grind [Multiset.mem_map] nth_rw 1 [eq_prod_roots_of_splits_id (IsAlgClosed.splits p)] rw [logMahlerMeasure_mul_eq_add_logMahelerMeasure (by simp [hp, X_sub_C_ne_zero])] simp [posLog_eq_log_max_one, logMahlerMeasure_eq_log_MahlerMeasure, - prod_mahlerMeasure_eq_mahlerMeasure_prod, log_prod' this] + prod_mahlerMeasure_eq_mahlerMeasure_prod, log_multiset_prod this] /-- The Mahler measure of a polynomial is the the absolute value of its leading coefficient times the product of the absolute values of its roots lying outside the unit disk. -/ From 5b5a8c6c46cb6f7170e1c931d6d384ef42111adf Mon Sep 17 00:00:00 2001 From: fbarroero Date: Thu, 23 Oct 2025 00:40:55 +0200 Subject: [PATCH 11/11] parethesis --- Mathlib/Analysis/Polynomial/MahlerMeasure.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Analysis/Polynomial/MahlerMeasure.lean b/Mathlib/Analysis/Polynomial/MahlerMeasure.lean index 100c97886efed3..fb2990adc48d74 100644 --- a/Mathlib/Analysis/Polynomial/MahlerMeasure.lean +++ b/Mathlib/Analysis/Polynomial/MahlerMeasure.lean @@ -261,7 +261,7 @@ theorem mahlerMeasure_degree_eq_one {p : ℂ[X]} (h : p.degree = 1) : p.mahlerMe coefficient plus the sum of the `log`s of the absolute values of its roots lying outside the unit disk. -/ theorem logMahlerMeasure_eq_log_leadingCoeff_add_sum_log_roots (p : ℂ[X]) : p.logMahlerMeasure = - log ‖p.leadingCoeff‖ + ((p.roots).map (fun a ↦ log⁺ ‖a‖)).sum := by + log ‖p.leadingCoeff‖ + (p.roots.map (fun a ↦ log⁺ ‖a‖)).sum := by by_cases hp : p = 0 · simp [hp] have : ∀ x ∈ Multiset.map (fun x ↦ max 1 ‖x‖) p.roots, x ≠ 0 := by grind [Multiset.mem_map] @@ -273,7 +273,7 @@ theorem logMahlerMeasure_eq_log_leadingCoeff_add_sum_log_roots (p : ℂ[X]) : p. /-- The Mahler measure of a polynomial is the the absolute value of its leading coefficient times the product of the absolute values of its roots lying outside the unit disk. -/ theorem mahlerMeasure_eq_leadingCoeff_mul_prod_roots (p : ℂ[X]) : p.mahlerMeasure = - ‖p.leadingCoeff‖ * ((p.roots).map (fun a ↦ max 1 ‖a‖)).prod := by + ‖p.leadingCoeff‖ * (p.roots.map (fun a ↦ max 1 ‖a‖)).prod := by by_cases hp : p = 0; · simp [hp] have := logMahlerMeasure_eq_log_leadingCoeff_add_sum_log_roots p