Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 4 additions & 0 deletions Mathlib/Algebra/BigOperators/Group/Multiset/Defs.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 2 additions & 2 deletions Mathlib/Analysis/Meromorphic/FactorizedRational.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
28 changes: 21 additions & 7 deletions Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -363,17 +363,31 @@ 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) :
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 : 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) := 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 [← 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) :=
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
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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]

/--
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Probability/Moments/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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'

Expand Down