From 402128875fa3c67b001f5b5deb4cdeeea166c2ed Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Fri, 20 Dec 2024 20:52:06 +0100
Subject: [PATCH] Update logpos.lean

---
 Nevanlinna/logpos.lean | 92 +++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 90 insertions(+), 2 deletions(-)

diff --git a/Nevanlinna/logpos.lean b/Nevanlinna/logpos.lean
index 60d6ade..cd85108 100644
--- a/Nevanlinna/logpos.lean
+++ b/Nevanlinna/logpos.lean
@@ -35,5 +35,93 @@ theorem logpos_norm {r : ℝ} : log⁺ r = 2⁻¹ * (log r + ‖log r‖) := by
     rw [this]
     ring
 
--- WANT: logpos is even and continuous
--- WANT: Inequalities
+theorem logpos_abs
+  {x : ℝ} :
+  log⁺ x = log⁺ |x| := by
+  unfold logpos
+  simp
+
+-- Warning: This should be fixed in Mathlib
+
+theorem log_pos_iff' (hx : 0 ≤ x) : 0 < log x ↔ 1 < x := by
+  by_cases h₁x : x = 0
+  · rw [h₁x]; simp
+  · exact log_pos_iff (lt_of_le_of_ne hx (Ne.symm h₁x))
+
+
+theorem Real.monotoneOn_logpos :
+  MonotoneOn logpos (Set.Ici 0) := by
+
+  intro x hx y hy hxy
+  unfold logpos
+  simp
+
+  by_cases h : log x ≤ 0
+  · tauto
+  · simp [h]
+    simp at h
+
+    have : log x ≤ log y := by
+      apply log_le_log
+      --
+      rw [log_pos_iff' hx] at h
+      have : (0 : ℝ) < 1 := by exact Real.zero_lt_one
+      exact lt_trans this h
+      assumption
+
+    constructor
+    · linarith
+    · linarith
+
+
+theorem logpos_add_le_add_logpos_add_log2₀
+  {a b : ℝ}
+  (h : |a| ≤ |b|) :
+  log⁺ (a + b) ≤ log⁺ a + log⁺ b + log 2 := by
+
+  nth_rw 1 [logpos_abs]
+  nth_rw 2 [logpos_abs]
+  nth_rw 3 [logpos_abs]
+
+  calc log⁺ |a + b|
+  _ ≤ log⁺ (|a| + |b|) := by
+    apply Real.monotoneOn_logpos
+    simp [abs_nonneg]; simp [abs_nonneg]
+    apply add_nonneg
+    simp [abs_nonneg]; simp [abs_nonneg]
+    exact abs_add_le a b
+  _ ≤ log⁺ (|b| + |b|) := by
+    apply Real.monotoneOn_logpos
+    simp [abs_nonneg]
+    apply add_nonneg
+    simp [abs_nonneg]; simp [abs_nonneg]
+    simp [h]
+    linarith
+  _ = log⁺ (2 * |b|) := by
+    congr; ring
+  _ ≤ log⁺ |b| + log 2 := by
+    unfold logpos; simp
+    constructor
+    · apply add_nonneg
+      simp
+      exact log_nonneg one_le_two
+    · by_cases hb: b = 0
+      · rw [hb]; simp
+        exact log_nonneg one_le_two
+      · rw [log_mul, log_abs, add_comm]
+        simp
+        exact Ne.symm (NeZero.ne' 2)
+        exact abs_ne_zero.mpr hb
+  _ ≤ log⁺ |a| + log⁺ |b| + log 2 := by
+    unfold logpos; simp
+
+
+theorem logpos_add_le_add_logpos_add_log2
+  {a b : ℝ} :
+  log⁺ (a + b) ≤ log⁺ a + log⁺ b + log 2 := by
+
+  by_cases h : |a| ≤ |b|
+  · exact logpos_add_le_add_logpos_add_log2₀ h
+  · rw [add_comm a b, add_comm (log⁺ a) (log⁺ b)]
+    apply logpos_add_le_add_logpos_add_log2₀
+    exact le_of_not_ge h