TransmittedSubtreeErrors.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Error transmitted from constant terminal values

Every map displacement is counted at its actual node, with its actual path weight. The proof follows the concrete finite evaluator. No positive uniform lower bound on the weights and no affine property of the node maps is needed.

theorem OAI.ReflexiveFixedPoints.TreeEvaluation.sum_descendant_weighted_children line 29

Source documentation

Regroup the weighted children of the descendants at one level.

theorem sum_descendant_weighted_children {k n : ℕ} (h : k ≤ n)
    (v : T.Node k) (f : T.Node (n + 1) → ℝ) :
    (∑ p ∈ T.descendants h v, W.pathWeight n p *
      (∑ c ∈ Finset.univ.filter (fun c => T.parent n c = p), W.weight n c * f c)) =
      ∑ c ∈ T.descendants (Nat.le_succ_of_le h) v, W.pathWeight (n + 1) c * f c := by
…

theorem OAI.ReflexiveFixedPoints.TreeEvaluation.subtreeOutput_scaled_norm_sub_le line 51

Source documentation

The actual path weight times subtree sensitivity is bounded by the weighted cutoff errors on that subtree's own descendants.

theorem subtreeOutput_scaled_norm_sub_le {k N : ℕ} (h : k ≤ N) :
    ∀ (H H' : T.Node N → K) (v : T.Node k),
      W.pathWeight k v *
          ‖(E.subtreeOutput h H v : X) - E.subtreeOutput h H' v‖ ≤
        ∑ s ∈ T.descendants h v, W.pathWeight N s * ‖(H s : X) - H' s‖ := by
…

def OAI.ReflexiveFixedPoints.TreeEvaluation.terminalDefect line 83
Source documentation
The unweighted displacement of all maps strictly above terminal depth.
```
noncomputable def terminalDefect (N : ℕ) (b : K) : ℝ :=
…
```
def OAI.ReflexiveFixedPoints.TreeEvaluation.descendantLevelDefect line 88
Source documentation
Weighted map displacement on one level below a specified ancestor. Levels before the ancestor contribute zero.
```
noncomputable def descendantLevelDefect {k : ℕ} (v : T.Node k) (b : K)
    (d : ℕ) : ℝ := by
…
```
def OAI.ReflexiveFixedPoints.TreeEvaluation.internalDescendantDefect line 96
Source documentation
The exact finite weighted sum over internal descendants of a node.
```
noncomputable def internalDescendantDefect {k : ℕ} (N : ℕ) (b : K)
    (v : T.Node k) : ℝ :=
…
```
theorem OAI.ReflexiveFixedPoints.TreeEvaluation.internalDescendantDefect_self line 100
theorem OAI.ReflexiveFixedPoints.TreeEvaluation.internalDescendantDefect_succ line 107

theorem OAI.ReflexiveFixedPoints.TreeEvaluation.descendantLevelDefect_le line 116

Source documentation

Every descendant path weight is at most its ancestor's path weight.

theorem descendantLevelDefect_le {k : ℕ} (v : T.Node k) (b : K) (d : ℕ) :
    E.descendantLevelDefect v b d ≤
      W.pathWeight k v * ∑ s : T.Node d, ‖(E.map d s b : X) - b‖ := by
…

theorem OAI.ReflexiveFixedPoints.TreeEvaluation.internalDescendantDefect_le line 137
Source documentation
Summing the ancestor-weight comparisons gives the full unweighted terminal displacement budget, multiplied by just the ancestor's weight.
```
theorem internalDescendantDefect_le {k : ℕ} (N : ℕ) (b : K) (v : T.Node k) :
    E.internalDescendantDefect N b v ≤ W.pathWeight k v * E.terminalDefect N b := by
…
```

theorem OAI.ReflexiveFixedPoints.TreeEvaluation.subtreeOutput_const_scaled_norm_sub_le line 147

Source documentation

Exact scaled transmitted bound for a constant terminal assignment.

theorem subtreeOutput_const_scaled_norm_sub_le {k N : ℕ} (h : k ≤ N)
    (b : K) (v : T.Node k) :
    W.pathWeight k v * ‖(E.subtreeOutput h (fun _ => b) v : X) - b‖ ≤
      E.internalDescendantDefect N b v := by
…

theorem OAI.ReflexiveFixedPoints.TreeEvaluation.subtreeOutput_const_norm_sub_le_quotient line 183

Source documentation

Dividing by the positive weight gives the weighted internal-descendant error formula.

theorem subtreeOutput_const_norm_sub_le_quotient {k N : ℕ} (h : k ≤ N)
    (b : K) (v : T.Node k) :
    ‖(E.subtreeOutput h (fun _ => b) v : X) - b‖ ≤
      E.internalDescendantDefect N b v / W.pathWeight k v := by
…

theorem OAI.ReflexiveFixedPoints.TreeEvaluation.subtreeOutput_const_norm_sub_le_terminalDefect line 192
Source documentation
Constant terminal error is at most the total unweighted displacement. Only positivity of this one path weight is used to cancel it.
```
theorem subtreeOutput_const_norm_sub_le_terminalDefect {k N : ℕ} (h : k ≤ N)
    (b : K) (v : T.Node k) :
    ‖(E.subtreeOutput h (fun _ => b) v : X) - b‖ ≤ E.terminalDefect N b := by
…
```

theorem OAI.ReflexiveFixedPoints.TreeEvaluation.subtreeOutput_scaled_norm_sub_le_of_descendants_eq line 200

Source documentation

The scaled bound only needs constant terminal values below this node.

theorem subtreeOutput_scaled_norm_sub_le_of_descendants_eq {k N : ℕ} (h : k ≤ N)
    (H : T.Node N → K) (b : K) (v : T.Node k)
    (heq : ∀ s ∈ T.descendants h v, H s = b) :
    W.pathWeight k v * ‖(E.subtreeOutput h H v : X) - b‖ ≤
      E.internalDescendantDefect N b v := by
…

theorem OAI.ReflexiveFixedPoints.TreeEvaluation.subtreeOutput_norm_sub_le_terminalDefect line 210

Source documentation

A completely switched subtree has error bounded by the common terminal budget, regardless of all terminal values outside that subtree.

theorem subtreeOutput_norm_sub_le_terminalDefect {k N : ℕ} (h : k ≤ N)
    (H : T.Node N → K) (b : K) (v : T.Node k)
    (heq : ∀ s ∈ T.descendants h v, H s = b) :
    ‖(E.subtreeOutput h H v : X) - b‖ ≤ E.terminalDefect N b := by
…