FirstDefaultSelection.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem310.FirstDefault.cylinder_iff_chooseChild line 15
Source documentation
A path cylinder is exactly the event that first-success routing selects its prescribed child at each of its prescribed nodes.
```
theorem cylinder_iff_chooseChild {M d : ℕ} {Ω : Type u_Ω}
    (S : Address M → Ω → Bool) (f : Path M d) (ω : Ω) :
    ω ∈ cylinder S f ↔ ∀ k : Fin d,
      OrderedRouting.chooseChild (fun j => S (pathPrefix f k, j) ω) = (f k).castSucc := by
…
```
Mentions: OAI.Problem310.FirstDefault.Address, OAI.Problem310.FirstDefault.Path, OAI.Problem310.FirstDefault.cylinder, OAI.Problem310.OrderedRouting.chooseChild, OAI.Problem310.FirstDefault.pathPrefix
def OAI.Problem310.FirstDefault.centerChoice line 46
Source documentation
Canonical child choice from a family of selector bits at tree addresses.
```
def centerChoice {M : ℕ} {Ω : Type u_Ω} (S : Address M → Ω → Bool)
    (P : List (Fin (M + 1))) (ω : Ω) : Fin (M + 1) :=
…
```
Mentions: OAI.Problem310.FirstDefault.Address
theorem OAI.Problem310.FirstDefault.noDefault_iff_mem_cylinders line 52
Source documentation
The actual routed center avoids the default exactly on the finite union of the path cylinders used by the exact first-default probability law.
```
theorem noDefault_iff_mem_cylinders {M d : ℕ} {Ω : Type u_Ω}
    (S : Address M → Ω → Bool) (ω : Ω) :
    (∀ k < d, centerChoice S (RoutingPath.routeFrom (centerChoice S) k [] ω) ω ≠
      Fin.last M) ↔ ω ∈ ⋃ f : Path M d, cylinder S f := by
…
```
Mentions: OAI.Problem310.FirstDefault.Address, OAI.Problem310.FirstDefault.centerChoice, OAI.Problem310.RoutingPath.routeFrom, OAI.Problem310.FirstDefault.Path, OAI.Problem310.FirstDefault.cylinder
theorem OAI.Problem310.FirstDefault.noDefault_event_eq_cylinders line 67
Source documentation
The equality is also available as a set rewrite for probability measures.
```
theorem noDefault_event_eq_cylinders {M d : ℕ} {Ω : Type u_Ω}
    (S : Address M → Ω → Bool) :
    {ω | ∀ k < d, centerChoice S (RoutingPath.routeFrom (centerChoice S) k [] ω) ω ≠
      Fin.last M} = ⋃ f : Path M d, cylinder S f := by
…
```
Mentions: OAI.Problem310.FirstDefault.Address, OAI.Problem310.FirstDefault.centerChoice, OAI.Problem310.RoutingPath.routeFrom, OAI.Problem310.FirstDefault.Path, OAI.Problem310.FirstDefault.cylinder

theorem OAI.Problem310.FirstDefault.routeFrom_change_parameter line 75

Source documentation

Change the auxiliary parameter space without changing any node choices.

theorem routeFrom_change_parameter {ι : Type u_ι} {X : Type u_X} {Y : Type u_Y}
    (f : List ι → X → ι) (g : List ι → Y → ι) (x : X) (y : Y)
    (h : ∀ P, f P x = g P y) (n : ℕ) (P : List ι) :
    RoutingPath.routeFrom f n P x = RoutingPath.routeFrom g n P y := by
…

Mentions: OAI.Problem310.RoutingPath.routeFrom

theorem OAI.Problem310.FirstDefault.default_not_mem_iff_mem_cylinders line 84
Source documentation
Equivalent leaf-membership formulation, convenient for concrete routers.
```
theorem default_not_mem_iff_mem_cylinders {M d : ℕ} {Ω : Type u_Ω}
    (S : Address M → Ω → Bool) (ω : Ω) :
    Fin.last M ∉ RoutingPath.routeFrom (centerChoice S) d [] ω ↔
      ω ∈ ⋃ f : Path M d, cylinder S f := by
…
```
Mentions: OAI.Problem310.FirstDefault.Address, OAI.Problem310.RoutingPath.routeFrom, OAI.Problem310.FirstDefault.centerChoice, OAI.Problem310.FirstDefault.Path, OAI.Problem310.FirstDefault.cylinder
theorem OAI.Problem310.FirstDefault.spatial_default_not_mem_iff line 93
Source documentation
Spatially parametrized selectors have the same no-default event as the cylinders at a fixed center. This is directly usable with selectorValue.
```
theorem spatial_default_not_mem_iff {M d : ℕ} {Ω : Type u_Ω} {X : Type u_X}
    (S : Ω → List (Fin (M + 1)) → Fin M → X → Bool) (ω : Ω) (x : X) :
    Fin.last M ∉ RoutingPath.routeFrom
      (fun P y => OrderedRouting.chooseChild (fun j => S ω P j y)) d [] x ↔
      ω ∈ ⋃ f : Path M d,
        cylinder (fun a ω' => S ω' a.1 a.2 x) f := by
…
```
Mentions: OAI.Problem310.RoutingPath.routeFrom, OAI.Problem310.OrderedRouting.chooseChild, OAI.Problem310.FirstDefault.Path, OAI.Problem310.FirstDefault.cylinder