Exponential, logarithmic and related functions

Exponential, logarithmic and trigonometric-type functions and their relatives: exponential integral E1 and Ein, logarithmic integral, Lambert W, logistic function, x^y = y^x, exponential sums, Mittag-Leffler expansion of 1/(e^u − 1), modified Bessel functions, Dickman–de Bruijn function, Bell-polynomial functions.

• Dickman–de Bruijn function
• Exponential autonomous functions
• Exponential integral
• Lambert W function
• Logarithmic integral
• Mittag-Leffler expansion of 1/(e^u − 1)
• Modified Bessel functions of the first kind

TheoremExponential sums have full column rank#✓fully proved

If ∑_{u ∈ S} c_u exp(-a u) vanishes at |S| distinct points a ∈ P (the rates u ∈ S are distinct as elements of a Finset), every coefficient is zero. Equivalently, the matrix (exp(-a u))_{a ∈ P, u ∈ S} has full column rank when |P| ≥ |S|.

theorem eq_zero_of_sum_mul_exp_eq_zero {S P : Finset ℝ} (hSP : S.card ≤ P.card) (c : ℝ → ℝ)
    (h : ∀ a ∈ P, ∑ u ∈ S, c u * Real.exp (-(a * u)) = 0) :
    ∀ u ∈ S, c u = 0

Used by 1

Used byBhaskar–Song identifiability

TheoremParametrization of the solutions of \(x^y = y^x\) with \(0 < y < x\)#✓fully proved

Let \(x\) and \(y\) be real numbers with \(0 < y < x\) and \(x^y = y^x\). Then there is a real number \(t > 0\) such that \(y = (1 + 1/t)^t\) and \(x = (1 + 1/t)^{t+1}\).

theorem exists_parametrization_of_rpow_eq_rpow (x y : ℝ) (hy : 0 < y) (hyx : y < x)
  (hxy : Real.rpow x y = Real.rpow y x) : ∃ (t : ℝ), 0 < t ∧
  (y = Real.rpow (1 + 1 / t) t ∧ x = Real.rpow (1 + 1 / t) (t + 1))

Sources

• Hirotaka Kobayashi, Kota Saito, and Wataru Takeda, "Transcendence of Values of the Iterated Exponential Function at Algebraic Points," Journal of Integer Sequences 26 (2023), Article 23.3.3, Lemma, lines 604–612, https://cs.uwaterloo.ca/journals/JIS/VOL26/Takeda/tak6.tex.

TheoremThe logistic function of the log odds#✓fully proved

For real numbers \(a > 0\) and \(b > 0\), the logistic function \(\sigma(z) = 1 / (1 + e^{-z})\) satisfies \(\sigma(\log a - \log b) = a / (a + b)\).

theorem sigmoid_log_sub_log {a b : ℝ} (ha : 0 < a) (hb : 0 < b) :
    sigmoid (log a - log b) = a / (a + b)

Used by 1

Used byNaive-Bayes posterior

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.