CoarseTransforms.lean`

20 declarations, 0 contain sorry, 0 declared as axioms

Linear sweeps for the coarse penalty transform

The finite minima define the semantic arrays. These sweeps compute them with one rational addition and one comparison per scan transition.

def OAI.EditApproximation.coarsePrefixMinimum line 16
theorem OAI.EditApproximation.coarsePrefixMinimum_le line 20
theorem OAI.EditApproximation.coarsePrefixMinimum_attained line 39

def OAI.EditApproximation.coarseLeftSweep line 56

Source documentation

The executable left sweep; Lean's scanl traverses its input once.

def coarseLeftSweep : List ℚ → List ℚ
  | [] => []
  | first :: rest => rest.scanl (fun previous value => min value (previous + 2)) first

theorem OAI.EditApproximation.coarseLeftSweep_length line 60
theorem OAI.EditApproximation.coarseLeftSweep_getElem line 64
def OAI.EditApproximation.coarseCostedScan line 87
Source documentation
A costed scan records the addition and comparison actually performed at each transition; list traversal is charged separately by the RAM model.
```
def coarseCostedScan (previous : ℚ) : List ℚ → List ℚ × ℕ
  | [] => ([previous], 0)
  | value :: rest =>
    let next := min value (previous + 2)
…
```
theorem OAI.EditApproximation.coarseCostedScan_result line 94
def OAI.EditApproximation.coarseArrayLookup line 105
def OAI.EditApproximation.coarseReverseLookup line 108

theorem OAI.EditApproximation.coarse_two_prefix_minimum line 112

Source documentation

Two one-sided recurrences equal the complete literal penalty minimum.

theorem coarse_two_prefix_minimum {n : ℕ} [NeZero n] (value : Fin n → ℚ) (v : Fin n) :
    min (coarsePrefixMinimum (coarseArrayLookup value) v.val)
        (coarsePrefixMinimum (coarseReverseLookup value) (n - 1 - v.val)) =
      univ.inf' univ_nonempty (fun u => value u + (2 * Nat.dist v.val u.val : ℕ)) := by
…

Mentions: OAI.EditApproximation.coarsePrefixMinimum, OAI.EditApproximation.coarseArrayLookup, OAI.EditApproximation.coarseReverseLookup

def OAI.EditApproximation.coarsePenaltyTransform line 165
Source documentation
Literal array output of the two linear sweeps.
```
def coarsePenaltyTransform (source : List ℚ) : List ℚ :=
…
```
theorem OAI.EditApproximation.coarsePenaltyTransform_length line 168
theorem OAI.EditApproximation.coarseArrayLookup_list line 173
theorem OAI.EditApproximation.coarseReverseLookup_list line 182

theorem OAI.EditApproximation.coarsePenaltyTransform_getElem line 194

Source documentation

Every returned array cell equals the complete finite semantic minimum.

theorem coarsePenaltyTransform_getElem (source : List ℚ) [NeZero source.length]
    (v : Fin source.length) :
    (coarsePenaltyTransform source)[v.val]'(by rw [coarsePenaltyTransform_length]; exact v.isLt) =
      univ.inf' univ_nonempty (fun u : Fin source.length =>
        source[u.val] + (2 * Nat.dist v.val u.val : ℕ)) := by
…

Mentions: OAI.EditApproximation.coarsePenaltyTransform, OAI.EditApproximation.coarsePenaltyTransform_length

def OAI.EditApproximation.coarseCostedLeftSweep line 211
theorem OAI.EditApproximation.coarseCostedLeftSweep_result line 215
def OAI.EditApproximation.coarseCostedPenaltyTransform line 225
Source documentation
Instrumented actual sweeps plus the final cellwise comparisons.
```
def coarseCostedPenaltyTransform (source : List ℚ) : List ℚ × ℕ :=
…
```
theorem OAI.EditApproximation.coarseCostedPenaltyTransform_result line 231