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.

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

Definition, Notation and Reformulations #

source
noncomputable def Real.posLog :
ℝ → ℝ

Definition: the positive part of the logarithm.

Equations
Instances For
    source
    def Real.«termLog⁺» :
    Lean.ParserDescr

    Notation log⁺ for the positive part of the logarithm.

    Equations
    Instances For
      source
      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 #

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

      Presentation of log in terms of its positive part.

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

      Presentation of log⁺ in terms of log.

      source
      @[simp]
      theorem Real.posLog_zero :
      posLog 0 = 0
      source
      @[simp]
      theorem Real.posLog_one :
      posLog 1 = 0
      source
      theorem Real.posLog_nonneg {x : ℝ} :
      0 ≤ x.posLog

      The positive part of log is never negative.

      source
      @[simp]
      theorem Real.posLog_neg (x : ℝ) :
      (-x).posLog = x.posLog

      The function log⁺ is even.

      source
      @[simp]
      theorem Real.posLog_abs (x : ℝ) :
      |x|.posLog = x.posLog

      The function log⁺ is even.

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

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

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

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

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

      The function log⁺ equals log for all natural numbers.

      source
      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.

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

      The function log⁺ is monotone on the positive axis.

      source
      theorem Real.posLog_le_posLog {x y : ℝ} (hx : 0 ≤ x) (hxy : x ≤ y) :
      x.posLog ≤ y.posLog
      source
      @[simp]
      theorem Real.posLog_pow (n : ℕ) (x : ℝ) :
      (x ^ n).posLog = ↑n * x.posLog

      The function log⁺ commutes with taking powers.

      Estimates for Products #

      source
      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.

      source
      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.

      source
      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 #

      source
      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.

      source
      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.

      source
      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.

      source
      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.