Scalar Activation Derivatives

Real calculus lemmas (HasDerivAt, etc.) for scalar activation functions, used as building blocks for TorchLean autograd correctness proofs. These identify derivatives of the real specifications, not the behavior of native kernels.

Related PyTorch operators

The operator references below give context for the formulas. Native evaluation, rounding, and implementation-specific branches are outside these exact-real theorems.

• ReLU: torch.relu / torch.nn.functional.relu https://pytorch.org/docs/stable/generated/torch.relu.html https://pytorch.org/docs/stable/generated/torch.nn.functional.relu.html
• Leaky ReLU: torch.nn.functional.leaky_relu https://pytorch.org/docs/stable/generated/torch.nn.functional.leaky_relu.html
• Sigmoid (logistic): torch.sigmoid https://pytorch.org/docs/stable/generated/torch.sigmoid.html
• Tanh: torch.tanh https://pytorch.org/docs/stable/generated/torch.tanh.html
• Softplus: torch.nn.functional.softplus https://pytorch.org/docs/stable/generated/torch.nn.functional.softplus.html
• SiLU / Swish: torch.nn.functional.silu https://pytorch.org/docs/stable/generated/torch.nn.functional.silu.html
• ELU: torch.nn.functional.elu https://pytorch.org/docs/stable/generated/torch.nn.functional.elu.html
• GELU: torch.nn.functional.gelu(..., approximate="tanh") https://pytorch.org/docs/stable/generated/torch.nn.functional.gelu.html
• Hyperbolic sine/cosine: torch.sinh, torch.cosh https://pytorch.org/docs/stable/generated/torch.sinh.html https://pytorch.org/docs/stable/generated/torch.cosh.html

The ReLU, leaky-ReLU, and ELU theorems assume x ≠ 0. ReLU has a kink there; leaky ReLU and ELU are differentiable there when their slope parameter is 1, but these statements do not cover that case.

theorem Proofs.relu_deriv_correct (x : ℝ) (h : x ≠ 0) : HasDerivAt Activation.Math.reluSpec (Activation.Math.reluDerivSpec x) x

Correctness of the ReLU derivative spec away from the kink at 0.

PyTorch note: torch.relu uses a subgradient convention at 0; in this file we avoid that subtlety by assuming x ≠ 0.

theorem Proofs.leaky_relu_deriv_correct (x : ℝ) (h : x ≠ 0) (αₗ : ℝ) : αₗ > 0 → HasDerivAt (fun (x : ℝ) => Activation.Math.leakyReluSpec x αₗ) (Activation.Math.leakyReluDerivSpec x αₗ) x

Correctness of the leaky-ReLU derivative spec away from the kink at 0.

PyTorch correspondence: torch.nn.functional.leaky_relu(x, negative_slope = αₗ) with αₗ > 0.

theorem Proofs.square_deriv_correct (x : ℝ) : HasDerivAt (fun (y : ℝ) => y * y) (2 * x) x

Correctness of the square derivative spec: d/dx x^2 = 2x.

theorem Proofs.sinh_deriv_correct (x : ℝ) : HasDerivAt Activation.Math.sinhSpec (Activation.Math.sinhDerivSpec x) x

Correctness of the hyperbolic-sine derivative spec: sinh' = cosh.

theorem Proofs.cosh_deriv_correct (x : ℝ) : HasDerivAt Activation.Math.coshSpec (Activation.Math.coshDerivSpec x) x

Correctness of the hyperbolic-cosine derivative spec: cosh' = sinh.

theorem Proofs.expm1_spec_eq_exp_sub_one (x : ℝ) : Activation.Math.expm1Spec x = Real.exp x - 1

The compensated exponential difference agrees with exp x - 1 over the reals.

theorem Proofs.elu_deriv_correct (x α : ℝ) (h : x ≠ 0) : HasDerivAt (fun (y : ℝ) => Activation.Math.eluSpec y α) (Activation.Math.eluDerivSpec x α) x

Correctness of the ELU derivative spec away from the kink at 0.

PyTorch correspondence: torch.nn.functional.elu(x, alpha = α). For arbitrary α, the left derivative at 0 is α and the right derivative is 1, so the clean reusable statement is the pointwise theorem away from 0.

