smoothTransition — Mathlib

English

The real function smoothTransition is defined by the ratio expNegInvGlue(x) / (expNegInvGlue(x) + expNegInvGlue(1 - x)).

Русский

Реальная функция smoothTransition задана как отношение expNegInvGlue(x) к сумме expNegInvGlue(x) и expNegInvGlue(1 - x).

LaTeX

$$$\operatorname{Real.smoothTransition}(x)=\dfrac{\expNegInvGlue(x)}{\expNegInvGlue(x)+\expNegInvGlue(1-x)}$$$

Lean4

/-- An infinitely smooth function `f : ℝ → ℝ` such that `f x = 0` for `x ≤ 0`,
`f x = 1` for `1 ≤ x`, and `0 < f x < 1` for `0 < x < 1`. -/
def smoothTransition (x : ℝ) : ℝ :=
  expNegInvGlue x / (expNegInvGlue x + expNegInvGlue (1 - x))

Похожие утверждения