Documentation

Mathlib.Analysis.SpecialFunctions.Log.Basic

Real logarithm #

In this file we define Real.log to be the logarithm of a real number. As usual, we extend it from its domain (0, +∞) to a globally defined function. We choose to do it so that log 0 = 0 and log (-x) = log x.

We prove some basic properties of this function and show that it is continuous.

Tags #

logarithm, continuity

noncomputable def Real.log (x : ) :

The real logarithm function, equal to the inverse of the exponential for x > 0, to log |x| for x < 0, and to 0 for 0. We use this unconventional extension to (-∞, 0] as it gives the formula log (x * y) = log x + log y for all nonzero x and y, and the derivative of log is 1/x away from 0.

Equations
Instances For
    theorem Real.log_of_ne_zero {x : } (hx : x 0) :
    Real.log x = Real.expOrderIso.symm |x|,
    theorem Real.log_of_pos {x : } (hx : 0 < x) :
    Real.log x = Real.expOrderIso.symm x, hx
    theorem Real.exp_log_eq_abs {x : } (hx : x 0) :
    theorem Real.exp_log {x : } (hx : 0 < x) :
    theorem Real.exp_log_of_neg {x : } (hx : x < 0) :
    @[simp]
    theorem Real.log_exp (x : ) :
    @[simp]
    @[simp]
    theorem Real.log_zero :
    @[simp]
    theorem Real.log_one :
    @[simp]
    theorem Real.log_abs (x : ) :
    @[simp]
    theorem Real.sinh_log {x : } (hx : 0 < x) :
    theorem Real.cosh_log {x : } (hx : 0 < x) :
    theorem Real.log_mul {x : } {y : } (hx : x 0) (hy : y 0) :
    theorem Real.log_div {x : } {y : } (hx : x 0) (hy : y 0) :
    @[simp]
    theorem Real.log_le_log_iff {x : } {y : } (h : 0 < x) (h₁ : 0 < y) :
    theorem Real.log_le_log {x : } {y : } (hx : 0 < x) (hxy : x y) :
    theorem Real.log_lt_log {x : } {y : } (hx : 0 < x) (h : x < y) :
    theorem Real.log_lt_log_iff {x : } {y : } (hx : 0 < x) (hy : 0 < y) :
    theorem Real.log_le_iff_le_exp {x : } {y : } (hx : 0 < x) :
    theorem Real.log_lt_iff_lt_exp {x : } {y : } (hx : 0 < x) :
    theorem Real.le_log_iff_exp_le {x : } {y : } (hy : 0 < y) :
    theorem Real.lt_log_iff_exp_lt {x : } {y : } (hy : 0 < y) :
    theorem Real.log_pos_iff {x : } (hx : 0 < x) :
    0 < Real.log x 1 < x
    theorem Real.log_pos {x : } (hx : 1 < x) :
    theorem Real.log_pos_of_lt_neg_one {x : } (hx : x < -1) :
    theorem Real.log_neg_iff {x : } (h : 0 < x) :
    Real.log x < 0 x < 1
    theorem Real.log_neg {x : } (h0 : 0 < x) (h1 : x < 1) :
    theorem Real.log_neg_of_lt_zero {x : } (h0 : x < 0) (h1 : -1 < x) :
    theorem Real.log_nonneg_iff {x : } (hx : 0 < x) :
    theorem Real.log_nonneg {x : } (hx : 1 x) :
    theorem Real.log_nonpos_iff {x : } (hx : 0 < x) :
    theorem Real.log_nonpos_iff' {x : } (hx : 0 x) :
    theorem Real.log_nonpos {x : } (hx : 0 x) (h'x : x 1) :
    @[deprecated Real.log_natCast_nonneg]

    Alias of Real.log_natCast_nonneg.

    @[deprecated Real.log_neg_natCast_nonneg]

    Alias of Real.log_neg_natCast_nonneg.

    @[deprecated Real.log_intCast_nonneg]

    Alias of Real.log_intCast_nonneg.

    theorem Real.log_lt_sub_one_of_pos {x : } (hx1 : 0 < x) (hx2 : x 1) :
    Real.log x < x - 1
    theorem Real.eq_one_of_pos_of_log_eq_zero {x : } (h₁ : 0 < x) (h₂ : Real.log x = 0) :
    x = 1
    theorem Real.log_ne_zero_of_pos_of_ne_one {x : } (hx_pos : 0 < x) (hx : x 1) :
    @[simp]
    theorem Real.log_eq_zero {x : } :
    Real.log x = 0 x = 0 x = 1 x = -1
    theorem Real.log_ne_zero {x : } :
    Real.log x 0 x 0 x 1 x -1
    @[simp]
    theorem Real.log_pow (x : ) (n : ) :
    Real.log (x ^ n) = n * Real.log x
    @[simp]
    theorem Real.log_zpow (x : ) (n : ) :
    Real.log (x ^ n) = n * Real.log x
    theorem Real.log_sqrt {x : } (hx : 0 x) :
    theorem Real.log_le_sub_one_of_pos {x : } (hx : 0 < x) :
    Real.log x x - 1
    theorem Real.log_le_self {x : } (hx : 0 x) :

    See Real.log_le_sub_one_of_pos for the stronger version when x ≠ 0.

    theorem Real.neg_inv_le_log {x : } (hx : 0 x) :

    See Real.one_sub_inv_le_log_of_pos for the stronger version when x ≠ 0.

    theorem Real.abs_log_mul_self_lt (x : ) (h1 : 0 < x) (h2 : x 1) :
    |Real.log x * x| < 1

    Bound for |log x * x| in the interval (0, 1].

    theorem Real.tendsto_log_atTop :
    Filter.Tendsto Real.log Filter.atTop Filter.atTop

    The real logarithm function tends to +∞ at +∞.

    theorem Real.continuous_log :
    Continuous fun (x : { x : // x 0 }) => Real.log x
    theorem Real.continuous_log' :
    Continuous fun (x : { x : // 0 < x }) => Real.log x
    theorem Real.log_prod {α : Type u_1} (s : Finset α) (f : α) (hf : xs, f x 0) :
    Real.log (∏ is, f i) = is, Real.log (f i)
    theorem Finsupp.log_prod {α : Type u_1} {β : Type u_2} [Zero β] (f : α →₀ β) (g : αβ) (hg : ∀ (a : α), g a (f a) = 0f a = 0) :
    Real.log (f.prod g) = f.sum fun (a : α) (b : β) => Real.log (g a b)
    theorem Real.log_nat_eq_sum_factorization (n : ) :
    Real.log n = n.factorization.sum fun (p t : ) => t * Real.log p
    theorem Real.tendsto_pow_log_div_mul_add_atTop (a : ) (b : ) (n : ) (ha : a 0) :
    Filter.Tendsto (fun (x : ) => Real.log x ^ n / (a * x + b)) Filter.atTop (nhds 0)
    theorem Real.isLittleO_pow_log_id_atTop {n : } :
    (fun (x : ) => Real.log x ^ n) =o[Filter.atTop] id
    theorem Real.isLittleO_const_log_atTop {c : } :
    (fun (x : ) => c) =o[Filter.atTop] Real.log
    theorem Filter.Tendsto.log {α : Type u_1} {f : α} {l : Filter α} {x : } (h : Filter.Tendsto f l (nhds x)) (hx : x 0) :
    Filter.Tendsto (fun (x : α) => Real.log (f x)) l (nhds (Real.log x))
    theorem Continuous.log {α : Type u_1} [TopologicalSpace α] {f : α} (hf : Continuous f) (h₀ : ∀ (x : α), f x 0) :
    Continuous fun (x : α) => Real.log (f x)
    theorem ContinuousAt.log {α : Type u_1} [TopologicalSpace α] {f : α} {a : α} (hf : ContinuousAt f a) (h₀ : f a 0) :
    ContinuousAt (fun (x : α) => Real.log (f x)) a
    theorem ContinuousWithinAt.log {α : Type u_1} [TopologicalSpace α] {f : α} {s : Set α} {a : α} (hf : ContinuousWithinAt f s a) (h₀ : f a 0) :
    ContinuousWithinAt (fun (x : α) => Real.log (f x)) s a
    theorem ContinuousOn.log {α : Type u_1} [TopologicalSpace α] {f : α} {s : Set α} (hf : ContinuousOn f s) (h₀ : xs, f x 0) :
    ContinuousOn (fun (x : α) => Real.log (f x)) s
    theorem Real.tendsto_log_comp_add_sub_log (y : ) :
    Filter.Tendsto (fun (x : ) => Real.log (x + y) - Real.log x) Filter.atTop (nhds 0)
    theorem Real.tendsto_log_nat_add_one_sub_log :
    Filter.Tendsto (fun (k : ) => Real.log (k + 1) - Real.log k) Filter.atTop (nhds 0)
    theorem Mathlib.Meta.Positivity.log_pos_of_isRat {e : } {d : } {n : } :
    Mathlib.Meta.NormNum.IsRat e n ddecide (1 < n / d) = true0 < Real.log e
    theorem Mathlib.Meta.Positivity.log_nz_of_isRat {e : } {d : } {n : } :
    Mathlib.Meta.NormNum.IsRat e n ddecide (0 < n / d) = truedecide (n / d < 1) = trueReal.log e 0
    theorem Mathlib.Meta.Positivity.log_nz_of_isRat_neg {e : } {d : } {n : } :
    Mathlib.Meta.NormNum.IsRat e n ddecide (n / d < 0) = truedecide (-1 < n / d) = trueReal.log e 0

    Extension for the positivity tactic: Real.log of a natural number is always nonnegative.

    Instances For

      Extension for the positivity tactic: Real.log of an integer is always nonnegative.

      Instances For

        Extension for the positivity tactic: Real.log of a numeric literal.

        Instances For