FrontierFromGroups.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Assembling a frontier from its ordered parent groups

The local children are concatenated in parent order. The inverse of the actual concatenation equivalence retrieves each child's weight and map. Reindexing the parent fiber proves normalization and identifies the actual child average with its local group sum.

def OAI.ReflexiveFixedPoints.FrontierExtension.groupValue line 24
Source documentation
Read a local value using the unique group and position of a global index.
```
def groupValue {n : ℕ} (c : Fin n → ℕ) {V : Type v}
    (f : ∀ p, Fin (c p) → V) (i : Fin (OrderedGroupConcat.total c)) : V :=
…
```
Mentions: OAI.ReflexiveFixedPoints.OrderedGroupConcat.total
theorem OAI.ReflexiveFixedPoints.FrontierExtension.groupValue_group line 29
def OAI.ReflexiveFixedPoints.FrontierExtension.ofGroups line 48
Source documentation
Assemble the actual extension from the positive, normalized child groups.
```
def ofGroups : FrontierExtension F where
…
```
Mentions: OAI.ReflexiveFixedPoints.FrontierExtension
theorem OAI.ReflexiveFixedPoints.FrontierExtension.ofGroups_size line 67
theorem OAI.ReflexiveFixedPoints.FrontierExtension.ofGroups_parent line 71
theorem OAI.ReflexiveFixedPoints.FrontierExtension.ofGroups_parent_group line 75
theorem OAI.ReflexiveFixedPoints.FrontierExtension.ofGroups_weight_group line 80
theorem OAI.ReflexiveFixedPoints.FrontierExtension.ofGroups_map_group line 86
theorem OAI.ReflexiveFixedPoints.FrontierExtension.ofGroups_childAverage_val line 93
Source documentation
The extension's actual parent fiber average is exactly the local group sum.
```
theorem ofGroups_childAverage_val
    (H : Fin (OrderedGroupConcat.total childCount) → K) (p : Fin F.size) :
    ((ofGroups F childCount count_pos childWeight weight_pos weight_sum
      childMap map_nonexpansive).childAverage H p : X) =
      ∑ j, childWeight p j • (H (OrderedGroupConcat.group childCount p j) : X) := by
…
```
Mentions: OAI.ReflexiveFixedPoints.OrderedGroupConcat.total, OAI.ReflexiveFixedPoints.FrontierExtension.ofGroups, OAI.ReflexiveFixedPoints.FrontierExtension.childAverage, OAI.ReflexiveFixedPoints.OrderedGroupConcat.group

theorem OAI.ReflexiveFixedPoints.FrontierExtension.ofGroups_childAverage_map_val line 105

Source documentation

Label every global child by its actual map applied to the common anchor.

theorem ofGroups_childAverage_map_val (x : K) (p : Fin F.size) :
    ((ofGroups F childCount count_pos childWeight weight_pos weight_sum
      childMap map_nonexpansive).childAverage
        (fun i => (ofGroups F childCount count_pos childWeight weight_pos weight_sum
          childMap map_nonexpansive).map i x) p : X) =
      ∑ j, childWeight p j • (childMap p j x : X) := by
…

Mentions: OAI.ReflexiveFixedPoints.FrontierExtension.ofGroups, OAI.ReflexiveFixedPoints.FrontierExtension.childAverage

theorem OAI.ReflexiveFixedPoints.FrontierExtension.ofGroups_childAverage_near line 118

Source documentation

Every local anchor return estimate is preserved by the assembled extension.

theorem ofGroups_childAverage_near (x : K) {τ : ℝ}
    (hreturn : ∀ p, ‖(∑ j, childWeight p j • (childMap p j x : X)) - (x : X)‖ < τ)
    (p : Fin F.size) :
    ‖((ofGroups F childCount count_pos childWeight weight_pos weight_sum
      childMap map_nonexpansive).childAverage
        (fun i => (ofGroups F childCount count_pos childWeight weight_pos weight_sum
          childMap map_nonexpansive).map i x) p : X) - (x : X)‖ < τ := by
…

Mentions: OAI.ReflexiveFixedPoints.FrontierExtension.ofGroups, OAI.ReflexiveFixedPoints.FrontierExtension.childAverage