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

---
 Nevanlinna/logpos.lean | 15 +++++++++------
 1 file changed, 9 insertions(+), 6 deletions(-)

diff --git a/Nevanlinna/logpos.lean b/Nevanlinna/logpos.lean
index b89b3af..60d6ade 100644
--- a/Nevanlinna/logpos.lean
+++ b/Nevanlinna/logpos.lean
@@ -1,14 +1,14 @@
-import Mathlib.MeasureTheory.Integral.CircleIntegral
-import Nevanlinna.divisor
-import Nevanlinna.stronglyMeromorphicOn
-import Nevanlinna.meromorphicOn_divisor
+import Mathlib.Analysis.SpecialFunctions.Log.Basic
 
 open Real
 
 
 noncomputable def logpos : ℝ → ℝ := fun r ↦ max 0 (log r)
 
-theorem loglogpos {r : ℝ} : log r = logpos r - logpos r⁻¹ := by
+notation "log⁺" => logpos
+
+
+theorem loglogpos {r : ℝ} : log r = log⁺ r - log⁺ r⁻¹ := by
   unfold logpos
   rw [log_inv]
   by_cases h : 0 ≤ log r
@@ -19,7 +19,7 @@ theorem loglogpos {r : ℝ} : log r = logpos r - logpos r⁻¹ := by
     exact neg_nonneg.mp this
 
 
-theorem logpos_norm {r : ℝ} : logpos r = 2⁻¹ * (log r + ‖log r‖) := by
+theorem logpos_norm {r : ℝ} : log⁺ r = 2⁻¹ * (log r + ‖log r‖) := by
   by_cases hr : 0 ≤ log r
   · rw [norm_of_nonneg hr]
     have : logpos r = log r := by
@@ -34,3 +34,6 @@ theorem logpos_norm {r : ℝ} : logpos r = 2⁻¹ * (log r + ‖log r‖) := by
       exact le_of_not_ge hr
     rw [this]
     ring
+
+-- WANT: logpos is even and continuous
+-- WANT: Inequalities