LocalPredicateFactor.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem310.LocalPredicateFactor.route_eq_of_key_eq line 18

Source documentation

Routing through a subtree only uses its strict-descendant choices. If those choices factor through one key, the terminal leaf does too.

theorem route_eq_of_key_eq (choose : List ι → X → ι)
    (key : X → K) (r : ℕ) (P : List ι)
    (hchoice : ∀ Q : List ι, P.IsPrefix Q → Q.length < P.length + r →
      ∀ x y : X, key x = key y → choose Q x = choose Q y)
    {x y : X} (hxy : key x = key y) :
    routeFrom choose r P x = routeFrom choose r P y := by
…

theorem OAI.Problem310.LocalPredicateFactor.terminal_eq_of_key_eq line 33

Source documentation

A terminal output on a routed subtree factors through a common key provided every choice and every possible terminal output does.

theorem terminal_eq_of_key_eq (choose : List ι → X → ι)
    (terminal : List ι → X → V) (key : X → K) (r : ℕ) (P : List ι)
    (hchoice : ∀ Q : List ι, P.IsPrefix Q → Q.length < P.length + r →
      ∀ x y : X, key x = key y → choose Q x = choose Q y)
    (hterminal : ∀ Q : List ι, P.IsPrefix Q → Q.length = P.length + r →
      ∀ x y : X, key x = key y → terminal Q x = terminal Q y)
    {x y : X} (hxy : key x = key y) :
    terminal (routeFrom choose r P x) x = terminal (routeFrom choose r P y) y := by
…

theorem OAI.Problem310.LocalPredicateFactor.local_predicate_eq_of_key_eq line 48

Source documentation

An incoming selector multiplied by a local terminal predicate also factors through that key. This includes a child which is already a leaf.

theorem local_predicate_eq_of_key_eq (choose : List ι → X → ι)
    (terminal : List ι → X → Bool) (incoming : X → Bool)
    (key : X → K) (r : ℕ) (P : List ι)
    (hchoice : ∀ Q : List ι, P.IsPrefix Q → Q.length < P.length + r →
      ∀ x y : X, key x = key y → choose Q x = choose Q y)
    (hterminal : ∀ Q : List ι, P.IsPrefix Q → Q.length = P.length + r →
      ∀ x y : X, key x = key y → terminal Q x = terminal Q y)
    (hincoming : ∀ x y : X, key x = key y → incoming x = incoming y)
    {x y : X} (hxy : key x = key y) :
    (incoming x && terminal (routeFrom choose r P x) x) =
      (incoming y && terminal (routeFrom choose r P y) y) := by
…

theorem OAI.Problem310.LocalPredicateFactor.table_eq_of_finest_key line 63

Source documentation

A single table evaluated at any coarser grid is a function of the finest key.

theorem table_eq_of_finest_key {b B : ℕ} (hb : b ≤ B)
    (table : Fin (2 ^ (b + 2)) → V) {x y : ℝ}
    (hxy : ⌊(2 : ℝ) ^ (B + 2) * Int.fract x⌋ =
      ⌊(2 : ℝ) ^ (B + 2) * Int.fract y⌋) :
    table (dyadicKey b x) = table (dyadicKey b y) := by
…

theorem OAI.Problem310.LocalPredicateFactor.choice_eq_of_finest_key line 76

Source documentation

An arbitrary deterministic rule applied to selector-table lookups depends only on a common finer key. In particular this applies to first-success routing.

theorem choice_eq_of_finest_key (b : J → ℕ) (B : ℕ)
    (tables : ∀ j, Fin (2 ^ (b j + 2)) → Bool)
    (rule : (J → Bool) → ι) (hb : ∀ j, b j ≤ B) {x y : ℝ}
    (hxy : ⌊(2 : ℝ) ^ (B + 2) * Int.fract x⌋ =
      ⌊(2 : ℝ) ^ (B + 2) * Int.fract y⌋) :
    rule (fun j => tables j (dyadicKey (b j) x)) =
      rule (fun j => tables j (dyadicKey (b j) y)) := by
…

def OAI.Problem310.LocalPredicateFactor.gridChoice line 89
Source documentation
A table-based node rule, with no restriction on which deterministic first-success/default convention the rule uses.
```
def gridChoice (b : List ι → J → ℕ)
    (tables : ∀ Q j, Fin (2 ^ (b Q j + 2)) → Bool)
    (rule : List ι → (J → Bool) → ι) (Q : List ι) (x : ℝ) : ι :=
…
```
def OAI.Problem310.LocalPredicateFactor.gridTerminal line 94

theorem OAI.Problem310.LocalPredicateFactor.grid_local_predicate_factors line 101

Source documentation

The incoming selector and every table in a child subtree may have different resolutions. A bound on all those resolutions gives exactly the common-key factorization needed for deterministic scale representatives.

theorem grid_local_predicate_factors
    (b : List ι → J → ℕ) (c : List ι → ℕ) (bIn B : ℕ)
    (selectors : ∀ Q j, Fin (2 ^ (b Q j + 2)) → Bool)
    (terminals : ∀ Q, Fin (2 ^ (c Q + 2)) → Bool)
    (incoming : Fin (2 ^ (bIn + 2)) → Bool)
    (rule : List ι → (J → Bool) → ι) (r : ℕ) (P : List ι)
    (hb : ∀ Q : List ι, P.IsPrefix Q → Q.length < P.length + r →
      ∀ j, b Q j ≤ B)
    (hc : ∀ Q : List ι, P.IsPrefix Q → Q.length = P.length + r → c Q ≤ B)
    (hIn : bIn ≤ B) {x y : ℝ}
    (hxy : ⌊(2 : ℝ) ^ (B + 2) * Int.fract x⌋ =
      ⌊(2 : ℝ) ^ (B + 2) * Int.fract y⌋) :
…