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)

See Mathlib/Analysis/SpecialFunctions/Integrals/PosLogEqCircleAverage.lean for the presentation of log⁺ as a Circle Average.

Definition, Notation and Reformulations

noncomputable def Real.posLog : ℝ → ℝ

Definition: the positive part of the logarithm.

def Real.«termLog⁺» : Lean.ParserDescr

Notation log⁺ for the positive part of the logarithm.

theorem Real.posLog_def {x : ℝ} : x.posLog = max 0 (log x)

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

Elementary Properties

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

Presentation of log in terms of its positive part.

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

Presentation of log⁺ in terms of log.

@[simp]

theorem Real.posLog_zero : posLog 0 = 0

@[simp]

theorem Real.posLog_one : posLog 1 = 0

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.posLog_eq_log_max_one {x : ℝ} (hx : 0 ≤ x) : x.posLog = log (max 1 x)

The function log⁺ equals log (max 1 _) for non-negative real numbers.

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

The function log⁺ is monotone on the positive axis.

theorem Real.posLog_le_posLog {x y : ℝ} (hx : 0 ≤ x) (hxy : x ≤ y) : x.posLog ≤ y.posLog

@[simp]

theorem Real.posLog_pow (n : ℕ) (x : ℝ) : (x ^ n).posLog = ↑n * x.posLog

The function log⁺ commutes with taking powers.

Estimates for Products

theorem Real.posLog_mul {x y : ℝ} : (x * y).posLog ≤ x.posLog + y.posLog

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

theorem Real.posLog_nat_mul {x : ℝ} {n : ℕ} : (↑n * x).posLog ≤ log ↑n + x.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_norm_sum_le {E : Type u_1} [SeminormedAddCommGroup E] {α : Type u_2} (s : Finset α) (f : α → E) : ‖∑ t ∈ s, f t‖.posLog ≤ log ↑s.card + ∑ t ∈ s, ‖f t‖.posLog

Variant of posLog_sum for norms of elements in normed additive commutative groups, using monotonicity of log⁺ and the triangle inequality.

theorem Real.posLog_add {x y : ℝ} : (x + y).posLog ≤ log 2 + x.posLog + y.posLog

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

theorem Real.posLog_norm_add_le {E : Type u_1} [SeminormedAddCommGroup E] (a b : E) : ‖a + b‖.posLog ≤ ‖a‖.posLog + ‖b‖.posLog + log 2

Variant of posLog_add for norms of elements in normed additive commutative groups, using monotonicity of log⁺ and the triangle inequality.