The logistic function and the log-odds

The log-odds Real.logit p = log (p / (1 - p)) invert the logistic function on (0, 1). The share of one of two exponentials in their sum is the logistic function of the difference of their exponents.

theorem Real.exp_div_add_exp_eq_sigmoid (x y : ℝ) : exp x / (exp x + exp y) = (x - y).sigmoid

theorem Real.sigmoid_log {x : ℝ} (hx : 0 < x) : (log x).sigmoid = x / (x + 1)

noncomputable def Real.logit (p : ℝ) : ℝ

The log-odds log (p / (1 - p)), the inverse of Real.sigmoid.

Equations

• p.logit = Real.log (p / (1 - p))

@[simp]

theorem Real.logit_sigmoid (x : ℝ) : x.sigmoid.logit = x

theorem Real.sigmoid_logit {p : ℝ} (hp : p ∈ Set.Ioo 0 1) : p.logit.sigmoid = p