Sigmoid function

In this file we define the sigmoid function x : ℝ ↦ (1 + exp (-x))⁻¹ and prove some of its analytic properties.

We then show that the sigmoid function can be seen as an order embedding from ℝ to I = [0, 1] and that this embedding is both a topological embedding and a measurable embedding. We also prove that the composition of this embedding with the measurable embedding from a standard Borel space α to ℝ is a measurable embedding from α to I.

Main definitions and results

Sigmoid as a function from ℝ to ℝ

• Real.sigmoid : the sigmoid function from ℝ to ℝ.
• Real.sigmoid_strictMono : the sigmoid function is strictly monotone.
• Real.continuous_sigmoid : the sigmoid function is continuous.
• Real.tendsto_sigmoid_atTop : the sigmoid function tends to 1 at +∞.
• Real.tendsto_sigmoid_atBot : the sigmoid function tends to 0 at -∞.
• Real.hasDerivAt_sigmoid : the derivative of the sigmoid function.
• Real.analyticAt_sigmoid : the sigmoid function is analytic at every point.

Sigmoid as a function from ℝ to I

• unitInterval.sigmoid : the sigmoid function from ℝ to I.
• unitInterval.sigmoid_strictMono : the sigmoid function is strictly monotone.
• unitInterval.continuous_sigmoid : the sigmoid function is continuous.
• unitInterval.tendsto_sigmoid_atTop : the sigmoid function tends to 1 at +∞.
• unitInterval.tendsto_sigmoid_atBot : the sigmoid function tends to 0 at -∞.

Sigmoid as an OrderEmbedding from ℝ to I

• OrderEmbedding.sigmoid : the sigmoid function as an OrderEmbedding from ℝ to I.
• Topology.isEmbedding_sigmoid : the sigmoid function from ℝ to I is a topological embedding.
• measurableEmbedding_sigmoid : the sigmoid function from ℝ to I is a measurable embedding.
• measurableEmbedding_sigmoid_comp_embeddingReal : the composition of the sigmoid function from ℝ to I with the measurable embedding from a standard Borel space α to ℝ is a measurable embedding from α to I.

Tags

sigmoid, embedding, measurable embedding, topological embedding

noncomputable def Real.sigmoid (x : ℝ) : ℝ

The sigmoid function from ℝ to ℝ.

theorem Real.sigmoid_def (x : ℝ) : x.sigmoid = (1 + exp (-x))⁻¹

@[simp]

theorem Real.sigmoid_zero : sigmoid 0 = 2⁻¹

theorem Real.sigmoid_pos (x : ℝ) : 0 < x.sigmoid

theorem Real.sigmoid_nonneg (x : ℝ) : 0 ≤ x.sigmoid

theorem Real.sigmoid_lt_one (x : ℝ) : x.sigmoid < 1

theorem Real.sigmoid_le_one (x : ℝ) : x.sigmoid ≤ 1

theorem Real.sigmoid_strictMono : StrictMono sigmoid

theorem Real.sigmoid_le_iff {a b : ℝ} : a.sigmoid ≤ b.sigmoid ↔ a ≤ b

theorem Real.sigmoid_le {a b : ℝ} : a ≤ b → a.sigmoid ≤ b.sigmoid

theorem Real.sigmoid_lt_iff {a b : ℝ} : a.sigmoid < b.sigmoid ↔ a < b

theorem Real.sigmoid_lt {a b : ℝ} : a < b → a.sigmoid < b.sigmoid

theorem Real.sigmoid_monotone : Monotone sigmoid

theorem Real.sigmoid_injective : Function.Injective sigmoid

@[simp]

theorem Real.sigmoid_inj {a b : ℝ} : a.sigmoid = b.sigmoid ↔ a = b

theorem Real.sigmoid_neg (x : ℝ) : (-x).sigmoid = 1 - x.sigmoid

theorem Real.sigmoid_mul_rexp_neg (x : ℝ) : x.sigmoid * exp (-x) = (-x).sigmoid

theorem Real.range_sigmoid : Set.range sigmoid = Set.Ioo 0 1

theorem Real.tendsto_sigmoid_atTop : Filter.Tendsto sigmoid Filter.atTop (nhds 1)

theorem Real.tendsto_sigmoid_atBot : Filter.Tendsto sigmoid Filter.atBot (nhds 0)

theorem Real.hasDerivAt_sigmoid (x : ℝ) : HasDerivAt sigmoid (x.sigmoid * (1 - x.sigmoid)) x

theorem Real.deriv_sigmoid : deriv sigmoid = fun (x : ℝ) => x.sigmoid * (1 - x.sigmoid)

theorem analyticAt_sigmoid {x : ℝ} : AnalyticAt ℝ Real.sigmoid x

