BlockBefore.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

The actual root output before switching a descendant block

We follow one node through the recursive nonlinear evaluation. The other child outputs contribute at most their total weight because they lie in a set of diameter at most one. The error along the chosen path is the actual displacement of its ancestor maps at the comparison point.

theorem OAI.ReflexiveFixedPoints.weighted_focus_sum_le line 23

Source documentation

Separate one term of a normalized weighted sum. Only the other terms need to be bounded by one.

theorem weighted_focus_sum_le {ι : Type*} (s : Finset ι) (w D : ι → ℝ)
    (v : ι) (hv : v ∈ s)
    (hw : ∀ i ∈ s, 0 ≤ w i) (hsum : ∑ i ∈ s, w i = 1)
    (hD : ∀ i ∈ s, i ≠ v → D i ≤ 1) :
    (∑ i ∈ s, w i * D i) ≤ w v * D v + (1 - w v) := by
…

def OAI.ReflexiveFixedPoints.TreeEvaluation.pathDisplacement line 49

Source documentation

Sum the actual displacement at the proper ancestors of the selected node.

def pathDisplacement : (k : ℕ) → T.Node k → K → ℝ
  | 0, _, _ => 0
  | k + 1, v, z => pathDisplacement k (T.parent k v) z +
      ‖(E.map k (T.parent k v) z : X) - z‖

theorem OAI.ReflexiveFixedPoints.TreeEvaluation.pathDisplacement_zero line 54
theorem OAI.ReflexiveFixedPoints.TreeEvaluation.pathDisplacement_succ line 57

def OAI.ReflexiveFixedPoints.TreeEvaluation.weightedPathDisplacement line 62

Source documentation

The same ancestor displacements weighted by their actual root path mass.

def weightedPathDisplacement : (k : ℕ) → T.Node k → K → ℝ
  | 0, _, _ => 0
  | k + 1, v, z => weightedPathDisplacement k (T.parent k v) z +
      W.pathWeight k (T.parent k v) * ‖(E.map k (T.parent k v) z : X) - z‖

theorem OAI.ReflexiveFixedPoints.TreeEvaluation.weightedPathDisplacement_zero line 67
theorem OAI.ReflexiveFixedPoints.TreeEvaluation.weightedPathDisplacement_succ line 70
theorem OAI.ReflexiveFixedPoints.TreeEvaluation.pathDisplacement_nonneg line 75
theorem OAI.ReflexiveFixedPoints.TreeEvaluation.weightedPathDisplacement_nonneg line 81
theorem OAI.ReflexiveFixedPoints.TreeEvaluation.weightedPathDisplacement_le_pathDisplacement line 90
Source documentation
Dropping path weights can only increase this sum of nonnegative errors.
```
theorem weightedPathDisplacement_le_pathDisplacement (k : ℕ) (v : T.Node k) (z : K) :
    E.weightedPathDisplacement k v z ≤ E.pathDisplacement k v z := by
…
```

theorem OAI.ReflexiveFixedPoints.TreeEvaluation.collapse_focus_norm_sub_le line 102

Source documentation

Focus one actual child while bounding all off-path child outputs by the diameter of the set. The node map is used only through nonexpansiveness.

theorem collapse_focus_norm_sub_le
    (hdiam : ∀ a b : K, ‖(a : X) - b‖ ≤ 1)
    (k : ℕ) (H : T.Node (k + 1) → K) (v : T.Node (k + 1)) (z : K) :
    ‖(E.collapse k H (T.parent k v) : X) - z‖ ≤
      W.weight k v * ‖(H v : X) - z‖ + (1 - W.weight k v) +
        ‖(E.map k (T.parent k v) z : X) - z‖ := by
…

theorem OAI.ReflexiveFixedPoints.TreeEvaluation.evaluate_focus_norm_sub_le line 119

Source documentation

Follow one selected cutoff value through the actual nonlinear evaluation. No affinity or positive lower bound on path weights is used.

theorem evaluate_focus_norm_sub_le
    (hdiam : ∀ a b : K, ‖(a : X) - b‖ ≤ 1)
    (k : ℕ) (H : T.Node k → K) (v : T.Node k) (z : K) :
    ‖(E.evaluate k H : X) - z‖ ≤
      W.pathWeight k v * ‖(H v : X) - z‖ + (1 - W.pathWeight k v) +
        E.weightedPathDisplacement k v z := by
…

theorem OAI.ReflexiveFixedPoints.TreeEvaluation.before_block_bound line 151

Source documentation

The before-block root bound from the actual focused cutoff error and the actual unweighted ancestor displacement budget.

theorem before_block_bound
    (hdiam : ∀ a b : K, ‖(a : X) - b‖ ≤ 1)
    (k : ℕ) (H : T.Node k → K) (v : T.Node k) (z : K) {e : ℝ}
    (hfocused : ‖(H v : X) - z‖ ≤ e)
    (hpath : E.pathDisplacement k v z ≤ e) :
    ‖(E.evaluate k H : X) - z‖ ≤ 1 - W.pathWeight k v + 2 * e := by
…