English
For all x ∈ ℝ, smoothing does not change when replacing x by its projection onto the interval [0,1]: smoothTransition(projIcc(0,1,0≤1,x)) = smoothTransition(x).
Русский
Для любого x ∈ ℝ эффект плавного перехода одинаков как при замене x на его проекцию на отрезок [0,1]: smoothTransition(projIcc(0,1,0≤1,x)) = smoothTransition(x).
LaTeX
$$$$ \operatorname{smoothTransition}\bigl(\max(0, \min(1, x))\bigr) = \operatorname{smoothTransition}(x). $$$$
Lean4
/-- Since `Real.smoothTransition` is constant on $(-∞, 0]$ and $[1, ∞)$, applying it to the
projection of `x : ℝ` to $[0, 1]$ gives the same result as applying it to `x`. -/
@[simp]
protected theorem projIcc : smoothTransition (projIcc (0 : ℝ) 1 zero_le_one x) = smoothTransition x :=
by
refine congr_fun (IccExtend_eq_self zero_le_one smoothTransition (fun x hx => ?_) fun x hx => ?_) x
· rw [smoothTransition.zero, zero_of_nonpos hx.le]
· rw [smoothTransition.one, one_of_one_le hx.le]
