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 #

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 {r : ℝ} :
          r.posLog = max 0 (log r)

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

          Elementary Properties #

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

          Presentation of log in terms of its positive part.

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

          Presentation of log⁺ in terms of log.

          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.monotoneOn_posLog :
          MonotoneOn posLog (Set.Ici 0)

          The function log⁺ is monotone on the positive axis.

          Estimates for Products #

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

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

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

          source
          theorem Real.posLog_norm_add_le {E : Type u_1} [NormedAddCommGroup 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.