40 lines
875 B
Plaintext
40 lines
875 B
Plaintext
import Mathlib.Analysis.SpecialFunctions.Log.Basic
|
||
|
||
open Real
|
||
|
||
|
||
noncomputable def logpos : ℝ → ℝ := fun r ↦ max 0 (log r)
|
||
|
||
notation "log⁺" => logpos
|
||
|
||
|
||
theorem loglogpos {r : ℝ} : log r = log⁺ r - log⁺ 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 : ℝ} : 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
|
||
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
|
||
|
||
-- WANT: logpos is even and continuous
|
||
-- WANT: Inequalities
|