Documentation

Linglib.Processing.DiscriminativeLexicon.Normed

DLM in normed carriers #

Over finite-dimensional real normed carriers the production map is continuous, hence Lipschitz with constant its operator norm: meanings within ε of each other produce forms within ‖production‖ * ε of each other. This is the quantitative form of the papers' form–meaning isomorphy claims ([chuang-bell-tseng-baayen-2026], [lu-chuang-baayen-2026]).

References #

theorem DiscriminativeLexicon.Linear.lipschitzWith_production {F : Type u_1} {M : Type u_2} [NormedAddCommGroup F] [NormedAddCommGroup M] [NormedSpace F] [NormedSpace M] [FiniteDimensional M] (D : Linear F M) :
LipschitzWith LinearMap.toContinuousLinearMap D.production‖₊ D.production

The production map is Lipschitz with constant its operator norm.

theorem DiscriminativeLexicon.Linear.norm_production_sub_le {F : Type u_1} {M : Type u_2} [NormedAddCommGroup F] [NormedAddCommGroup M] [NormedSpace F] [NormedSpace M] [FiniteDimensional M] (D : Linear F M) {e₁ e₂ : M} {ε : } (h : e₁ - e₂ ε) :
D.production e₁ - D.production e₂ LinearMap.toContinuousLinearMap D.production * ε

Meanings within ε of each other produce forms within ‖production‖ * ε.