From 2178a08621d6d4540a4390227edb1ff3406a63d9 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Sun, 19 Oct 2025 23:28:29 +0100 Subject: [PATCH 1/2] chore(Analysis/SpecialFunctions/Log/PosLog): golf a proof using `grw` --- Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean b/Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean index 319774eb4c6ff1..5bec46db50e619 100644 --- a/Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean +++ b/Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean @@ -91,6 +91,11 @@ theorem monotoneOn_posLog : MonotoneOn log⁺ (Set.Ici 0) := by simp only [this, and_true, ge_iff_le] linarith +@[gcongr] +lemma posLog_le_posLog (x y : ℝ) (hx : 0 ≤ x) (hxy : x ≤ y) : + log⁺ x ≤ log⁺ y := + Real.monotoneOn_posLog hx (hx.trans hxy) hxy + /-! ## Estimates for Products -/ @@ -169,12 +174,6 @@ monotonicity of `log⁺` and the triangle inequality. -/ lemma posLog_norm_add_le {E : Type*} [NormedAddCommGroup E] (a b : E) : log⁺ ‖a + b‖ ≤ log⁺ ‖a‖ + log⁺ ‖b‖ + log 2 := by - calc log⁺ ‖a + b‖ - _ ≤ log⁺ (‖a‖ + ‖b‖) := by - apply monotoneOn_posLog _ _ (norm_add_le a b) - <;> simp [add_nonneg (norm_nonneg a) (norm_nonneg b)] - _ ≤ log⁺ ‖a‖ + log⁺ ‖b‖ + log 2 := by - convert posLog_add using 1 - ring + grw [norm_add_le, posLog_add, add_rotate] end Real From 4f24a277e0401fd728804b7e926c3baf6de42ff1 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Sun, 19 Oct 2025 23:29:43 +0100 Subject: [PATCH 2/2] Update PosLog.lean --- Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean b/Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean index 5bec46db50e619..354bc9fde36f6a 100644 --- a/Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean +++ b/Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean @@ -92,9 +92,8 @@ theorem monotoneOn_posLog : MonotoneOn log⁺ (Set.Ici 0) := by linarith @[gcongr] -lemma posLog_le_posLog (x y : ℝ) (hx : 0 ≤ x) (hxy : x ≤ y) : - log⁺ x ≤ log⁺ y := - Real.monotoneOn_posLog hx (hx.trans hxy) hxy +lemma posLog_le_posLog {x y : ℝ} (hx : 0 ≤ x) (hxy : x ≤ y) : log⁺ x ≤ log⁺ y := + monotoneOn_posLog hx (hx.trans hxy) hxy /-! ## Estimates for Products