From 7b9f4c4411e9a951e6cd8d62b45b57e55cc983bf Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Tue, 19 May 2026 10:06:18 +0200 Subject: [PATCH 1/2] Update PosLog.lean --- Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean b/Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean index afeed57a6af872..d2719b295175fe 100644 --- a/Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean +++ b/Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean @@ -157,8 +157,6 @@ theorem posLog_prod {α : Type*} (s : Finset α) (f : α → ℝ) : ## Estimates for Sums -/ --- TODO: non-terminal simp followed by positivity -set_option linter.flexible false in /-- Estimate for `log⁺` of a sum. See `Real.posLog_add` for a variant involving just two summands. -/ theorem posLog_sum {α : Type*} (s : Finset α) (f : α → ℝ) : @@ -176,7 +174,7 @@ theorem posLog_sum {α : Type*} (s : Finset α) (f : α → ℝ) : apply monotoneOn_posLog (by simp) (by simp [Finset.sum_nonneg]) simp [Finset.abs_sum_le_sum_abs] _ ≤ log⁺ (∑ t ∈ s, |f t_max|) := by - apply monotoneOn_posLog (by simp [Finset.sum_nonneg]) (by simp; positivity) + apply monotoneOn_posLog (by simp [Finset.sum_nonneg]) (by aesop) apply Finset.sum_le_sum (fun i ih ↦ ht_max.2 i ih) _ = log⁺ (s.card * |f t_max|) := by simp [Finset.sum_const] From 632e3075c516fa750cab1ffeb3de766fdd78f2fd Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Tue, 19 May 2026 12:46:29 +0200 Subject: [PATCH 2/2] Update Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com> --- Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean b/Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean index d2719b295175fe..1d10fdb63a1995 100644 --- a/Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean +++ b/Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean @@ -174,7 +174,7 @@ theorem posLog_sum {α : Type*} (s : Finset α) (f : α → ℝ) : apply monotoneOn_posLog (by simp) (by simp [Finset.sum_nonneg]) simp [Finset.abs_sum_le_sum_abs] _ ≤ log⁺ (∑ t ∈ s, |f t_max|) := by - apply monotoneOn_posLog (by simp [Finset.sum_nonneg]) (by aesop) + apply monotoneOn_posLog (by simp [Finset.sum_nonneg]) (by simp [mul_nonneg]) apply Finset.sum_le_sum (fun i ih ↦ ht_max.2 i ih) _ = log⁺ (s.card * |f t_max|) := by simp [Finset.sum_const]