Documentation

Mathlib.Analysis.SpecialFunctions.Log.PosLog

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.

Definition, Notation and Reformulations #

noncomputable def Real.posLog :

Definition: the positive part of the logarithm.

Equations

Notation log⁺ for the positive part of the logarithm.

Equations
theorem Real.posLog_def {r : } :
r.posLog = max 0 (log r)

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

Elementary Properties #

Presentation of log in terms of its positive part.

Presentation of log⁺ in terms of log.

theorem Real.posLog_nonneg {x : } :

The positive part of log is never negative.

@[simp]
theorem Real.posLog_neg (x : ) :

The function log⁺ is even.

@[simp]
theorem Real.posLog_abs (x : ) :

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|) :

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.

The function log⁺ is monotone on the positive axis.

Estimates for Products #

theorem Real.posLog_mul {a b : } :

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 : α) :
(∏ ts, f t).posLog ts, (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 : α) :
(∑ ts, f t).posLog log s.card + ts, (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.