SubtreeEvaluation.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Actual evaluation of a subtree

Evaluation between two arbitrary levels is an iteration of the same collapse operation used by root evaluation. The cutoff's own maps are not applied. Composition gives both the root factorization and the recurrence at the top of a subtree.

def OAI.ReflexiveFixedPoints.TreeEvaluation.subtreeOutput line 28
Source documentation
The actual outputs between two levels, formed by iterating collapse.
```
noncomputable def subtreeOutput {i j : ℕ} (h : i ≤ j) :
    (T.Node j → K) → T.Node i → K :=
…
```
theorem OAI.ReflexiveFixedPoints.TreeEvaluation.subtreeOutput_refl_apply line 33

theorem OAI.ReflexiveFixedPoints.TreeEvaluation.subtreeOutput_step line 38

Source documentation

Peel off the collapse immediately above the cutoff level.

theorem subtreeOutput_step {i j : ℕ} (h : i ≤ j) {h' : i ≤ j + 1}
    (H : T.Node (j + 1) → K) :
    E.subtreeOutput h' H = E.subtreeOutput h (E.collapse j H) := by
…

theorem OAI.ReflexiveFixedPoints.TreeEvaluation.subtreeOutput_succ line 44

theorem OAI.ReflexiveFixedPoints.TreeEvaluation.subtreeOutput_comp line 49

Source documentation

Evaluating through two consecutive intervals equals their actual composite.

theorem subtreeOutput_comp {i j k : ℕ} (hij : i ≤ j) (hjk : j ≤ k)
    (H : T.Node k → K) :
    E.subtreeOutput hij (E.subtreeOutput hjk H) =
      E.subtreeOutput (hij.trans hjk) H := by
…

theorem OAI.ReflexiveFixedPoints.TreeEvaluation.subtreeOutput_top_step line 60

Source documentation

The recursive rule at the top of a subtree uses its actual child outputs.

theorem subtreeOutput_top_step {i j : ℕ} (h : i ≤ j) (hnext : i + 1 ≤ j)
    (H : T.Node j → K) :
    E.subtreeOutput h H = E.collapse i (E.subtreeOutput hnext H) := by
…

theorem OAI.ReflexiveFixedPoints.TreeEvaluation.subtreeOutput_top_step_apply line 69
theorem OAI.ReflexiveFixedPoints.TreeEvaluation.evaluate_subtreeOutput line 77
Source documentation
Root evaluation factorizes through the actual outputs at every intermediate level.
```
theorem evaluate_subtreeOutput {i j : ℕ} (h : i ≤ j) (H : T.Node j → K) :
    E.evaluate j H = E.evaluate i (E.subtreeOutput h H) := by
…
```
theorem OAI.ReflexiveFixedPoints.TreeEvaluation.subtreeOutput_zero_root line 85
theorem OAI.ReflexiveFixedPoints.TreeEvaluation.subtreeOutput_eq_evaluateFrom line 90
Source documentation
The inequality-indexed and distance-indexed implementations coincide.
```
theorem subtreeOutput_eq_evaluateFrom (i d : ℕ) (H : T.Node (i + d) → K) :
    E.subtreeOutput (Nat.le_add_right i d) H = E.evaluateFrom i d H := by
…
```

theorem OAI.ReflexiveFixedPoints.TreeEvaluation.childAverage_congr line 99

Source documentation

A child average depends only on the children belonging to that parent.

theorem childAverage_congr (k : ℕ) (H H' : T.Node (k + 1) → K)
    (p : T.Node k) (heq : ∀ c, T.parent k c = p → H c = H' c) :
    E.childAverage k H p = E.childAverage k H' p := by
…

theorem OAI.ReflexiveFixedPoints.TreeEvaluation.collapse_congr line 109

Source documentation

The nonlinear parent map preserves equality of its actual child input.

theorem collapse_congr (k : ℕ) (H H' : T.Node (k + 1) → K)
    (p : T.Node k) (heq : ∀ c, T.parent k c = p → H c = H' c) :
    E.collapse k H p = E.collapse k H' p := by
…

theorem OAI.ReflexiveFixedPoints.TreeEvaluation.subtreeOutput_congr line 116

Source documentation

A subtree output depends only on the cutoff values below that node.

theorem subtreeOutput_congr {i j : ℕ} (h : i ≤ j) :
    ∀ (H H' : T.Node j → K) (v : T.Node i),
      (∀ s, T.ancestorLE h s = v → H s = H' s) →
      E.subtreeOutput h H v = E.subtreeOutput h H' v := by
…

theorem OAI.ReflexiveFixedPoints.TreeEvaluation.subtreeOutput_congr_of_descendants line 135