Input.lean`

31 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Superstring.Input.subwords line 12
Source documentation
Quadratic substring enumeration, with boundaries represented explicitly.
```
def subwords (s : List α) : Finset (List α) :=
…
```
theorem OAI.Superstring.Input.mem_subwords line 16
def OAI.Superstring.Input.core line 30
Source documentation
Deleting empty, duplicate and properly contained input words.
```
def core (S : List (List α)) : Finset (List α) :=
…
```
theorem OAI.Superstring.Input.mem_core line 33
theorem OAI.Superstring.Input.core_cover line 37
def OAI.Superstring.Input.vertices line 51
theorem OAI.Superstring.Input.mem_vertices line 54
def OAI.Superstring.Input.alphabet line 59
def OAI.Superstring.Input.data line 61
theorem OAI.Superstring.Input.closed line 63
theorem OAI.Superstring.Input.letter_mem line 71
theorem OAI.Superstring.Input.required_mem line 77
theorem OAI.Superstring.Input.core_superstring_iff line 80
theorem OAI.Superstring.concatenation_superstring line 94
theorem OAI.Superstring.feasible_lengths_nonempty line 97
theorem OAI.Superstring.weight_le_opt line 102
Source documentation
The actual computed lower bound is bounded by the unrestricted optimum.
```
theorem weight_le_opt (S : Instance) : (Input.data S).weight ≤ opt S := by
…
```
Mentions: OAI.Superstring.Instance, OAI.Superstring.Input.data, OAI.Superstring.opt
theorem OAI.Superstring.input_count_le_total line 110
structure OAI.Superstring.Counts.Data.WellFormed line 120
Source documentation
The hypotheses supplied by the actual all-substrings input construction.
```
structure WellFormed (D : Counts.Data α) : Prop where
…
```
Mentions: OAI.Superstring.Counts.Data
theorem OAI.Superstring.Counts.Data.input_wellFormed line 126
theorem OAI.Superstring.Counts.Data.mem_of_count_ne_zero line 129
theorem OAI.Superstring.Counts.Data.left_bound line 134
theorem OAI.Superstring.Counts.Data.right_bound line 147
def OAI.Superstring.Counts.Data.up line 161
def OAI.Superstring.Counts.Data.down line 164
theorem OAI.Superstring.Counts.Data.up_add line 167
theorem OAI.Superstring.Counts.Data.down_add line 171
theorem OAI.Superstring.Counts.Data.balanced line 177
Source documentation
Balance is an exact natural-number equality; no truncated subtraction is silently cancelled without the extension inequalities.
```
theorem balanced (D : Data α) (hD : D.WellFormed) (s : List α) :
    D.up s + ∑ c ∈ D.alphabet, D.down (c :: s) =
      D.down s + ∑ c ∈ D.alphabet, D.up (s ++ [c]) := by
…
```
Mentions: OAI.Superstring.Counts.Data
theorem OAI.Superstring.Counts.Data.sum_left_all line 203
Source documentation
Reindex all left extensions by their unique first letter and suffix.
```
theorem sum_left_all (D : Data α) (hD : D.WellFormed) :
    (∑ s ∈ D.vertices, ∑ c ∈ D.alphabet, D.count (c :: s)) =
      ∑ r ∈ D.vertices, D.count r := by
…
```
Mentions: OAI.Superstring.Counts.Data

theorem OAI.Superstring.Counts.Data.sum_right_all line 224

Source documentation

The dual reindexing by prefix and final letter.

theorem sum_right_all (D : Data α) (hD : D.WellFormed) :
    (∑ s ∈ D.vertices, ∑ c ∈ D.alphabet, D.count (s ++ [c])) =
      ∑ r ∈ D.vertices, D.count r := by
…

Mentions: OAI.Superstring.Counts.Data

theorem OAI.Superstring.Counts.Data.total_up line 251
Source documentation
Telescoping of all actual up-edge multiplicities.
```
theorem total_up (D : Data α) (hD : D.WellFormed) :
    (∑ s ∈ D.vertices, D.up s) = D.weight := by
…
```
Mentions: OAI.Superstring.Counts.Data
theorem OAI.Superstring.Counts.Data.total_down line 266