theorem AnalyticAt.sigmoid {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} (fa : AnalyticAt ℝ f x) : AnalyticAt ℝ (Real.sigmoid ∘ f) x

theorem AnalyticAt.sigmoid' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} (fa : AnalyticAt ℝ f x) : AnalyticAt ℝ (fun (z : E) => (f z).sigmoid) x

theorem analyticOnNhd_sigmoid : AnalyticOnNhd ℝ Real.sigmoid Set.univ

theorem AnalyticOnNhd.sigmoid {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {s : Set E} (fs : AnalyticOnNhd ℝ f s) : AnalyticOnNhd ℝ (Real.sigmoid ∘ f) s

theorem analyticOn_sigmoid : AnalyticOn ℝ Real.sigmoid Set.univ

theorem AnalyticOn.sigmoid {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {s : Set E} (fs : AnalyticOn ℝ f s) : AnalyticOn ℝ (Real.sigmoid ∘ f) s

theorem analyticWithinAt_sigmoid {x : ℝ} {s : Set ℝ} : AnalyticWithinAt ℝ Real.sigmoid s x

theorem AnalyticWithinAt.sigmoid {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {s : Set E} {x : E} (fa : AnalyticWithinAt ℝ f s x) : AnalyticWithinAt ℝ (Real.sigmoid ∘ f) s x

theorem contDiff_sigmoid : ContDiff ℝ ⊤ Real.sigmoid

theorem ContDiff.sigmoid {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} (hf : ContDiff ℝ ⊤ f) : ContDiff ℝ ⊤ (Real.sigmoid ∘ f)

theorem differentiable_sigmoid : Differentiable ℝ Real.sigmoid

theorem Differentiable.sigmoid {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} (hf : Differentiable ℝ f) : Differentiable ℝ (Real.sigmoid ∘ f)

theorem differentiableAt_sigmoid {x : ℝ} : DifferentiableAt ℝ Real.sigmoid x

theorem DifferentiableAt.sigmoid {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} (hf : DifferentiableAt ℝ f x) : DifferentiableAt ℝ (Real.sigmoid ∘ f) x

theorem continuous_sigmoid : Continuous Real.sigmoid

theorem Continuous.sigmoid {E : Type u_1} [NormedAddCommGroup E] {f : E → ℝ} (hf : Continuous f) : Continuous (Real.sigmoid ∘ f)

noncomputable def unitInterval.sigmoid : ℝ → ↑unitInterval

The sigmoid function from ℝ to I.

theorem unitInterval.sigmoid_pos (x : ℝ) : 0 < sigmoid x

theorem unitInterval.sigmoid_lt_one (x : ℝ) : sigmoid x < 1

theorem unitInterval.sigmoid_strictMono : StrictMono sigmoid

theorem unitInterval.sigmoid_le_iff {a b : ℝ} : sigmoid a ≤ sigmoid b ↔ a ≤ b

theorem unitInterval.sigmoid_le {a b : ℝ} : a ≤ b → sigmoid a ≤ sigmoid b

theorem unitInterval.sigmoid_lt_iff {a b : ℝ} : sigmoid a < sigmoid b ↔ a < b

theorem unitInterval.sigmoid_lt {a b : ℝ} : a < b → sigmoid a < sigmoid b

theorem unitInterval.sigmoid_monotone : Monotone sigmoid

theorem unitInterval.sigmoid_injective : Function.Injective sigmoid

@[simp]

theorem unitInterval.sigmoid_inj {a b : ℝ} : sigmoid a = sigmoid b ↔ a = b

theorem unitInterval.continuous_sigmoid : Continuous sigmoid

theorem unitInterval.sigmoid_neg (x : ℝ) : sigmoid (-x) = symm (sigmoid x)

theorem unitInterval.range_sigmoid : Set.range sigmoid = Set.Ioo 0 1

theorem unitInterval.tendsto_sigmoid_atTop : Filter.Tendsto sigmoid Filter.atTop (nhds 1)

theorem unitInterval.tendsto_sigmoid_atBot : Filter.Tendsto sigmoid Filter.atBot (nhds 0)

noncomputable def OrderEmbedding.sigmoid : ℝ ↪o ↑unitInterval

The Sigmoid function as an OrderEmbedding from ℝ to I.

theorem Topology.isEmbedding_sigmoid : IsEmbedding unitInterval.sigmoid

theorem measurableEmbedding_sigmoid : MeasurableEmbedding unitInterval.sigmoid

theorem measurableEmbedding_sigmoid_comp_embeddingReal (α : Type u_2) [MeasurableSpace α] [StandardBorelSpace α] : MeasurableEmbedding (unitInterval.sigmoid ∘ MeasureTheory.embeddingReal α)