theorem Proofs.sigmoid_eq_inv_exp (x : ℝ) : Activation.Math.sigmoidSpec x = (1 + Real.exp (-x))⁻¹

Both evaluation branches of sigmoid define (1 + exp (-x))⁻¹ over the reals.

The negative branch multiplies numerator and denominator by exp x. This identity lets the calculus proofs use one smooth expression, including at the branch boundary x = 0.

theorem Proofs.sigmoid_spec_nonneg (x : ℝ) : 0 ≤ Activation.Math.sigmoidSpec x

The real sigmoid is nonnegative.

theorem Proofs.sigmoid_spec_le_one (x : ℝ) : Activation.Math.sigmoidSpec x ≤ 1

The real sigmoid is at most 1.

theorem Proofs.sigmoid_eq_exp_div (x : ℝ) : Activation.Math.sigmoidSpec x = Real.exp x / (1 + Real.exp x)

Sigmoid also equals exp x / (1 + exp x) over the reals.

This form is the negative-input evaluation branch and the derivative obtained by differentiating log (1 + exp x).

theorem Proofs.sigmoid_deriv_spec_eq (x : ℝ) : Activation.Math.sigmoidDerivSpec x = Activation.Math.sigmoidSpec x * (1 - Activation.Math.sigmoidSpec x)

The decaying-exponential slope is the usual real sigmoid derivative.

theorem Proofs.sigmoid_deriv_correct (x : ℝ) : HasDerivAt Activation.Math.sigmoidSpec (Activation.Math.sigmoidDerivSpec x) x

Correctness of the sigmoid derivative spec.

PyTorch correspondence: torch.sigmoid.

theorem Proofs.sigmoid_deriv_spec_deriv_correct (x : ℝ) : HasDerivAt Activation.Math.sigmoidDerivSpec (Activation.Math.sigmoidDerivSpec x * (1 - 2 * Activation.Math.sigmoidSpec x)) x

Differentiating σ(x)(1 - σ(x)) gives σ'(x)(1 - 2σ(x)).

This is the scalar second derivative used when a sigmoid VJP is evaluated over dual numbers. The real identity holds at zero as well as on either evaluation branch.

theorem Proofs.logisticSpec_eq_sigmoidSpec (x : ℝ) : Activation.Math.logisticSpec x = Activation.Math.sigmoidSpec x

Over the reals the logistic formula exp x / (exp x + 1) is the sigmoid, despite their different floating-point evaluation schedules.

theorem Proofs.logistic_deriv_correct (x : ℝ) : HasDerivAt Activation.Math.logisticSpec (Activation.Math.logisticDerivSpec x) x

Correctness of the derivative spec for Activation.Math.logisticSpec.

This is the scalar logistic formula exp x / (exp x + 1). It is not named softmax: a one-entry softmax is always 1, while TorchLean's actual axis-normalizing softmax is the tensor-level Activation.softmaxSpec in NN/Spec/Layers/Activation.lean. Over the reals it is the sigmoid (logisticSpec_eq_sigmoidSpec). Its output-form derivative equals the input-based sigmoid slope by sigmoid_deriv_spec_eq, so correctness follows from sigmoid_deriv_correct.

theorem Proofs.contDiff_tanh {n : WithTop ℕ∞} : ContDiff ℝ n Real.tanh

Real tanh is smooth at every order because its cosh denominator never vanishes.

theorem Proofs.tanh_exp_eq (x : ℝ) : Real.tanh x = (Real.exp x - Real.exp (-x)) / (Real.exp x + Real.exp (-x))

tanh in terms of exp.

Mathlib states Real.sinh and Real.cosh in exponential form (Real.sinh_eq, Real.cosh_eq); the common factor 1 / 2 cancels in the quotient.

theorem Proofs.tanh_deriv_spec_eq (x : ℝ) : Activation.Math.tanhDerivSpec x = 1 - Real.tanh x * Real.tanh x

Squaring the scaled reciprocal cosh preserves the exact real tanh derivative.

