DLM training as weighted regression

[GB24] [Hei24]

The weighted loss is a least-squares residual: √q-scaling embeds the training objective into EuclideanSpace ℝ (Fin m × Fin n) (weightedLoss_eq_norm_sq), identifying the ERM solutions with the least-squares solutions of the design map (isERMSolution_iff_isLeastSquares). Existence then follows from the Hilbert projection theorem via Core.exists_isLeastSquares — the normal-equations solvability of [GB24]'s appendix, with no invertibility hypothesis.

noncomputable def Processing.Lexical.Discriminative.designMap {m n d : ℕ} (data : TrainingExperience m n d) (q : FrequencyVector m) : (MeaningVec d →ₗ[ℝ] FormVec n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m × Fin n)

The √q-scaled design map: the linear embedding of candidate production maps into Euclidean event-coordinate space whose residual against scaledTarget is the weighted loss.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Processing.Lexical.Discriminative.designMap_apply {m n d : ℕ} (data : TrainingExperience m n d) (q : FrequencyVector m) (G : MeaningVec d →ₗ[ℝ] FormVec n) (p : Fin m × Fin n) : ((designMap data q) G).ofLp p = √(q p.1) * G (data.meanings p.1) p.2

noncomputable def Processing.Lexical.Discriminative.scaledTarget {m n d : ℕ} (data : TrainingExperience m n d) (q : FrequencyVector m) : EuclideanSpace ℝ (Fin m × Fin n)

The √q-scaled observed forms, as a point of Euclidean event-coordinate space.

Equations

• Processing.Lexical.Discriminative.scaledTarget data q = WithLp.toLp 2 fun (p : Fin m × Fin n) => √(q p.1) * data.forms p.1 p.2

theorem Processing.Lexical.Discriminative.weightedLoss_eq_norm_sq {m n d : ℕ} (data : TrainingExperience m n d) {q : FrequencyVector m} (hq : ∀ (i : Fin m), 0 ≤ q i) (G : MeaningVec d →ₗ[ℝ] FormVec n) : weightedLoss data q G = ‖(designMap data q) G - scaledTarget data q‖ ^ 2

The weighted loss is the squared least-squares residual of the design map against the scaled target.

theorem Processing.Lexical.Discriminative.isERMSolution_iff_isLeastSquares {m n d : ℕ} (data : TrainingExperience m n d) {q : FrequencyVector m} (hq : ∀ (i : Fin m), 0 ≤ q i) {G : MeaningVec d →ₗ[ℝ] FormVec n} : IsERMSolution data q G ↔ Core.IsLeastSquares (designMap data q) (scaledTarget data q) G

ERM solutions are exactly the least-squares solutions of the design map — the DLM training problem, seen through √q-scaling, is weighted linear regression.

theorem Processing.Lexical.Discriminative.exists_isERMSolution {m n d : ℕ} (data : TrainingExperience m n d) {q : FrequencyVector m} (hq : ∀ (i : Fin m), 0 ≤ q i) : ∃ (G : MeaningVec d →ₗ[ℝ] FormVec n), IsERMSolution data q G

ERM solutions exist for any nonnegative frequency vector, by the Hilbert projection theorem (Core.exists_isLeastSquares).

theorem Processing.Lexical.Discriminative.exists_isELSolution {m n d : ℕ} (data : TrainingExperience m n d) : ∃ (G : MeaningVec d →ₗ[ℝ] FormVec n), IsELSolution data G

Endstate solutions exist.

theorem Processing.Lexical.Discriminative.existsUnique_isERMSolution_iff {m n d : ℕ} [NeZero n] (data : TrainingExperience m n d) {q : FrequencyVector m} (hq : ∀ (i : Fin m), 0 < q i) : (∃! G : MeaningVec d →ₗ[ℝ] FormVec n, IsERMSolution data q G) ↔ Submodule.span ℝ (Set.range data.meanings) = ⊤

The trained lexicon is uniquely determined exactly when the experienced meanings span the whole meaning space — the coordinate-free form of the papers' full-column-rank condition on the closed-form solution ([GB24] appendix; [Hei24]). Below that threshold the ERM map is genuinely underdetermined (IsERMSolution.exists_apply_ne), though its fitted values never are (IsERMSolution.apply_meanings_eq).