Elementwise

OpSpecFDerivCorrect instances for elementwise (map) ops on Euclidean vectors.

The generic coordinatewise calculus (elemwiseVec, elemwiseDerivCLM, hasFDerivAt_elemwiseVec_at) lives in NN.Proofs.Autograd.FDeriv.Core. This file turns the scalar calculus lemmas in NN/Proofs/Gradients/Activation.lean into OpSpecFDerivCorrect instances for vector-valued ops (sigmoid/tanh/softplus/…).

@[simp]

theorem Proofs.Autograd.getScalar_map_spec_ofFnE {n : ℕ} (f : ℝ → ℝ) (xV : Vec n) (i : Fin n) : (TorchLean.Tensor.map f (ofFnE xV)).getScalar i = f (xV.ofLp i)

Evaluation lemma: converting an elementwise-mapped tensor back to coordinates agrees with applying f to the corresponding Euclidean coordinate.

@[simp]

theorem Proofs.Autograd.getScalarE_map_spec_ofFnE_eq_elemwiseVec {n : ℕ} (f : ℝ → ℝ) (xV : Vec n) : getScalarE (TorchLean.Tensor.map f (ofFnE xV)) = elemwiseVec f xV

Vectorized form of the previous lemma: mapping f over a tensor is elemwiseVec f on vectors.

This is the statement that lets an elementwise operation's derivative be proved once on EuclideanSpace and then transported to every tensor of vector shape.

noncomputable def Proofs.Autograd.OpSpecFDerivCorrect.exp {n : ℕ} : OpSpecFDerivCorrect n n

exp as an OpSpecFDerivCorrect instance (elementwise Real.exp).

noncomputable def Proofs.Autograd.OpSpecFDerivCorrect.square {n : ℕ} : OpSpecFDerivCorrect n n

square as an OpSpecFDerivCorrect instance (elementwise x ↦ x^2).

noncomputable def Proofs.Autograd.OpSpecFDerivCorrect.sinh {n : ℕ} : OpSpecFDerivCorrect n n

sinh as an OpSpecFDerivCorrect instance (elementwise).

noncomputable def Proofs.Autograd.OpSpecFDerivCorrect.cosh {n : ℕ} : OpSpecFDerivCorrect n n

cosh as an OpSpecFDerivCorrect instance (elementwise).

noncomputable def Proofs.Autograd.OpSpecFDerivCorrect.tanh {n : ℕ} : OpSpecFDerivCorrect n n

tanh as an OpSpecFDerivCorrect instance (elementwise).

noncomputable def Proofs.Autograd.OpSpecFDerivCorrect.sigmoid {n : ℕ} : OpSpecFDerivCorrect n n

sigmoid as an OpSpecFDerivCorrect instance (elementwise).

noncomputable def Proofs.Autograd.OpSpecFDerivCorrect.softplus {n : ℕ} : OpSpecFDerivCorrect n n

softplus as an OpSpecFDerivCorrect instance (elementwise).

noncomputable def Proofs.Autograd.OpSpecFDerivCorrect.silu {n : ℕ} : OpSpecFDerivCorrect n n

SiLU as an OpSpecFDerivCorrect instance (elementwise).

noncomputable def Proofs.Autograd.OpSpecFDerivCorrect.gelu {n : ℕ} : OpSpecFDerivCorrect n n

Tanh-approximate GELU as an OpSpecFDerivCorrect instance (elementwise).

noncomputable def Proofs.Autograd.OpSpecFDerivCorrect.safeLog {n : ℕ} (ε : ℝ) (hε : 0 < ε) : OpSpecFDerivCorrect n n

safeLog as an OpSpecFDerivCorrect instance (elementwise), assuming ε > 0.

This is the differentiable calculus fact; the corresponding dot-level VJP correctness lives in NN.Proofs.Autograd.Core.RealCorrectness.

noncomputable def Proofs.Autograd.OpSpecFDerivCorrect.smoothAbs {n : ℕ} (ε : ℝ) (hε : 0 < ε) : OpSpecFDerivCorrect n n

smoothAbs as an OpSpecFDerivCorrect instance (elementwise), assuming ε > 0.

This is a differentiable approximation to abs.