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/…).

noncomputable 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 map_spec.

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

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.toVec_map_spec_ofVecE {n : ℕ} (f : ℝ → ℝ) (xV : Vec n) (i : Fin n) : TensorAlgebra.toVec (Spec.Tensor.mapSpec f (ofVecE xV)) i = f (xV.ofLp i)

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

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

safe_log 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

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

This is a differentiable approximation to abs.