Connections.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Connection costs with arbitrary gaps and overlaps

This proves the edit-cost part of the connection inequality of Section 2 for actual substrings and edit scripts. Prefixes telescope across the child intervals; common-prefix cancellation then removes the outside prefix. The children need not have ordered or shared target endpoints.

theorem OAI.EditApproximation.edit_drop_insert_le line 22
theorem OAI.EditApproximation.edit_drop_step_le line 35
theorem OAI.EditApproximation.edit_drop_script_le line 56
theorem OAI.EditApproximation.edit_drop_nonexpansive line 65
theorem OAI.EditApproximation.edit_append_left_cancel line 69
theorem OAI.EditApproximation.edit_append_right_le line 76
def OAI.EditApproximation.targetConcatenation line 85
Source documentation
The outside and successive endpoint charges, including the final jump.
```
def targetConcatenation {α : Type u} (word : List α)
    (states : List (TargetInterval word.length)) : List α :=
…
```
Mentions: OAI.EditApproximation.TargetInterval
theorem OAI.EditApproximation.prefix_append_substring line 89
theorem OAI.EditApproximation.prefix_child_step line 96
theorem OAI.EditApproximation.prefix_connection_bound line 105
theorem OAI.EditApproximation.target_connection_bound line 126
Source documentation
The target-only part of the connection inequality. The prefix proof accounts for overlaps and backwards connecting jumps automatically.
```
theorem target_connection_bound {α : Type u} (word : List α)
    (states : List (TargetInterval word.length)) (parent : TargetInterval word.length) :
    edit (targetConcatenation word states) (substring word parent.lo parent.hi) ≤
      connectionBudget parent.lo states parent.hi := by
…
```
Mentions: OAI.EditApproximation.TargetInterval, OAI.EditApproximation.targetConcatenation, OAI.EditApproximation.substring, OAI.EditApproximation.connectionBudget
theorem OAI.EditApproximation.edit_flatten_pairs_le line 142

theorem OAI.EditApproximation.child_connection_bound line 155

Source documentation

Child editing plus endpoint connections bounds the parent cost, for an actual concatenated partition of the source string.

theorem child_connection_bound {α : Type u} (word : List α)
    (children : List (List α × TargetInterval word.length))
    (parent : TargetInterval word.length) :
    edit (children.map Prod.fst).flatten (substring word parent.lo parent.hi) ≤
      (children.map fun child => edit child.1 (substring word child.2.lo child.2.hi)).sum +
        connectionBudget parent.lo (children.map Prod.snd) parent.hi := by
…

Mentions: OAI.EditApproximation.TargetInterval, OAI.EditApproximation.substring, OAI.EditApproximation.connectionBudget

def OAI.EditApproximation.signedLengthGap line 171
theorem OAI.EditApproximation.signedLengthGap_append line 174
theorem OAI.EditApproximation.flattened_length_gap_le line 179

theorem OAI.EditApproximation.child_shift_connection_bound line 190

Source documentation

Length gaps obey the same arbitrary-gap connection inequality as the edit costs. This is the second lower invariant of the Bellman operator.

theorem child_shift_connection_bound {α : Type u} (word : List α)
    (children : List (List α × TargetInterval word.length))
    (parent : TargetInterval word.length) :
    |signedLengthGap (children.map Prod.fst).flatten (substring word parent.lo parent.hi)| ≤
      (children.map fun child =>
        |signedLengthGap child.1 (substring word child.2.lo child.2.hi)|).sum +
        (connectionBudget parent.lo (children.map Prod.snd) parent.hi : ℝ) := by
…

Mentions: OAI.EditApproximation.TargetInterval, OAI.EditApproximation.signedLengthGap, OAI.EditApproximation.substring, OAI.EditApproximation.connectionBudget