BlockEstimates.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Detection of actual switched descendant blocks

The before and after estimates are proved for the actual root states. The ideal cutoff contains labels strictly to the left and the common terminal point elsewhere. Its identification with an earlier prediction is supplied by the candidate construction, after which the terminal detector applies.

def OAI.ReflexiveFixedPoints.TreeEvaluation.idealCutoff line 28
Source documentation
The ideal state at a cutoff immediately after a whole block has switched.
```
def idealCutoff (k : ℕ) (x b : K) (v : T.Node k) : T.Node k → K :=
…
```

theorem OAI.ReflexiveFixedPoints.TreeEvaluation.beforeBlock_norm_sub_label_le line 32

Source documentation

The actual before-block root is close to the selected node's label.

theorem beforeBlock_norm_sub_label_le
    (hdiam : ∀ a c : K, ‖(a : X) - c‖ ≤ 1)
    (x b : K) (τ : ℕ → ℝ) {k N : ℕ} (h : k ≤ N) (v : T.Node k)
    (haverage : ∀ d, d < N → ∀ p : T.Node d,
      ‖(E.childAverage d (fun c => E.map (d + 1) c x) p : X) - x‖ ≤ τ d)
    {e : ℝ} (htail : (∑ d ∈ Finset.Ico k N, τ d) ≤ e)
    (hpath : E.pathDisplacement k v (E.map k v x) ≤ e) :
    ‖(E.beforeBlock h (fun s => E.map N s x) b v : X) - E.map k v x‖ ≤
      1 - W.pathWeight k v + 2 * e := by
…

theorem OAI.ReflexiveFixedPoints.TreeEvaluation.afterBlock_norm_sub_ideal_le line 52

Source documentation

Uniform errors of untouched and transmitted subtrees give the actual post-block root's distance from its ideal cutoff evaluation.

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

theorem OAI.ReflexiveFixedPoints.TreeEvaluation.actual_block_detection line 79

Source documentation

The exact W_v - 5e_v lower bound for an actual before-minus-after block increment, proved from the actual child averages and ancestor displacements.

theorem actual_block_detection
    (hdiam : ∀ a c : K, ‖(a : X) - c‖ ≤ 1)
    (x b : K) (τ : ℕ → ℝ) {k N : ℕ} (h : k ≤ N) (v : T.Node k)
    (haverage : ∀ d, d < N → ∀ p : T.Node d,
      ‖(E.childAverage d (fun c => E.map (d + 1) c x) p : X) - x‖ ≤ τ d)
    (f : X →L[ℝ] ℝ) (hf : ‖f‖ ≤ 1) {e : ℝ}
    (htail : (∑ d ∈ Finset.Ico k N, τ d) ≤ e)
    (hpath : E.pathDisplacement k v (E.map k v x) ≤ e)
    (hterminal : E.terminalDefect N b ≤ e)
    (hdetect : 1 - 2 * e ≤
      f ((E.map k v x : X) - E.evaluate k (E.idealCutoff k x b v))) :
    W.pathWeight k v - 5 * e ≤
…