Words.lean`

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

All alternating word shapes, allowing either algebra at either endpoint.

def OAI.Generator.alternatingFrom line 19
def OAI.Generator.alternatingSlotSets line 23
theorem OAI.Generator.alternatingFrom_slots line 27
theorem OAI.Generator.alternatingSlotSets_length line 34
def OAI.Generator.alternatingMomentsZero line 41
Source documentation
Vanishing of every nonempty alternating word from two specified sets.
```
def alternatingMomentsZero {K : Type*} [Zero K] [Monoid A]
    (φ : A → K) (S T : Set A) : Prop :=
…
```
theorem OAI.Generator.alternatingFrom_image line 50
theorem OAI.Generator.alternatingMomentsZero_map line 61
theorem OAI.Generator.word_split_first line 75
theorem OAI.Generator.reduced_append_left line 94
theorem OAI.Generator.reduced_append_right line 98
theorem OAI.Generator.reduced_tail line 102
def OAI.Generator.orderedWords line 109
theorem OAI.Generator.orderedWords_zero line 116
theorem OAI.Generator.orderedWords_nil line 119
theorem OAI.Generator.orderedWords_cons line 123
Source documentation
Grouping nondecreasing row words by the number of initial first-row letters.
```
theorem orderedWords_cons (a : R) (as : List R) (d : ℕ) :
    orderedWords (a :: as) d =
      ∑ k ∈ Finset.range (d + 1), a ^ k * orderedWords as (d - k) := by
…
```
Mentions: OAI.Generator.orderedWords
theorem OAI.Generator.orderedWords_nonneg line 140
theorem OAI.Generator.orderedWords_tail_le line 152
theorem OAI.Generator.orderedWords_step_le line 163
Source documentation
Choosing the first row of a nondecreasing word gives a subset of all choices.
```
theorem orderedWords_step_le (xs : List R) (hx : ∀ a ∈ xs, 0 ≤ a) (d : ℕ) :
    orderedWords xs (d + 1) ≤ xs.sum * orderedWords xs d := by
…
```
Mentions: OAI.Generator.orderedWords
theorem OAI.Generator.orderedWords_le_sum_pow line 181
Source documentation
All-degree bound by the full distributive power, without commuting factors.
```
theorem orderedWords_le_sum_pow (xs : List R) (hx : ∀ a ∈ xs, 0 ≤ a) (d : ℕ) :
    orderedWords xs d ≤ xs.sum ^ d := by
…
```
Mentions: OAI.Generator.orderedWords