Model.lean`

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

def OAI.TreeEdit.BinaryLower.deficit line 11
Source documentation
The one-sided deficit r_n, used on pairs of length n.
```
def deficit {α : Type u} (n : ℕ) (x y : List α) : ℕ := n - lcs x y
```
Mentions: OAI.TreeEdit.lcs
def OAI.TreeEdit.BinaryLower.finiteL1Distance line 14
Source documentation
The usual ℓ₁ distance in finite dimension, not the sup norm on a Pi type.
```
def finiteL1Distance {M : ℕ} (x y : Fin M → ℝ) : ℝ :=
…
```
def OAI.TreeEdit.BinaryLower.distortion line 19
Source documentation
Product of the two maximal ratios. On the finite nontrivial metric spaces used below each displayed supremum is a maximum.
Distinct definitions of this name: ComparatorChallenges/BinaryEditLower.lean:30 (different declaration text). Qualify references as OAI.TreeEdit.BinaryLower.distortion@path.
```
def distortion {X : Type u} (ρ : X → X → ℝ) (f : X → RealL1) : ℝ :=
…
```
Mentions: OAI.TreeEdit.RealL1
def OAI.TreeEdit.BinaryLower.c1 line 25
Source documentation
Infimum over every injective map into the full real sequence space ℓ₁; there is no dimension or computability restriction.
Distinct definitions of this name: ComparatorChallenges/BinaryEditLower.lean:35 (different declaration text). Qualify references as OAI.TreeEdit.BinaryLower.c1@path.
```
def c1 (X : Type u) (ρ : X → X → ℝ) : ℝ :=
…
```
abbrev OAI.TreeEdit.BinaryLower.WordsLE line 29
Source documentation
Words of length at most the specified cap.
```
abbrev WordsLE (α : Type u) (d : ℕ) := {x : List α // x.length ≤ d}
```
def OAI.TreeEdit.BinaryLower.alphabetDistortion line 32
Source documentation
Distortion of the ordinary edit metric on the all-length capped domain.
```
def alphabetDistortion (α : Type u) (d : ℕ) : ℝ :=
…
```
def OAI.TreeEdit.BinaryLower.binarySetDistortion line 36
Source documentation
Distortion of a finite collection of equal-length binary words.
Distinct definitions of this name: ComparatorChallenges/BinaryEditLower.lean:38 (different declaration text). Qualify references as OAI.TreeEdit.BinaryLower.binarySetDistortion@path.
```
def binarySetDistortion {n : ℕ} (W : Finset (Word Bool n)) : ℝ :=
…
```
Mentions: OAI.TreeEdit.Word
def OAI.TreeEdit.BinaryLower.alphabetDistortionSup line 43
Source documentation
Supremum over finite alphabets of cardinality at least two, represented by canonical alphabets Fin K. Relabeling invariance identifies this with the source's supremum over all finite alphabets.
```
def alphabetDistortionSup (d : ℕ) : ℝ :=
…
```
def OAI.TreeEdit.BinaryLower.growth line 47
Source documentation
Natural-logarithm scale of all three asymptotic endpoints.
Distinct definitions of this name: ComparatorChallenges/BinaryEditLower.lean:42 (different declaration text). Qualify references as OAI.TreeEdit.BinaryLower.growth@path.
```
def growth (c : ℝ) (d : ℕ) : ℝ :=
…
```