DLM-derived semantic-support measures

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

The semantic support measures projected from a LinearDiscriminativeLexicon's production map, specialised to the FormVec/MeaningVec carriers.

Main declarations

• semSup D s j: semantic support for form coordinate j from meaning s.
• semSupWord D s js: sum of semSup over a word's form coordinates — [GB24]'s Semantic Support for Form, [STB25]'s SemSupWord.
• semSup_add / semSup_smul / semSup_zero: @[simp] linearity lemmas in the meaning argument.

Semantic support — coordinate projection of production

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

Semantic support for form coordinate j from meaning vector s: the named binding for D.production s j ([STB25]; [GB24]'s per-triphone support).

Equations

• Processing.Lexical.Discriminative.semSup D s j = D.production s j

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 ([GB24]'s Semantic Support for Form; [STB25]'s SemSupWord).

Equations

• Processing.Lexical.Discriminative.semSupWord D s js = (List.map (Processing.Lexical.Discriminative.semSup D s) js).sum

semSup is linear in the meaning vector

Since D.production is a LinearMap, semSup D · j is a linear functional on the meaning space.

@[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

@[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

@[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

The general semSupWord_add / semSupWord_smul linearity is deferred until a consumer needs it.

@[simp]

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