Model.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

inductive OAI.TreeEdit.EditStep line 10

Source documentation

A single unit-cost insertion, deletion or substitution, at any position.

Also declared: ComparatorChallenges/BinaryEditLower.lean:10 (same declaration text), ComparatorChallenges/TreeEdit.lean:10 (same declaration text).

inductive EditStep {α : Type u} : List α → List α → Prop
  | insert (p q : List α) (a : α) : EditStep (p ++ q) (p ++ a :: q)
  | delete (p q : List α) (a : α) : EditStep (p ++ a :: q) (p ++ q)
  | substitute (p q : List α) (a b : α) : EditStep (p ++ a :: q) (p ++ b :: q)

/-- A script of precisely `n` edits. There is no restriction on its intermediate lengths. -/

inductive OAI.TreeEdit.EditScript line 16
Source documentation
A script of precisely n edits. There is no restriction on its intermediate lengths.
Also declared: ComparatorChallenges/BinaryEditLower.lean:16 (same declaration text), ComparatorChallenges/TreeEdit.lean:16 (same declaration text).
```
inductive EditScript {α : Type u} : List α → List α → ℕ → Prop
  | nil (x : List α) : EditScript x x 0
  | cons {x y z : List α} {n : ℕ} :
      EditStep x y → EditScript y z n → EditScript x z (n + 1)

/-- Ordinary unit-cost edit distance. The set is nonempty (delete then insert). -/
```
Mentions: OAI.TreeEdit.EditStep
def OAI.TreeEdit.ed line 22
Source documentation
Ordinary unit-cost edit distance. The set is nonempty (delete then insert).
Also declared: ComparatorChallenges/BinaryEditLower.lean:21 (same declaration text), ComparatorChallenges/TreeEdit.lean:22 (same declaration text).
```
noncomputable def ed {α : Type u} (x y : List α) : ℕ :=
…
```
abbrev OAI.TreeEdit.RealL1 line 26
Source documentation
The full infinite-dimensional real ℓ₁ space.
Also declared: ComparatorChallenges/BinaryEditLower.lean:24 (same declaration text), ComparatorChallenges/TreeEdit.lean:26 (same declaration text).
```
abbrev RealL1 := lp (fun _ : ℕ => ℝ) 1
```
def OAI.TreeEdit.distortion line 29
Source documentation
Product of the two maximal pairwise distance ratios.
Also declared: ComparatorChallenges/TreeEdit.lean:29 (same declaration text).
```
noncomputable def distortion (W : Finset (List Bool)) (f : W → RealL1) : ℝ :=
…
```
Mentions: OAI.TreeEdit.RealL1
def OAI.TreeEdit.c1 line 36
Source documentation
Infimum over all injective ℓ₁ maps, used on finite sets with at least two points.
Also declared: ComparatorChallenges/TreeEdit.lean:36 (same declaration text).
```
noncomputable def c1 (W : Finset (List Bool)) : ℝ :=
…
```
def OAI.TreeEdit.BinaryLowerBound line 40
Source documentation
The binary main endpoint, for every sufficiently large cap (natural logarithms).
Also declared: ComparatorChallenges/TreeEdit.lean:40 (same declaration text).
```
def BinaryLowerBound : Prop :=
…
```
def OAI.TreeEdit.lcs line 47
Source documentation
The length of a longest arbitrary common subsequence.
```
noncomputable def lcs {α : Type u} (x y : List α) : ℕ :=
…
```
def OAI.TreeEdit.deficit line 51
Source documentation
One-sided deficit; used below only when the two lengths agree.
```
noncomputable def deficit {α : Type u} (x y : List α) : ℕ := x.length - lcs x y
```
Mentions: OAI.TreeEdit.lcs
abbrev OAI.TreeEdit.Word line 54
Source documentation
Fixed-length words, with symbols at every position arbitrary.
Also declared: ComparatorChallenges/BinaryEditLower.lean:25 (same declaration text).
```
abbrev Word (α : Type u) (n : ℕ) := {x : List α // x.length = n}
```
def OAI.TreeEdit.encode line 57
Source documentation
The concatenation extension of a fixed-width symbol code, on all finite words.
```
def encode {α : Type u} {β : Type v} {P : ℕ} (c : α → Word β P) (x : List α) : List β :=
…
```
Mentions: OAI.TreeEdit.Word
def OAI.TreeEdit.FixedLengthBinaryConversion line 61
Source documentation
Exact polynomial-width code endpoint, including the stronger deficit inequality.
```
def FixedLengthBinaryConversion : Prop :=
…
```
def OAI.TreeEdit.vectorWord line 74