RoutingPath.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem310.RoutingPath.routeFrom line 15
Source documentation
Route from a node by appending the locally selected child at each step. The choice rule is abstract: a first-success/default selector can be supplied.
```
def routeFrom (choose : List ι → X → ι) : ℕ → List ι → X → List ι
  | 0, P, _ => P
  | n + 1, P, x =>
      let Q := routeFrom choose n P x
…
```
theorem OAI.Problem310.RoutingPath.routeFrom_zero line 21
theorem OAI.Problem310.RoutingPath.routeFrom_succ line 24
theorem OAI.Problem310.RoutingPath.length_routeFrom line 28

theorem OAI.Problem310.RoutingPath.routeFrom_add line 36

Source documentation

A route can be resumed at any intermediate node.

theorem routeFrom_add (choose : List ι → X → ι)
    (n m : ℕ) (P : List ι) (x : X) :
    routeFrom choose (n + m) P x =
      routeFrom choose m (routeFrom choose n P x) x := by
…

Mentions: OAI.Problem310.RoutingPath.routeFrom

theorem OAI.Problem310.RoutingPath.prefix_routeFrom line 45
Source documentation
Every routed node extends the starting node.
```
theorem prefix_routeFrom (choose : List ι → X → ι)
    (n : ℕ) (P : List ι) (x : X) : P.IsPrefix (routeFrom choose n P x) := by
…
```
Mentions: OAI.Problem310.RoutingPath.routeFrom

theorem OAI.Problem310.RoutingPath.routeFrom_eq_of_choices_eq line 54

Source documentation

Earlier decisions along one path suffice to preserve the full common prefix. No restriction is imposed on decisions off that path.

theorem routeFrom_eq_of_choices_eq (choose : List ι → X → ι)
    (n : ℕ) (P : List ι) (x y : X)
    (hchoice : ∀ k < n,
      choose (routeFrom choose k P x) y = choose (routeFrom choose k P x) x) :
    routeFrom choose n P y = routeFrom choose n P x := by
…

Mentions: OAI.Problem310.RoutingPath.routeFrom

theorem OAI.Problem310.RoutingPath.routeFrom_eq_local_route line 67

Source documentation

Preservation through an ancestor prefix followed by one specified local child identifies the actual terminal leaf with the locally routed leaf.

theorem routeFrom_eq_local_route (choose : List ι → X → ι)
    (k r : ℕ) (P U : List ι) (x y : X) (i : ι)
    (hU : routeFrom choose k P x = U)
    (hchoice : ∀ l < k,
      choose (routeFrom choose l P x) y = choose (routeFrom choose l P x) x)
    (hi : choose U y = i) :
    routeFrom choose (k + 1 + r) P y = routeFrom choose r (U ++ [i]) y := by
…

Mentions: OAI.Problem310.RoutingPath.routeFrom

theorem OAI.Problem310.RoutingPath.terminal_success_of_local_success line 81

Source documentation

Generic local-success implication used by random routing: once the prefix is preserved and child i is selected, the local terminal predicate is exactly the terminal predicate of the actual root route.

theorem terminal_success_of_local_success (choose : List ι → X → ι)
    (terminal : List ι → X → Prop) (k r : ℕ) (P U : List ι)
    (x y : X) (i : ι)
    (hU : routeFrom choose k P x = U)
    (hchoice : ∀ l < k,
      choose (routeFrom choose l P x) y = choose (routeFrom choose l P x) x)
    (hi : choose U y = i)
    (hlocal : terminal (routeFrom choose r (U ++ [i]) y) y) :
    terminal (routeFrom choose (k + 1 + r) P y) y := by
…

Mentions: OAI.Problem310.RoutingPath.routeFrom

theorem OAI.Problem310.RoutingPath.routeFrom_prefix_of_le line 94
Source documentation
Every earlier routed node is a prefix of every later routed node.
```
theorem routeFrom_prefix_of_le (choose : List ι → X → ι)
    (P : List ι) (x : X) {k d : ℕ} (hkd : k ≤ d) :
    (routeFrom choose k P x).IsPrefix (routeFrom choose d P x) := by
…
```
Mentions: OAI.Problem310.RoutingPath.routeFrom

theorem OAI.Problem310.RoutingPath.take_routeFrom line 102

Source documentation

Truncating a routed leaf recovers the intermediate routed node.

theorem take_routeFrom (choose : List ι → X → ι)
    (P : List ι) (x : X) {k d : ℕ} (hkd : k ≤ d) :
    (routeFrom choose d P x).take (P.length + k) = routeFrom choose k P x := by
…

Mentions: OAI.Problem310.RoutingPath.routeFrom

theorem OAI.Problem310.RoutingPath.routeFrom_eq_take_of_choices line 112

Source documentation

Prescribed decisions on all initial segments determine a route.

theorem routeFrom_eq_take_of_choices (choose : List ι → X → ι)
    (L : List ι) (x : X)
    (hchoice : ∀ (k : ℕ) (hk : k < L.length), choose (L.take k) x = L[k])
    {n : ℕ} (hn : n ≤ L.length) : routeFrom choose n [] x = L.take n := by
…

Mentions: OAI.Problem310.RoutingPath.routeFrom

