Model.lean`

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.EditDistortion.L1 line 20
Source documentation
Minimum script length. Scripts always exist (delete x and insert y).
Also declared: ComparatorChallenges/EditDistance.lean:26 (same declaration text).
```
abbrev L1 := lp (fun _ : ℕ => ℝ) 1
```
def OAI.EditDistortion.distortion line 23
Source documentation
The product of the two maximal distance ratios.
Also declared: ComparatorChallenges/EditDistance.lean:29 (same declaration text).
```
noncomputable def distortion {X : Type u} (ρ : X → X → ℝ) (f : X ↪ L1) : ℝ :=
…
```
Mentions: OAI.EditDistortion.L1
def OAI.EditDistortion.leastDistortion line 28
Source documentation
The infimum over injective maps to real absolutely summable sequences.
Also declared: ComparatorChallenges/EditDistance.lean:34 (same declaration text).
```
noncomputable def leastDistortion {X : Type u} (ρ : X → X → ℝ) : ℝ :=
…
```
abbrev OAI.EditDistortion.Words line 31
Also declared: ComparatorChallenges/EditDistance.lean:37 (same declaration text).
def OAI.EditDistortion.E line 33
Also declared: ComparatorChallenges/EditDistance.lean:39 (same declaration text).
def OAI.EditDistortion.exponentScale line 36
Also declared: ComparatorChallenges/EditDistance.lean:42 (same declaration text).
def OAI.EditDistortion.alphabetSup line 40
Source documentation
Supremum over finite alphabet cardinalities.
Also declared: ComparatorChallenges/EditDistance.lean:46 (same declaration text).
```
noncomputable def alphabetSup (d : ℕ) : ℝ :=
…
```
def OAI.EditDistortion.BinaryWitness line 44
Source documentation
A finite nonempty subset of binary words of one common length.
Also declared: ComparatorChallenges/EditDistance.lean:50 (same declaration text).
```
def BinaryWitness (c : ℝ) (d : ℕ) : Prop :=
…
```
def OAI.EditDistortion.MainClaim line 50
Source documentation
Uniform two-sided bounds with common positive constants and threshold.
Also declared: ComparatorChallenges/EditDistance.lean:56 (same declaration text).
```
def MainClaim : Prop :=
…
```