TreeFrontier.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Finite, already evaluated tree frontiers

A frontier contains only the current finite level and the actual evaluation of the part already built. The root and extension operations below construct that evaluation by recursion. In particular, a prediction made at a frontier does not inspect any future tree level.

structure OAI.ReflexiveFixedPoints.TreeFrontier line 25
Source documentation
The current maps and the evaluation strictly above a finite cutoff.
```
structure TreeFrontier (K : Set X) where
…
```
def OAI.ReflexiveFixedPoints.TreeFrontier.root line 41
Source documentation
At depth zero the sole cutoff output is already the root output.
```
def root (hK : Convex ℝ K) : TreeFrontier K where
…
```
Mentions: OAI.ReflexiveFixedPoints.TreeFrontier
theorem OAI.ReflexiveFixedPoints.TreeFrontier.root_size line 50
theorem OAI.ReflexiveFixedPoints.TreeFrontier.root_map line 52
theorem OAI.ReflexiveFixedPoints.TreeFrontier.root_evaluate line 55
structure OAI.ReflexiveFixedPoints.FrontierExtension line 62
Source documentation
One concrete finite successor level. Its parentwise positive weights are supplied only after the corresponding adaptive selections stop.
```
structure FrontierExtension {K : Set X} (F : TreeFrontier K) where
…
```
Mentions: OAI.ReflexiveFixedPoints.TreeFrontier
def OAI.ReflexiveFixedPoints.FrontierExtension.childAverage line 80
Source documentation
Actual parentwise convex average of the new cutoff outputs.
```
def childAverage (H : Fin C.size → K) (p : Fin F.size) : K := by
…
```
theorem OAI.ReflexiveFixedPoints.FrontierExtension.childAverage_val line 87
def OAI.ReflexiveFixedPoints.FrontierExtension.collapse line 93
Source documentation
The current maps act once, after the new child averages.
```
def collapse (H : Fin C.size → K) (p : Fin F.size) : K :=
…
```

theorem OAI.ReflexiveFixedPoints.FrontierExtension.childAverage_norm_sub_le_of_forall line 97

Source documentation

A uniform cutoff bound remains a uniform bound after averaging.

theorem childAverage_norm_sub_le_of_forall
    (H H' : Fin C.size → K) {ε : ℝ}
    (h : ∀ c, ‖(H c : X) - (H' c : X)‖ ≤ ε) (p : Fin F.size) :
    ‖(C.childAverage H p : X) - (C.childAverage H' p : X)‖ ≤ ε := by
…

theorem OAI.ReflexiveFixedPoints.FrontierExtension.collapse_norm_sub_le_of_forall line 120
def OAI.ReflexiveFixedPoints.FrontierExtension.toFrontier line 131
Source documentation
The next frontier evaluation is built from the preceding one.
```
def toFrontier : TreeFrontier K where
…
```
Mentions: OAI.ReflexiveFixedPoints.TreeFrontier
theorem OAI.ReflexiveFixedPoints.FrontierExtension.toFrontier_size line 142
theorem OAI.ReflexiveFixedPoints.FrontierExtension.toFrontier_map line 144
theorem OAI.ReflexiveFixedPoints.FrontierExtension.toFrontier_evaluate line 147