From 33694cd54955e197fa291a2a63adf57f56082c49 Mon Sep 17 00:00:00 2001
From: fbarroero <fbarroero@gmail.com>
Date: Sun, 19 Oct 2025 16:45:46 +0200
Subject: [PATCH 1/3] 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 <fbarroero@gmail.com>
Date: Sun, 19 Oct 2025 17:07:21 +0200
Subject: [PATCH 2/3] 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 e46ff3236dea00a561b62fa14e3c5079a608a12b Mon Sep 17 00:00:00 2001
From: fbarroero <fbarroero@gmail.com>
Date: Tue, 21 Oct 2025 18:55:44 +0200
Subject: [PATCH 3/3] implement suggestions

---
 .../BigOperators/Group/Multiset/Defs.lean     |  4 +++
 .../Analysis/SpecialFunctions/Log/Basic.lean  | 26 ++++++++++++-------
 2 files changed, 21 insertions(+), 9 deletions(-)

diff --git a/Mathlib/Algebra/BigOperators/Group/Multiset/Defs.lean b/Mathlib/Algebra/BigOperators/Group/Multiset/Defs.lean
index d67670a782ee09..38310197b6233f 100644
--- a/Mathlib/Algebra/BigOperators/Group/Multiset/Defs.lean
+++ b/Mathlib/Algebra/BigOperators/Group/Multiset/Defs.lean
@@ -57,6 +57,10 @@ theorem prod_toList (s : Multiset M) : s.toList.prod = s.prod := by
   conv_rhs => rw [← coe_toList s]
   rw [prod_coe]
 
+@[to_additive (attr := simp, grind =)]
+theorem prod_map_toList (s : Multiset ι) (f : ι → M) : (s.toList.map f).prod = (s.map f).prod := by
+  rw [← Multiset.prod_coe, ← Multiset.map_coe, coe_toList]
+
 @[to_additive (attr := simp, grind =)]
 theorem prod_zero : @prod M _ 0 = 1 :=
   rfl
diff --git a/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean b/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
index fe11373e9416db..52f5a0bba0f01d 100644
--- a/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
@@ -363,19 +363,27 @@ 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' {α : 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 =>
+open List in
+lemma log_list_prod {l : List ℝ} (h : ∀ x ∈ l, x ≠ 0) :
+    log l.prod = (l.map (fun x ↦ log x)).sum := by
+  induction l with
+  | nil => simp
+  | cons a l 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]
+    have : l.prod ≠ 0 := by grind [prod_ne_zero]
+    rw [log_mul h.1 this, add_right_inj, ih]
+
+open Multiset in
+lemma log_multiset_prod {s : Multiset ℝ} (h : ∀ x ∈ s, x ≠ 0) :
+    log s.prod = (s.map (fun x ↦ log x)).sum := by
+  rw [← prod_toList, log_list_prod (by simp_all), sum_map_toList]
 
+open Finset in
 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
+    log (∏ i ∈ s, f i) = ∑ i ∈ s, log (f i) := by
+  rw [← prod_map_toList, log_list_prod (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) :=