Lax132576.LeftDistance

Left distance and bounded variation

concepts/Lax132576/LeftDistance.lean · lax-132576

definition

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

In the paper

page 71 of the paper of lax-157538, Transducers

Definition

The left distance $\|w_1, w_2\|$ of two strings (Definition B.4.7 of Transducers) is the smallest $k$ such that the strings decompose as

w_1 = v\,v_1, \qquad w_2 = v\,v_2 \qquad \text{with } |v_1|, |v_2| \le k,

i.e. the larger of the two lengths that remain after the longest common prefix has been removed. It measures how far apart two outputs of a transducer can be allowed to be after reading the same input. A partial function $f$ has bounded variation if for all $w_1, w_2$ the left distances $\|f(w w_1), f(w w_2)\|$ are bounded, $w$ ranging over the strings for which both values are defined (Theorem B.4.8); for a total function, the relation

w_1 \sim w_2 \quad\Longleftrightarrow\quad \sup_w \|f(w w_1), f(w w_2)\| < \infty

is an equivalence relation on input strings, and its index is what characterises the rational functions (Theorem B.4.13).

Lean source view on GitHub

1	import Mathlib.Order.ConditionallyCompleteLattice.Basic
2	import Mathlib.Data.Nat.Lattice
3
4	/-!
5	---
6	title: Left distance and bounded variation
7	type: definition
8	---
9	The left distance $\\|w_1, w_2\\|$ of two strings (Definition B.4.7 of
10	Transducers) is the smallest $k$ such that the strings decompose as
11	$w_1 = v\,v_1, \qquad w_2 = v\,v_2 \qquad \text{with } \|v_1\|, \|v_2\| \le k,$
12	i.e. the larger of the two lengths that remain after the longest common prefix
13	has been removed. It measures how far apart two outputs of a transducer can be
14	allowed to be after reading the same input. A partial function $f$ has
15	bounded variation if for all $w_1, w_2$ the left distances
16	$\\|f(w w_1), f(w w_2)\\|$ are bounded, $w$ ranging over the strings for which
17	both values are defined (Theorem B.4.8); for a total function, the relation
18	$w_1 \sim w_2 \quad\Longleftrightarrow\quad \sup_w \\|f(w w_1), f(w w_2)\\| < \infty$
19	is an equivalence relation on input strings, and its index is what
20	characterises the rational functions (Theorem B.4.13).
21
22	# Formalization notes
23
24	`leftDist` is the infimum of the set of admissible `k`, which is nonempty
25	(`max \|w₁\| \|w₂\|` always works), so the infimum is attained and the convention
26	`sInf ∅ = 0` is never exercised. `BoundedVarRel f` is the relation `∼`, and
27	`BoundedVariation` the property of a partial function.
28	-/
29
30	namespace Lax132576.LeftDistance
31
32	/-- The left distance `‖w₁, w₂‖`: the least `k` such that `w₁ = v v₁` and
33	`w₂ = v v₂` with `\|v₁\|, \|v₂\| ≤ k`. -/
34	noncomputable def leftDist {B : Type} (w₁ w₂ : List B) : ℕ :=
35	sInf {k : ℕ \| ∃ v v₁ v₂ : List B,
36	w₁ = v ++ v₁ ∧ w₂ = v ++ v₂ ∧ v₁.length ≤ k ∧ v₂.length ≤ k}
37
38	/-- The relation `w₁ ∼ w₂` of Theorem B.4.13: the left distances
39	`‖f (w w₁), f (w w₂)‖` are bounded uniformly in `w`. -/
40	def BoundedVarRel {A B : Type} (f : List A → List B) (w₁ w₂ : List A) : Prop :=
41	∃ K : ℕ, ∀ w : List A, leftDist (f (w ++ w₁)) (f (w ++ w₂)) ≤ K
42
43	/-- A partial function has bounded variation if for all `w₁, w₂` the left distances
44	`‖f (w w₁), f (w w₂)‖` are bounded, over the `w` for which both are defined. -/
45	def BoundedVariation {A B : Type} (f : List A → Option (List B)) : Prop :=
46	∀ w₁ w₂ : List A, ∃ K : ℕ, ∀ (w : List A) (v₁ v₂ : List B),
47	f (w ++ w₁) = some v₁ → f (w ++ w₂) = some v₂ → leftDist v₁ v₂ ≤ K
48
49	end Lax132576.LeftDistance
50

Formalization notes

$leftDist$ is the infimum of the set of admissible $k$ , which is nonempty ( $max |w₁| |w₂|$ always works), so the infimum is attained and the convention $sInf ∅ = 0$ is never exercised. $BoundedVarRel f$ is the relation $∼$ , and $BoundedVariation$ the property of a partial function.

Builds on

none

Used by

From Mathlib

Community review

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

0 comments

Loading discussion…

Lax Lean Archive