OrderedGroupConcat.lean`

31 declarations, 0 contain sorry, 0 declared as axioms

Concatenation of ordered finite groups

Each parent contributes a finite group. The global index is the sum of the sizes of earlier groups plus the local index. This arithmetic construction gives both the monotone parent map and the order embedding induced by retaining an increasing subsequence within each group.

def OAI.ReflexiveFixedPoints.OrderedGroupConcat.total line 25
Source documentation
The number of entries after concatenating all groups.
```
def total (c : Fin n → ℕ) : ℕ := ∑ p, c p
```
def OAI.ReflexiveFixedPoints.OrderedGroupConcat.offset line 28
Source documentation
The number of entries in groups preceding p.
```
def offset (c : Fin n → ℕ) (p : Fin n) : ℕ :=
…
```
theorem OAI.ReflexiveFixedPoints.OrderedGroupConcat.offset_zero line 31
theorem OAI.ReflexiveFixedPoints.OrderedGroupConcat.offset_succ line 35
Source documentation
Appending one parent group advances the prefix counter by its size.
```
theorem offset_succ (c : Fin (n + 1) → ℕ) (p : Fin n) :
    offset c p.succ = offset c p.castSucc + c p.castSucc := by
…
```
Mentions: OAI.ReflexiveFixedPoints.OrderedGroupConcat.offset
abbrev OAI.ReflexiveFixedPoints.OrderedGroupConcat.Index line 57
Source documentation
A group and an index in that group.
```
abbrev Index (c : Fin n → ℕ) := Σ p : Fin n, Fin (c p)
```
theorem OAI.ReflexiveFixedPoints.OrderedGroupConcat.offset_add_le_total line 59
theorem OAI.ReflexiveFixedPoints.OrderedGroupConcat.offset_add_le_offset line 66
theorem OAI.ReflexiveFixedPoints.OrderedGroupConcat.offset_mono line 79
def OAI.ReflexiveFixedPoints.OrderedGroupConcat.encode line 88
Source documentation
The actual concatenation ordinal, with its bound proved from the sum.
```
def encode (c : Fin n → ℕ) (s : Index c) : Fin (total c) :=
…
```
Mentions: OAI.ReflexiveFixedPoints.OrderedGroupConcat.Index, OAI.ReflexiveFixedPoints.OrderedGroupConcat.total
theorem OAI.ReflexiveFixedPoints.OrderedGroupConcat.encode_val line 94
theorem OAI.ReflexiveFixedPoints.OrderedGroupConcat.encode_lt_of_parent_lt line 97
theorem OAI.ReflexiveFixedPoints.OrderedGroupConcat.encode_injective line 105
def OAI.ReflexiveFixedPoints.OrderedGroupConcat.equiv line 119
Source documentation
The concatenation is exhaustive: injectivity and the exact finite cardinality prove that every global ordinal has a group and a local index.
```
noncomputable def equiv (c : Fin n → ℕ) : Index c ≃ Fin (total c) :=
…
```
Mentions: OAI.ReflexiveFixedPoints.OrderedGroupConcat.Index, OAI.ReflexiveFixedPoints.OrderedGroupConcat.total
theorem OAI.ReflexiveFixedPoints.OrderedGroupConcat.equiv_apply line 126
theorem OAI.ReflexiveFixedPoints.OrderedGroupConcat.equiv_val line 129
def OAI.ReflexiveFixedPoints.OrderedGroupConcat.group line 133
Source documentation
Each individual group is an increasing interval in the concatenation.
```
def group (c : Fin n → ℕ) (p : Fin n) : Fin (c p) ↪o Fin (total c) :=
…
```
Mentions: OAI.ReflexiveFixedPoints.OrderedGroupConcat.total
theorem OAI.ReflexiveFixedPoints.OrderedGroupConcat.group_apply line 139
theorem OAI.ReflexiveFixedPoints.OrderedGroupConcat.group_val line 142
def OAI.ReflexiveFixedPoints.OrderedGroupConcat.parent line 146
Source documentation
The parent of a global index.
```
noncomputable def parent (c : Fin n → ℕ) (i : Fin (total c)) : Fin n :=
…
```
Mentions: OAI.ReflexiveFixedPoints.OrderedGroupConcat.total
theorem OAI.ReflexiveFixedPoints.OrderedGroupConcat.parent_group line 149
theorem OAI.ReflexiveFixedPoints.OrderedGroupConcat.parent_monotone line 154
theorem OAI.ReflexiveFixedPoints.OrderedGroupConcat.parent_surjective line 165
theorem OAI.ReflexiveFixedPoints.OrderedGroupConcat.sum_parent_fiber line 171
Source documentation
Reindex a sum over the actual parent fiber by the local group indices.
```
theorem sum_parent_fiber (c : Fin n → ℕ) (p : Fin n)
    {A : Type*} [AddCommMonoid A] (f : Fin (total c) → A) :
    (∑ i ∈ Finset.univ.filter (fun i => parent c i = p), f i) =
      ∑ j : Fin (c p), f (group c p j) := by
…
```
Mentions: OAI.ReflexiveFixedPoints.OrderedGroupConcat.total, OAI.ReflexiveFixedPoints.OrderedGroupConcat.parent, OAI.ReflexiveFixedPoints.OrderedGroupConcat.group
theorem OAI.ReflexiveFixedPoints.OrderedGroupConcat.total_pos line 193
def OAI.ReflexiveFixedPoints.OrderedGroupConcat.retainFun line 203
Source documentation
Retaining the prescribed ordered subsequence inside each parent group.
```
noncomputable def retainFun (r : ∀ p, Fin (c p) ↪o Fin (d p))
    (i : Fin (total c)) : Fin (total d) :=
…
```
Mentions: OAI.ReflexiveFixedPoints.OrderedGroupConcat.total
theorem OAI.ReflexiveFixedPoints.OrderedGroupConcat.retainFun_group line 208
theorem OAI.ReflexiveFixedPoints.OrderedGroupConcat.retainFun_strictMono line 215
def OAI.ReflexiveFixedPoints.OrderedGroupConcat.retain line 234
Source documentation
The global increasing retained subsequence.
```
noncomputable def retain (r : ∀ p, Fin (c p) ↪o Fin (d p)) :
    Fin (total c) ↪o Fin (total d) :=
…
```
Mentions: OAI.ReflexiveFixedPoints.OrderedGroupConcat.total
theorem OAI.ReflexiveFixedPoints.OrderedGroupConcat.retain_group line 238
theorem OAI.ReflexiveFixedPoints.OrderedGroupConcat.parent_retain line 242
theorem OAI.ReflexiveFixedPoints.OrderedGroupConcat.retain_group_val line 248