Special functions

DefinitionLogarithm#

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.

Real.log (x : ℝ) : ℝ
Sources
MathlibReal.log
Uses 1 · Used by 17
Statement usesExponential
Used byArithmetic Mean/Geometric Mean · Bertrand’s Postulate · Stirling’s Formula · First Main Theorem of Value Distribution Theory · Inverse hyperbolic trigonometric functions · Behrend's construction · Corners theorem · Roth's theorem · Regularity lemma · Triangle removal lemma · Dirichlet class number formula · Dirichlet unit theorem · Mellin inversion theorem · Akra–Bazzi theorem · Ostrowski's theorem · Log · Cauchy formulas

DefinitionExponential#

The real exponential function, defined as the real part of the complex exponential

Real.exp (x : ℝ) : ℝ
Sources
MathlibReal.exp
Uses 1 · Used by 10
Statement usesComplex exponential
Used byStirling’s Formula · Phragmen-Lindelöf principle · Logarithm · Bernoulli numbers · Exponential law · Gaussian law · Poisson law · Fourier theorem · Poisson limit theorem · Grönwall lemma

DefinitionTrigonometric functions#

The real sine function, defined as the real part of the complex sine

Real.sin (x : ℝ) : ℝ
Sources
MathlibReal.sin
Uses 1 · Used by 2
Statement usesSin (extension of trigonometric functions to the complex plane)
Used byInverse trigonometric functions · Fernique's theorem

DefinitionInverse trigonometric functions#

Inverse of the sin function, returns values in the range -π / 2 ≤ arcsin x ≤ π / 2. It defaults to -π / 2 on (-∞, -1) and to π / 2 to (1, ∞).

Real.arcsin : ℝ → ℝ
Sources
MathlibReal.arcsin
Uses 2 · Used by 7
Statement usesCos (extension of trigonometric functions to the complex plane) · Trigonometric functions
Used byThe Area of a Circle · Buffon Needle Problem · Angle · Mellin inversion theorem · Inscribed angle theorem · Change of variables to polar co-ordinates · Log

DefinitionHyperbolic trigonometric functions#

The real hyperbolic sine function, defined as the real part of the complex hyperbolic sine

Real.sinh (x : ℝ) : ℝ
Sources
MathlibReal.sinh
Uses 1
Statement usesComplex exponential

DefinitionInverse hyperbolic trigonometric functions#

arsinh is defined using a logarithm, arsinh x = log (x + √(1 + x^2)).

Real.arsinh (x : ℝ) : ℝ
Sources
MathlibReal.arsinh
Uses 1
Statement usesLogarithm

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.