The Positive Part of the Logarithm

This file defines the function Real.posLog = r ↦ max 0 (log r) and introduces the notation log⁺. For a finite length-n sequence f i of reals, it establishes the following standard estimates.

• theorem posLog_prod : log⁺ (∏ i, f i) ≤ ∑ i, log⁺ (f i)

• theorem posLog_sum : log⁺ (∑ i, f i) ≤ log n + ∑ i, log⁺ (f i)

Definition, Notation and Reformulations

noncomputable def Real.posLog : ℝ → ℝ

Definition: the positive part of the logarithm.

Equations

• r.posLog = 0 ⊔ Real.log r

def Real.«termLog⁺» : Lean.ParserDescr

Notation log⁺ for the positive part of the logarithm.

Equations

• Real.«termLog⁺» = Lean.ParserDescr.node `Real.«termLog⁺» 1024 (Lean.ParserDescr.symbol "log⁺")

theorem Real.posLog_def {r : ℝ} : r.posLog = 0 ⊔ log r

Definition of the positive part of the logarithm, formulated as a theorem.

Elementary Properties

theorem Real.posLog_sub_posLog_inv {r : ℝ} : r.posLog - r⁻¹.posLog = log r

Presentation of log in terms of its positive part.

theorem Real.half_mul_log_add_log_abs {r : ℝ} : 2⁻¹ * (log r + |log r|) = r.posLog

Presentation of log⁺ in terms of log.

theorem Real.posLog_nonneg {x : ℝ} : 0 ≤ x.posLog

The positive part of log is never negative.

@[simp]

theorem Real.posLog_neg (x : ℝ) : (-x).posLog = x.posLog

The function log⁺ is even.

@[simp]

theorem Real.posLog_abs (x : ℝ) : |x|.posLog = x.posLog

The function log⁺ is even.

theorem Real.posLog_eq_zero_iff (x : ℝ) : x.posLog = 0 ↔ |x| ≤ 1

The function log⁺ is zero in the interval [-1,1].

theorem Real.posLog_eq_log {x : ℝ} (hx : 1 ≤ |x|) : x.posLog = log x

The function log⁺ equals log outside of the interval (-1,1).

theorem Real.log_of_nat_eq_posLog {n : ℕ} : (↑n).posLog = log ↑n

The function log⁺ equals log for all natural numbers.

theorem Real.monotoneOn_posLog : MonotoneOn posLog (Set.Ici 0)

The function log⁺ is monotone on the positive axis.

Estimates for Products

theorem Real.posLog_mul {a b : ℝ} : (a * b).posLog ≤ a.posLog + b.posLog

Estimate for log⁺ of a product. See Real.posLog_prod for a variant involving multiple factors.

theorem Real.posLog_nat_mul {n : ℕ} {a : ℝ} : (↑n * a).posLog ≤ log ↑n + a.posLog

Estimate for log⁺ of a product. Special case of Real.posLog_mul where one of the factors is a natural number.

theorem Real.posLog_prod {α : Type u_1} (s : Finset α) (f : α → ℝ) : (∏ t ∈ s, f t).posLog ≤ ∑ t ∈ s, (f t).posLog

Estimate for log⁺ of a product. See Real.posLog_mul for a variant with only two factors.

Estimates for Sums

theorem Real.posLog_sum {α : Type u_1} (s : Finset α) (f : α → ℝ) : (∑ t ∈ s, f t).posLog ≤ log ↑s.card + ∑ t ∈ s, (f t).posLog

Estimate for log⁺ of a sum. See Real.posLog_add for a variant involving just two summands.

theorem Real.posLog_add {a b : ℝ} : (a + b).posLog ≤ log 2 + a.posLog + b.posLog

Estimate for log⁺ of a sum. See Real.posLog_sum for a variant involving multiple summands.