SubtreeErrors.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Errors of the actual nonlinear subtree evaluation.

An untouched subtree is compared to its map applied to the anchor. The proof uses the actual collapse rule and child-average estimates at each internal level. The local version follows from equality on descendant leaves.

theorem OAI.ReflexiveFixedPoints.TreeEvaluation.childAverage_const line 28
Source documentation
Averaging a constant child assignment returns the same actual point.
```
@[simp] theorem childAverage_const (k : ℕ) (b : K) (p : T.Node k) :
    E.childAverage k (fun _ => b) p = b := by
…
```
theorem OAI.ReflexiveFixedPoints.TreeEvaluation.map_norm_sub_le line 34
Source documentation
Each assigned map is nonexpansive in the original ambient norm.
```
theorem map_norm_sub_le (k : ℕ) (p : T.Node k) (a b : K) :
    ‖(E.map k p a : X) - E.map k p b‖ ≤ ‖(a : X) - b‖ := by
…
```

theorem OAI.ReflexiveFixedPoints.TreeEvaluation.collapse_norm_sub_point_le line 40

Source documentation

One actual collapse transmits a constant up to the node's displacement.

theorem collapse_norm_sub_point_le (k : ℕ) (H : T.Node (k + 1) → K)
    (b : K) (p : T.Node k) :
    ‖(E.collapse k H p : X) - b‖ ≤
      (∑ c ∈ Finset.univ.filter (fun c => T.parent k c = p),
        W.weight k c * ‖(H c : X) - b‖) + ‖(E.map k p b : X) - b‖ := by
…

theorem OAI.ReflexiveFixedPoints.TreeEvaluation.collapse_norm_sub_label_le line 57

Source documentation

Compare an actual parent output to the parent's prescribed anchor label.

theorem collapse_norm_sub_label_le (k : ℕ) (H : T.Node (k + 1) → K)
    (x : K) (p : T.Node k) :
    ‖(E.collapse k H p : X) - E.map k p x‖ ≤
      (∑ c ∈ Finset.univ.filter (fun c => T.parent k c = p),
        W.weight k c * ‖(H c : X) - E.map (k + 1) c x‖) +
      ‖(E.childAverage k (fun c => E.map (k + 1) c x) p : X) - x‖ := by
…

theorem OAI.ReflexiveFixedPoints.TreeEvaluation.subtreeOutput_labels_norm_sub_le line 75

Source documentation

The canonical untouched subtree incurs the sum of its finite level errors.

theorem subtreeOutput_labels_norm_sub_le (x : K) (τ : ℕ → ℝ) {N : ℕ}
    (haverage : ∀ k, k < N → ∀ p : T.Node k,
      ‖(E.childAverage k (fun c => E.map (k + 1) c x) p : X) - x‖ ≤ τ k)
    {k : ℕ} (h : k ≤ N) (v : T.Node k) :
    ‖(E.subtreeOutput h (fun s => E.map N s x) v : X) - E.map k v x‖ ≤
      ∑ d ∈ Finset.Ico k N, τ d := by
…

theorem OAI.ReflexiveFixedPoints.TreeEvaluation.subtreeOutput_untouched_norm_sub_le line 109

Source documentation

Only descendant leaves need be untouched; all other leaf states are arbitrary.

theorem subtreeOutput_untouched_norm_sub_le (x : K) (τ : ℕ → ℝ) {N : ℕ}
    (haverage : ∀ k, k < N → ∀ p : T.Node k,
      ‖(E.childAverage k (fun c => E.map (k + 1) c x) p : X) - x‖ ≤ τ k)
    {k : ℕ} (h : k ≤ N) (H : T.Node N → K) (v : T.Node k)
    (huntouched : ∀ s, T.ancestorLE h s = v → H s = E.map N s x) :
    ‖(E.subtreeOutput h H v : X) - E.map k v x‖ ≤
      ∑ d ∈ Finset.Ico k N, τ d := by
…