37 lines
891 B
Plaintext
37 lines
891 B
Plaintext
|
import Mathlib.MeasureTheory.Integral.CircleIntegral
|
|||
|
|
import Nevanlinna.divisor
|
|||
|
|
import Nevanlinna.stronglyMeromorphicOn
|
|||
|
|
import Nevanlinna.meromorphicOn_divisor
|
|||
|
|
|
|||
|
|
open Real
|
|||
|
|
|
|||
|
|
|
|||
|
|
noncomputable def logpos : ℝ → ℝ := fun r ↦ max 0 (log r)
|
|||
|
|
|
|||
|
|
theorem loglogpos {r : ℝ} : log r = logpos r - logpos r⁻¹ := by
|
|||
|
|
unfold logpos
|
|||
|
|
rw [log_inv]
|
|||
|
|
by_cases h : 0 ≤ log r
|
|||
|
|
· simp [h]
|
|||
|
|
· simp at h
|
|||
|
|
have : 0 ≤ -log r := Left.nonneg_neg_iff.2 (le_of_lt h)
|
|||
|
|
simp [h, this]
|
|||
|
|
exact neg_nonneg.mp this
|
|||
|
|
|
|||
|
|
|
|||
|
|
theorem logpos_norm {r : ℝ} : logpos r = 2⁻¹ * (log r + ‖log r‖) := by
|
|||
|
|
by_cases hr : 0 ≤ log r
|
|||
|
|
· rw [norm_of_nonneg hr]
|
|||
|
|
have : logpos r = log r := by
|
|||
|
|
unfold logpos
|
|||
|
|
simp [hr]
|
|||
|
|
rw [this]
|
|||
|
|
ring
|
|||
|
|
· rw [norm_of_nonpos (le_of_not_ge hr)]
|
|||
|
|
have : logpos r = 0 := by
|
|||
|
|
unfold logpos
|
|||
|
|
simp
|
|||
|
|
exact le_of_not_ge hr
|
|||
|
|
rw [this]
|
|||
|
|
ring
|