First-Order Optimizer Relations

Relations between distinct first-order optimizer updates.

This is the tensor-facing layer: the statements are phrased over TorchLean.Tensor and the executable operator dictionary Spec.Context. When we want ordinary algebraic simplification, such as proving that a zero weight-decay AdamW update is the same parameter update as Adam, we specialize to ℝ, where mathlib provides the ring laws.

Context α gives us executable operators, but not algebraic laws like x * 0 = 0.

Optimizer-relationship theorems (AdamW → Adam, L2 vs weight decay, etc.) therefore live most naturally over proof backends like ℝ where the laws are available from Mathlib.

theorem Optim.AdamW.update_weight_decay_zero_parameters_eq_adam_real {s : Spec.Shape} (state : State ℝ s) (parameters gradients : TorchLean.Tensor ℝ s) (hwd : state.weightDecay = 0) : (update state parameters gradients).parameters = (Adam.update { learningRate := state.learningRate, beta1 := state.beta1, beta2 := state.beta2, epsilon := state.epsilon, firstMoment := state.firstMoment, secondMoment := state.secondMoment, stepCount := state.stepCount } parameters gradients).parameters

AdamW reduces to Adam when weightDecay = 0 (parameter-update equality), over ℝ.