WikiLean Articles · Brain · Recent changes · Proposals · Flags · Stats · About

Diff — Logistic function

Revision #3480 → #4023 · back to history

addedLogistic as smooth approximation of Heaviside stepf166fa7e96b4
modifiedAnalyticity of standard logistic functionc212b42f922a
FieldFrom #3480To #4023
mathlib.declReal.analyticAt_sigmoidanalyticAt_sigmoid
note`Real.analyticAt_sigmoid` (and `Real.analyticOnNhd_sigmoid` on `Set.univ`) prove sigmoid is real-analytic everywhere.`analyticAt_sigmoid` (and `analyticOnNhd_sigmoid` on `Set.univ`) prove sigmoid is real-analytic everywhere; these are declared at the root, not in the `Real` namespace.