theorem OAI.Problem310.RoutingPath.routeFrom_eq_iff_choices line 125
Source documentation
Path-cylinder characterization: a terminal route equals a prescribed list exactly when each successive decision follows that list.
```
theorem routeFrom_eq_iff_choices (choose : List ι → X → ι) (L : List ι) (x : X) :
    routeFrom choose L.length [] x = L ↔
      ∀ (k : ℕ) (hk : k < L.length), choose (L.take k) x = L[k] := by
…
```
Mentions: OAI.Problem310.RoutingPath.routeFrom
theorem OAI.Problem310.RoutingPath.noDefault_iff_not_mem line 142
Source documentation
Avoiding a default at every decision is the same as avoiding it in the terminal path (for a route starting at the root).
```
theorem noDefault_iff_not_mem (choose : List ι → X → ι)
    (default : ι) (d : ℕ) (x : X) :
    (∀ k < d, choose (routeFrom choose k [] x) x ≠ default) ↔
      default ∉ routeFrom choose d [] x := by
…
```
Mentions: OAI.Problem310.RoutingPath.routeFrom

theorem OAI.Problem310.RoutingPath.noDefault_iff_exists_path line 163

Source documentation

A route with no default child is represented by a vector of nondefault children. This is the deterministic event equality needed for path-cylinder probability estimates.

theorem noDefault_iff_exists_path {M : ℕ}
    (choose : List (Fin (M + 1)) → X → Fin (M + 1)) (d : ℕ) (x : X) :
    (∀ k < d, choose (routeFrom choose k [] x) x ≠ Fin.last M) ↔
      ∃ f : Fin d → Fin M,
        routeFrom choose d [] x = List.ofFn (fun i => (f i).castSucc) := by
…

Mentions: OAI.Problem310.RoutingPath.routeFrom

theorem OAI.Problem310.RoutingPath.noDefault_iff_exists_choices line 194

Source documentation

The no-default event is a union of the prescribed nondefault path cylinders.

theorem noDefault_iff_exists_choices {M : ℕ}
    (choose : List (Fin (M + 1)) → X → Fin (M + 1)) (d : ℕ) (x : X) :
    (∀ k < d, choose (routeFrom choose k [] x) x ≠ Fin.last M) ↔
      ∃ f : Fin d → Fin M, ∀ (k : ℕ) (hk : k < d),
        choose ((List.ofFn (fun i => (f i).castSucc)).take k) x =
          (f ⟨k, hk⟩).castSucc := by
…

Mentions: OAI.Problem310.RoutingPath.routeFrom

theorem OAI.Problem310.RoutingPath.child_eq_of_prefix line 215
Source documentation
Two different immediate child subtrees cannot share a descendant.
```
theorem child_eq_of_prefix {P L : List ι} {i j : ι}
    (hi : (P ++ [i]).IsPrefix L) (hj : (P ++ [j]).IsPrefix L) : i = j := by
…
```
theorem OAI.Problem310.RoutingPath.routeFrom_ne_of_distinct_children line 225
Source documentation
Local terminal leaves in different child subtrees have distinct addresses, regardless of how the selectors route inside either subtree.
```
theorem routeFrom_ne_of_distinct_children (choose : List ι → X → ι)
    (r s : ℕ) (P : List ι) (x y : X) {i j : ι} (hij : i ≠ j) :
    routeFrom choose r (P ++ [i]) x ≠ routeFrom choose s (P ++ [j]) y := by
…
```
Mentions: OAI.Problem310.RoutingPath.routeFrom

theorem OAI.Problem310.RoutingPath.exists_first_default line 235

Source documentation

A first default on a finite route has a well-defined first occurrence.

theorem exists_first_default (choose : List ι → X → ι)
    (d : ℕ) (P : List ι) (x : X) (default : ι)
    (h : ∃ k < d, choose (routeFrom choose k P x) x = default) :
    ∃ k < d, choose (routeFrom choose k P x) x = default ∧
      ∀ l < k, choose (routeFrom choose l P x) x ≠ default := by
…

Mentions: OAI.Problem310.RoutingPath.routeFrom

theorem OAI.Problem310.RoutingPath.routeFrom_periodic line 246

Source documentation

Periodic node choices give periodic routed leaves.

theorem routeFrom_periodic (choose : List ι → ℝ → ι)
    (hchoose : ∀ P x, choose P (x + 1) = choose P x)
    (n : ℕ) (P : List ι) (x : ℝ) :
    routeFrom choose n P (x + 1) = routeFrom choose n P x := by
…

Mentions: OAI.Problem310.RoutingPath.routeFrom

theorem OAI.Problem310.RoutingPath.measurable_routeFrom line 256

Source documentation

Measurability of the finite router over a countable discrete child alphabet. The joint node-choice map is the only input required from the table model.

theorem measurable_routeFrom [Countable ι]
    [MeasurableSpace X] [MeasurableSpace ι] [MeasurableSingletonClass ι]
    [MeasurableSpace (List ι)] [MeasurableSingletonClass (List ι)]
    (choose : List ι → X → ι)
    (hchoose : Measurable (Function.uncurry choose)) (n : ℕ) (P : List ι) :
    Measurable (routeFrom choose n P) := by
…

Mentions: OAI.Problem310.RoutingPath.routeFrom