theorem Proofs.tanh_deriv_correct (x : ℝ) : HasDerivAt Activation.Math.tanhSpec (Activation.Math.tanhDerivSpec x) x

Correctness of the tanh derivative spec.

PyTorch correspondence: torch.tanh.

theorem HasDerivAt.tanh {f : ℝ → ℝ} {f' x : ℝ} (hf : HasDerivAt f f' x) : HasDerivAt (fun (y : ℝ) => Real.tanh (f y)) ((1 - Real.tanh (f x) * Real.tanh (f x)) * f') x

The real tanh chain rule, using the same derivative expression as the runtime.

theorem Proofs.gelu_deriv_correct (x : ℝ) : HasDerivAt Activation.Math.geluSpec (Activation.Math.geluDerivSpec x) x

Correctness of the tanh-approximate GELU derivative spec.

PyTorch correspondence: torch.nn.functional.gelu(x, approximate = "tanh"). The proof follows the product rule for x * (1 + tanh(c * (x + k*x^3))) / 2, plus the chain rule through the tanh inner polynomial.

theorem Proofs.log1p_spec_eq_log_one_add (x : ℝ) : Activation.Math.log1pSpec x = Real.log (1 + x)

The compensated formula agrees with log(1 + x) over the reals.

theorem Proofs.softplus_spec_eq_log_one_add_exp (x : ℝ) : Activation.Math.softplusSpec x = Real.log (1 + Real.exp x)

The branch-stable real softplus specification is extensionally log (1 + exp x).

theorem Proofs.softplus_deriv_correct (x : ℝ) : HasDerivAt Activation.Math.softplusSpec (Activation.Math.softplusDerivSpec x) x

Correctness of the softplus derivative spec.

PyTorch correspondence: torch.nn.functional.softplus.

theorem Proofs.softplus_deriv_spec_deriv_correct (x : ℝ) : HasDerivAt Activation.Math.softplusDerivSpec (Activation.Math.sigmoidDerivSpec x) x

The softplus derivative is sigmoid, so its derivative is σ(x)(1 - σ(x)) at every real input. This supplies the second-derivative identity without differentiating the branch test.

theorem Proofs.swish_spec_eq_mul_sigmoid (x : ℝ) : Activation.Math.swishSpec x = x * Activation.Math.sigmoidSpec x

Splitting the negative exponential does not change the real SiLU function.

theorem Proofs.swish_deriv_spec_eq (x : ℝ) : Activation.Math.swishDerivSpec x = Activation.Math.sigmoidSpec x + x * Activation.Math.sigmoidDerivSpec x

The split-exponential slope is the real product-rule derivative of SiLU.

theorem Proofs.silu_deriv_correct (x : ℝ) : HasDerivAt Activation.Math.swishSpec (Activation.Math.swishDerivSpec x) x

Correctness of the SiLU derivative spec.

silu(x) = x * sigmoid(x), so the proof is just the product rule plus the already-proved sigmoid derivative. This is the scalar calculus fact used by the tensor-level VJP proof bridge.

theorem Proofs.safe_log_deriv_correct (x ε : ℝ) (hε : 0 < ε) : HasDerivAt (fun (y : ℝ) => Activation.Math.safeLogSpec y ε) (Activation.Math.safeLogDerivSpec x ε) x

Correctness of the safeLog derivative spec (a smooth log surrogate).

safeLog is not a standard PyTorch primitive; conceptually it is “log-like but always defined” using softplus to avoid a strict-positivity side condition.

Related PyTorch primitives: https://pytorch.org/docs/stable/generated/torch.log.html

theorem Proofs.smooth_abs_spec_eq_sqrt (x ε : ℝ) (hε : 0 < ε) : Activation.Math.smoothAbsSpec x ε = √(x * x + ε)

Scaling before squaring preserves the real smooth-absolute-value function.

theorem Proofs.smooth_abs_deriv_correct (x ε : ℝ) (hε : 0 < ε) : HasDerivAt (fun (y : ℝ) => Activation.Math.smoothAbsSpec y ε) (Activation.Math.smoothAbsDerivSpec x ε) x

For positive ε, sqrt(x² + ε) is differentiable with derivative x / sqrt(x² + ε).