Elementwise

Elementwise (map) Fréchet-derivative facts for Euclidean vectors.

This is the missing bridge for turning the scalar calculus lemmas in NN/Proofs/Gradients/Activation.lean into OpSpecFDerivCorrect instances for vector-valued ops (sigmoid/tanh/softplus/…).

def Proofs.Autograd.elemwiseVec {n : ℕ} (f : ℝ → ℝ) : Vec n → Vec n

Apply a scalar function f : ℝ → ℝ coordinatewise to a vector.

This is the Euclidean-space analogue of the tensor-level mapSpec.

def Proofs.Autograd.evalCLM {n : ℕ} (i : Fin n) : Vec n →L[ℝ] ℝ

Coordinate evaluation as a continuous linear map on Vec n.

@[simp]

theorem Proofs.Autograd.evalCLM_apply {n : ℕ} (i : Fin n) (x : Vec n) : (evalCLM i) x = x.ofLp i

The coordinate evaluation functional reads coordinate i.

noncomputable def Proofs.Autograd.elemwiseDerivCLM {n : ℕ} (f' : ℝ → ℝ) (x : Vec n) : Vec n →L[ℝ] Vec n

The derivative candidate for elemwiseVec f at a point x, built from a proposed scalar derivative f'.

Concretely: (elemwiseDerivCLM f' x) dx has coordinates i ↦ f'(xᵢ) * dxᵢ.

theorem Proofs.Autograd.hasFDerivAt_elemwiseVec {n : ℕ} {f f' : ℝ → ℝ} (x : Vec n) (hf : ∀ (z : ℝ), HasDerivAt f (f' z) z) : HasFDerivAt (elemwiseVec f) (elemwiseDerivCLM f' x) x

If f is differentiable everywhere with derivative f', then elemwiseVec f is Fréchet differentiable everywhere with derivative elemwiseDerivCLM f'.

theorem Proofs.Autograd.hasFDerivAt_elemwiseVec_at {n : ℕ} {f f' : ℝ → ℝ} (x : Vec n) (hf : ∀ (i : Fin n), HasDerivAt f (f' (x.ofLp i)) (x.ofLp i)) : HasFDerivAt (elemwiseVec f) (elemwiseDerivCLM f' x) x

Pointwise (at x) version of hasFDerivAt_elemwiseVec.

This is useful when the scalar HasDerivAt facts are only available at the coordinates of x.

@[simp]

theorem Proofs.Autograd.getScalar_map_spec_ofFnE {n : ℕ} (f : ℝ → ℝ) (xV : Vec n) (i : Fin n) : (TorchLean.Tensor.mapSpec 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.mapSpec 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.