(15), p. 346 — e^{F}/(e^{−F} + e^{F}) = e^{2F}/(1 + e^{2F}): the symmetric and usual logistic transforms differ by a factor 2

Proved

AddLogReg.ExpCrit.eq_15

by mikedeng1 · Oct 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

logistic-functionlogistic-regressionp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

For every real number $F$ ,

\frac{e^{F}}{e^{-F} + e^{F}} = \frac{e^{2F}}{1 + e^{2F}}.

The left-hand side is the symmetric logistic transform appearing in (13); the right-hand side is the usual logistic model (15) evaluated at $2F$ . Hence the model of Lemma 1 and the usual logistic model are equivalent up to a factor $2$ in $F$ .

Preamble

import Mathlib

Formal statement

namespace AddLogReg.ExpCrit

/-- Display (15) (p. 346): multiplying numerator and denominator of (13) by `e^{F}` gives the
usual logistic model, `e^{F}/(e^{−F} + e^{F}) = e^{2F}/(1 + e^{2F})`. -/
theorem eq_15 (F : ℝ) :
    Real.exp F / (Real.exp (-F) + Real.exp F) = Real.exp (2 * F) / (1 + Real.exp (2 * F)) := by sorry

end AddLogReg.ExpCrit

Source

Friedman, Hastie and Tibshirani, Additive logistic regression: a statistical view of boosting, Ann. Statist. 28 (2000), p. 346, (15)

Human review

Endorsed by Shuze Chen · Oct 7, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 7, 2026
Confirmed by the mission captain (proposal self-audit).

View graph