DLM in normed carriers

[BCSBB19] [CBTB26] [LCB26] [HCB26]

Over finite-dimensional real normed carriers the DLM's maps are automatically continuous, so the papers' quantitative form-meaning isomorphism claims can be stated via operator norms.

Main declarations

• dlm_lipschitz_production / dlm_lipschitz_comprehension: each map is Lipschitz with constant its operator norm.
• dlm_neighbor_centroids_imply_neighbor_contours: meanings within ε produce forms within ‖production‖ * ε.
• LinearDiscriminativeLexicon.IsMeaningApproxIso / IsFormApproxIso: approximate-inverse round-trip properties.

Implementation notes

Lipschitz theorems require [FiniteDimensional ℝ ·] on the relevant map's source so LinearMap.toContinuousLinearMap applies. The carrier fixes the norm in the bound: Fin n → ℝ carries the sup norm, which suffices for direction-of-effect arguments; studies needing the Euclidean norm (e.g. for cosine-similarity statements) should use EuclideanSpace ℝ (Fin n).

Lipschitz continuity of the production map

theorem Processing.Lexical.Discriminative.dlm_lipschitz_production {F : Type u_1} {M : Type u_2} [NormedAddCommGroup F] [NormedAddCommGroup M] [NormedSpace ℝ F] [NormedSpace ℝ M] [FiniteDimensional ℝ M] (D : LinearDiscriminativeLexicon ℝ F M) (e₁ e₂ : M) : ‖D.production e₁ - D.production e₂‖ ≤ ‖LinearMap.toContinuousLinearMap D.production‖ * ‖e₁ - e₂‖

The production map is Lipschitz with constant its operator norm.

theorem Processing.Lexical.Discriminative.dlm_lipschitz_comprehension {F : Type u_1} {M : Type u_2} [NormedAddCommGroup F] [NormedAddCommGroup M] [NormedSpace ℝ F] [NormedSpace ℝ M] [FiniteDimensional ℝ F] (D : LinearDiscriminativeLexicon ℝ F M) (f₁ f₂ : F) : ‖D.comprehension f₁ - D.comprehension f₂‖ ≤ ‖LinearMap.toContinuousLinearMap D.comprehension‖ * ‖f₁ - f₂‖

Dual of dlm_lipschitz_production for the form → meaning direction.

Neighbor preservation

theorem Processing.Lexical.Discriminative.dlm_neighbor_centroids_imply_neighbor_contours {F : Type u_1} {M : Type u_2} [NormedAddCommGroup F] [NormedAddCommGroup M] [NormedSpace ℝ F] [NormedSpace ℝ M] [FiniteDimensional ℝ M] (D : LinearDiscriminativeLexicon ℝ F M) {e₁ e₂ : M} {ε : ℝ} (h : ‖e₁ - e₂‖ ≤ ε) : ‖D.production e₁ - D.production e₂‖ ≤ ‖LinearMap.toContinuousLinearMap D.production‖ * ε

Neighbor centroids → neighbor contours: meanings within ε of each other produce forms within ‖production‖ * ε of each other.

Approximate-inverse / form-meaning ε-isomorphism

def Processing.Lexical.Discriminative.LinearDiscriminativeLexicon.IsMeaningApproxIso {F : Type u_1} {M : Type u_2} [NormedAddCommGroup F] [NormedAddCommGroup M] [NormedSpace ℝ F] [NormedSpace ℝ M] (D : LinearDiscriminativeLexicon ℝ F M) (ε : ℝ) : Prop

D is an ε-approximate isomorphism on the meaning side: every round-trip comprehension (production e) returns within ε of e.

Equations

• D.IsMeaningApproxIso ε = ∀ (e : M), ‖D.comprehension (D.production e) - e‖ ≤ ε

def Processing.Lexical.Discriminative.LinearDiscriminativeLexicon.IsFormApproxIso {F : Type u_1} {M : Type u_2} [NormedAddCommGroup F] [NormedAddCommGroup M] [NormedSpace ℝ F] [NormedSpace ℝ M] (D : LinearDiscriminativeLexicon ℝ F M) (ε : ℝ) : Prop

Dual of IsMeaningApproxIso: every round-trip production (comprehension f) returns within ε of f.

Equations

• D.IsFormApproxIso ε = ∀ (f : F), ‖D.production (D.comprehension f) - f‖ ≤ ε

theorem Processing.Lexical.Discriminative.LinearDiscriminativeLexicon.isMeaningApproxIso_zero_iff {F : Type u_1} {M : Type u_2} [NormedAddCommGroup F] [NormedAddCommGroup M] [NormedSpace ℝ F] [NormedSpace ℝ M] (D : LinearDiscriminativeLexicon ℝ F M) : D.IsMeaningApproxIso 0 ↔ ∀ (e : M), D.comprehension (D.production e) = e

The ε = 0 case of IsMeaningApproxIso: comprehension is a left inverse of production.