TreeEvaluation.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Actual nonlinear evaluation on a weighted ordered tree

The maps act on the literal subtype of a convex subset of a real normed space. A cutoff value is an output: its own node map is not applied again.

structure OAI.ReflexiveFixedPoints.TreeEvaluation line 24
def OAI.ReflexiveFixedPoints.TreeEvaluation.childAverage line 35
Source documentation
The actual convex average of the child outputs.
```
noncomputable def childAverage (k : ℕ) (H : T.Node (k + 1) → K)
    (p : T.Node k) : K := by
…
```
theorem OAI.ReflexiveFixedPoints.TreeEvaluation.childAverage_val line 44
def OAI.ReflexiveFixedPoints.TreeEvaluation.collapse line 51
Source documentation
One genuine level of the nonlinear recursive evaluation.
```
noncomputable def collapse (k : ℕ) (H : T.Node (k + 1) → K)
    (p : T.Node k) : K := E.map k p (E.childAverage k H p)
```
def OAI.ReflexiveFixedPoints.TreeEvaluation.evaluate line 55
Source documentation
Evaluate a cutoff assignment, applying maps strictly above its level.
```
noncomputable def evaluate : (k : ℕ) → (T.Node k → K) → K
  | 0, H => H T.root
  | k + 1, H => evaluate k (E.collapse k H)
```
theorem OAI.ReflexiveFixedPoints.TreeEvaluation.evaluate_zero line 59
theorem OAI.ReflexiveFixedPoints.TreeEvaluation.evaluate_succ line 62

def OAI.ReflexiveFixedPoints.TreeEvaluation.evaluateFrom line 66

Source documentation

Evaluate only between the two indicated depths.

noncomputable def evaluateFrom (k : ℕ) :
    (d : ℕ) → (T.Node (k + d) → K) → T.Node k → K
  | 0, H => H
  | d + 1, H => evaluateFrom k d (E.collapse (k + d) H)

theorem OAI.ReflexiveFixedPoints.TreeEvaluation.evaluateFrom_zero line 71
theorem OAI.ReflexiveFixedPoints.TreeEvaluation.evaluateFrom_succ line 74
theorem OAI.ReflexiveFixedPoints.TreeEvaluation.evaluate_factorization line 79
Source documentation
Evaluation factorizes at every intermediate cutoff.
```
theorem evaluate_factorization (k d : ℕ) (H : T.Node (k + d) → K) :
    E.evaluate (k + d) H = E.evaluate k (E.evaluateFrom k d H) := by
…
```

theorem OAI.ReflexiveFixedPoints.TreeEvaluation.childAverage_norm_sub_le line 87

Source documentation

A finite weighted average has the expected weighted sensitivity.

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

theorem OAI.ReflexiveFixedPoints.TreeEvaluation.collapse_norm_sub_le line 106

Source documentation

Each actual parent map is nonexpansive after taking its child average.

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

theorem OAI.ReflexiveFixedPoints.TreeEvaluation.evaluate_norm_sub_le line 119

Source documentation

The sensitivity estimate for actual nonlinear root outputs.

theorem evaluate_norm_sub_le (k : ℕ) (H H' : T.Node k → K) :
    ‖(E.evaluate k H : X) - E.evaluate k H'‖ ≤
      ∑ v, W.pathWeight k v * ‖(H v : X) - H' v‖ := by
…

theorem OAI.ReflexiveFixedPoints.TreeEvaluation.evaluate_norm_sub_le_of_forall line 157

Source documentation

Uniform cutoff errors propagate with no increase to the root.

theorem evaluate_norm_sub_le_of_forall (k : ℕ) (H H' : T.Node k → K)
    {ε : ℝ} (hε : ∀ v, ‖(H v : X) - H' v‖ ≤ ε) :
    ‖(E.evaluate k H : X) - E.evaluate k H'‖ ≤ ε := by
…

theorem OAI.ReflexiveFixedPoints.TreeEvaluation.evaluate_norm_sub_le_single line 170

Source documentation

Changing just one cutoff output has its actual path weight as sensitivity.

theorem evaluate_norm_sub_le_single (k : ℕ) (H H' : T.Node k → K)
    (v : T.Node k) (heq : ∀ w, w ≠ v → H w = H' w) :
    ‖(E.evaluate k H : X) - E.evaluate k H'‖ ≤
      W.pathWeight k v * ‖(H v : X) - H' v‖ := by
…