Local diffeomorphisms of the scalar field

A C^n function g : 𝕂 → 𝕂, 1 ≤ n, whose derivative vanishes nowhere is a C^n local diffeomorphism of 𝕂 (TauCeti.isLocalDiffeomorph_of_deriv_ne_zero): its differential at each point is multiplication by the nonzero number deriv g x, so the inverse function theorem for manifolds (TauCeti.isLocalDiffeomorph_of_mfderiv_eq) applies. The logistic sigmoid, a diffeomorphism of ℝ onto (0, 1), is an example.

theorem TauCeti.isLocalDiffeomorph_of_deriv_ne_zero {𝕂 : Type u_1} [RCLike 𝕂] {n : WithTop ℕ∞} {g : 𝕂 → 𝕂} (hg : ContDiff 𝕂 n g) (hn : 1 ≤ n) (hg' : ∀ (x : 𝕂), deriv g x ≠ 0) : IsLocalDiffeomorph (modelWithCornersSelf 𝕂 𝕂) (modelWithCornersSelf 𝕂 𝕂) n g

The inverse function theorem in one variable: a C^n function 𝕂 → 𝕂, 1 ≤ n, whose derivative vanishes nowhere is a C^n local diffeomorphism.

theorem TauCeti.isLocalDiffeomorph_sigmoid {n : WithTop ℕ∞} (hn : 1 ≤ n) : IsLocalDiffeomorph (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) n Real.sigmoid

The logistic sigmoid x ↦ 1 / (1 + exp (-x)) is a C^n local diffeomorphism of ℝ for every n ≥ 1.