Documentation

Linglib.Processing.Lexical.Discriminative.Measures

DLM-derived semantic-support measures #

[BCSBB19] [GB24] [STB25] [HCB26]

Sibling to Defs.lean and Normed.lean. Hosts the family of semantic support measures derived from a trained LinearDiscriminativeLexicon — the per-coordinate, per-word, and per-region projections of production that consumer studies have come to rely on.

What is in this file #

Carriers #

Specialised to FormVec n / MeaningVec d (i.e. Fin n → ℝ / Fin d → ℝ), the most common DLM carrier types. All current consumers (ChuangEtAl2026, LuChuangBaayen2026, Saito2025, GahlBaayen2024) use these. A Measures/EuclideanSpace.lean sibling can host inner-product-typed variants if a future consumer needs cosine similarities directly.

source
def Processing.Lexical.Discriminative.semSup {n d : ℕ} (D : LinearDiscriminativeLexicon ℝ (FormVec n) (MeaningVec d)) (s : MeaningVec d) (j : Fin n) :
ℝ

Semantic support for coordinate j of the form vector predicted from meaning vector s: semSup D s j = D.production s j.

The substrate's D.production s j already provides this directly; the named binding makes the cross-paper concept (paper §3.1 eq. 1 of [STB25]; the per-triphone support of [GB24] §3.4) grep-able.

Equations
Instances For
    source
    def Processing.Lexical.Discriminative.semSupWord {n d : ℕ} (D : LinearDiscriminativeLexicon ℝ (FormVec n) (MeaningVec d)) (s : MeaningVec d) (js : List (Fin n)) :
    ℝ

    Word-level semantic support — the sum of semSup over a word's component form coordinates. In the consumer studies' triphone- based form representation, this is the sum over the word's component triphones (paper §3.4 of [GB24] terms this Semantic Support for Form; paper §3.1 eq. 2 of [STB25] terms it SemSupWord).

    Equations
    Instances For

      semSup is linear in the meaning vector #

      Since D.production is a LinearMap, semSup D · j is a linear functional on the meaning space. Three structural lemmas (additivity, scalar-multiplication, zero) follow by map_add / map_smul / map_zero on the production map. @[simp] so consumers can rewrite linear-combination meaning vectors directly.

      source
      @[simp]
      theorem Processing.Lexical.Discriminative.semSup_add {n d : ℕ} (D : LinearDiscriminativeLexicon ℝ (FormVec n) (MeaningVec d)) (s₁ s₂ : MeaningVec d) (j : Fin n) :
      semSup D (s₁ + s₂) j = semSup D s₁ j + semSup D s₂ j
      source
      @[simp]
      theorem Processing.Lexical.Discriminative.semSup_smul {n d : ℕ} (D : LinearDiscriminativeLexicon ℝ (FormVec n) (MeaningVec d)) (c : ℝ) (s : MeaningVec d) (j : Fin n) :
      semSup D (c • s) j = c * semSup D s j
      source
      @[simp]
      theorem Processing.Lexical.Discriminative.semSup_zero {n d : ℕ} (D : LinearDiscriminativeLexicon ℝ (FormVec n) (MeaningVec d)) (j : Fin n) :
      semSup D 0 j = 0

      semSupWord zero case #

      semSupWord D 0 js = 0 follows from semSup_zero plus List.sum of the constant-zero list. The general semSupWord_add / semSupWord_smul linearity (sum of linear functionals is linear) is deferred until a consumer needs to rewrite linear-combination meaning vectors at the word level — induction on js plus ring at the cons step works once Mathlib.Tactic.Ring is imported, but no current consumer requires it.

      source
      @[simp]
      theorem Processing.Lexical.Discriminative.semSupWord_zero {n d : ℕ} (D : LinearDiscriminativeLexicon ℝ (FormVec n) (MeaningVec d)) (js : List (Fin n)) :
      semSupWord D 0 js = 0