The logistic distribution

The standard logistic distribution is the probability measure on ℝ whose distribution function is the sigmoid σ x = 1 / (1 + exp (-x)). It is the Stieltjes measure of Real.sigmoid, so its cdf is the sigmoid (cdf_logisticMeasure) and its upper tail at x is σ (-x) (logisticMeasure_real_Ioi), so the log-odds Real.logit invert the distribution function on (0, 1). [UPSTREAM] candidate for Mathlib/Probability/Distributions/Logistic.lean.

Main definitions

• ProbabilityTheory.logisticMeasure: the standard logistic distribution.

Main results

• ProbabilityTheory.cdf_logisticMeasure: the cdf of the standard logistic distribution is the sigmoid.
• ProbabilityTheory.logisticMeasure_real_Ioi: its upper tail at x is σ (-x).

noncomputable def ProbabilityTheory.sigmoidStieltjes : StieltjesFunction ℝ

The sigmoid as a Stieltjes function.

Equations

• ProbabilityTheory.sigmoidStieltjes = { toFun := Real.sigmoid, mono' := Real.sigmoid_monotone, right_continuous' := ProbabilityTheory.sigmoidStieltjes._proof_1 }

@[simp]

theorem ProbabilityTheory.sigmoidStieltjes_apply (x : ℝ) : ↑sigmoidStieltjes x = x.sigmoid

noncomputable def ProbabilityTheory.logisticMeasure : MeasureTheory.Measure ℝ

The standard logistic distribution, the probability measure whose distribution function is the sigmoid.

Equations

• ProbabilityTheory.logisticMeasure = ProbabilityTheory.sigmoidStieltjes.measure

instance ProbabilityTheory.instIsProbabilityMeasureRealLogisticMeasure : MeasureTheory.IsProbabilityMeasure logisticMeasure

theorem ProbabilityTheory.cdf_logisticMeasure (x : ℝ) : ↑(cdf logisticMeasure) x = x.sigmoid

theorem ProbabilityTheory.logisticMeasure_real_Ioi (x : ℝ) : logisticMeasure.real (Set.Ioi x) = (-x).sigmoid

The upper tail of the standard logistic distribution at x is the sigmoid at -x.