The Widrow-Hoff (LMS) learning rule

[WH60] [RW72]

The delta rule for a linear map between real coordinate spaces: on observing an input-output pair (x, y), add the rank-one error-driven correction x' ↦ ⟨x, x'⟩ • (y − W x), scaled by a learning rate. On binary cue vectors with uniform salience one step reproduces one Rescorla-Wagner trial (whUpdate_single_eq_rescorlaWagner_update) — Widrow-Hoff is the real-valued member of the error-driven family.

Main declarations

• whCorrection, whUpdate: the correction and the η-scaled step.
• whUpdate_eq_self_iff: a step fixes W iff its correction vanishes.
• sum_whCorrection_eq_zero_iff: the orthogonality principle — the weighted total correction vanishes iff the residuals are orthogonal to every input direction.
• whUpdate_single_eq_rescorlaWagner_update: on binary cues with uniform salience a Widrow-Hoff step is a Core.RescorlaWagner trial.
• whUpdate_single_eq_self_of_blocked: blocking transfers through the specialization; overshadowing does not (non-uniform salience has no channel in binary cue coding).

def Core.whCorrection {k n : ℕ} (x : Fin k → ℝ) (y : Fin n → ℝ) (W : (Fin k → ℝ) →ₗ[ℝ] Fin n → ℝ) : (Fin k → ℝ) →ₗ[ℝ] Fin n → ℝ

The Widrow-Hoff correction on observing (x, y) is the rank-one error-driven update direction x' ↦ ⟨x', x⟩ • (y − W x) ([WH60]'s xᵀ(y − ŷ)).

Equations

• Core.whCorrection x y W = (Fintype.linearCombination ℝ x).smulRight (y - W x)

@[simp]

theorem Core.whCorrection_apply {k n : ℕ} (x : Fin k → ℝ) (y : Fin n → ℝ) (W : (Fin k → ℝ) →ₗ[ℝ] Fin n → ℝ) (x' : Fin k → ℝ) : (whCorrection x y W) x' = (∑ l : Fin k, x' l * x l) • (y - W x)

def Core.whUpdate {k n : ℕ} (η : ℝ) (x : Fin k → ℝ) (y : Fin n → ℝ) (W : (Fin k → ℝ) →ₗ[ℝ] Fin n → ℝ) : (Fin k → ℝ) →ₗ[ℝ] Fin n → ℝ

One Widrow-Hoff step on the observation (x, y) with learning rate η.

Equations

• Core.whUpdate η x y W = W + η • Core.whCorrection x y W

theorem Core.whUpdate_eq_self_iff {k n : ℕ} {η : ℝ} (hη : η ≠ 0) (x : Fin k → ℝ) (y : Fin n → ℝ) (W : (Fin k → ℝ) →ₗ[ℝ] Fin n → ℝ) : whUpdate η x y W = W ↔ whCorrection x y W = 0

A step fixes W iff the observation's correction vanishes.

theorem Core.sum_whCorrection_eq_zero_iff {k n m : ℕ} (x : Fin m → Fin k → ℝ) (y : Fin m → Fin n → ℝ) (q : Fin m → ℝ) (W : (Fin k → ℝ) →ₗ[ℝ] Fin n → ℝ) : ∑ i : Fin m, q i • whCorrection (x i) (y i) W = 0 ↔ ∀ (j : Fin n) (w : (Fin k → ℝ) →ₗ[ℝ] ℝ), ∑ i : Fin m, q i * ((W (x i) j - y i j) * w (x i)) = 0

By the orthogonality principle for the Widrow-Hoff rule ([WH60]), the weighted total correction over a family of observations vanishes — the rule is at a fixed point in expectation — iff every weighted residual column is orthogonal to every linear functional of the inputs. The equilibrium condition is order-invariant by construction, whereas the incremental trajectory is order- and rate-dependent.

theorem Core.whUpdate_single_eq_rescorlaWagner_update {k : ℕ} (rw : RescorlaWagner (Fin k)) (hsal : ∀ (c : Fin k), rw.salience c = 1) (present : Finset (Fin k)) (V : Fin k → ℝ) (l : Fin k) : (whUpdate rw.learnRate (fun (c : Fin k) => if c ∈ present then 1 else 0) (fun (x : Fin 1) => rw.maxCond) ((Fintype.linearCombination ℝ V).smulRight fun (x : Fin 1) => 1)) (Pi.single l 1) 0 = rw.update present V l

On a binary cue vector with uniform salience, one Widrow-Hoff step reproduces one Rescorla-Wagner trial, reading cue l's weight off the map at the l-th basis vector ([RW72]). Non-uniform salience has no channel in binary cue coding, so overshadowing is out of scope while blocking transfers (whUpdate_single_eq_self_of_blocked).

theorem Core.whUpdate_single_eq_self_of_blocked {k : ℕ} (rw : RescorlaWagner (Fin k)) (hsal : ∀ (c : Fin k), rw.salience c = 1) (present : Finset (Fin k)) (V : Fin k → ℝ) (l : Fin k) (h_total : ∑ c ∈ present, V c = rw.maxCond) : (whUpdate rw.learnRate (fun (c : Fin k) => if c ∈ present then 1 else 0) (fun (x : Fin 1) => rw.maxCond) ((Fintype.linearCombination ℝ V).smulRight fun (x : Fin 1) => 1)) (Pi.single l 1) 0 = V l

When the outcome is already fully predicted on the trial, the Widrow-Hoff step leaves every cue weight unchanged — blocking transfers through the specialization, as in Core.RescorlaWagner.no_learning_at_equilibrium ([Ell06]).