FiniteTableModel.lean`

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.Problem310.FiniteTableModel.Child line 12
Source documentation
Child M is default and the other M children have selectors.
```
abbrev Child (M : ℕ) := Fin (M + 1)
```
abbrev OAI.Problem310.FiniteTableModel.Node line 15
Source documentation
Nodes at which a depth-d router still makes a decision.
```
abbrev Node (M d : ℕ) := {P : List (Child M) // P.length < d}
```
Mentions: OAI.Problem310.FiniteTableModel.Child
abbrev OAI.Problem310.FiniteTableModel.Leaf line 18
Source documentation
A terminal path. This is definitionally a list with the required length.
```
abbrev Leaf (M d : ℕ) := List.Vector (Child M) d
```
Mentions: OAI.Problem310.FiniteTableModel.Child
instance OAI.Problem310.FiniteTableModel.nodeFintype line 20
instance OAI.Problem310.FiniteTableModel.nodeMeasurableSpace line 28
instance OAI.Problem310.FiniteTableModel.nodeDiscreteMeasurableSpace line 29
instance OAI.Problem310.FiniteTableModel.leafMeasurableSpace line 30
instance OAI.Problem310.FiniteTableModel.leafDiscreteMeasurableSpace line 31
abbrev OAI.Problem310.FiniteTableModel.SelectorAddress line 34
Source documentation
Finite selector-table addresses include the table name as well as its key.
```
abbrev SelectorAddress {M d : ℕ} (b : Node M d → Fin M → ℕ) :=
…
```
Mentions: OAI.Problem310.FiniteTableModel.Node
abbrev OAI.Problem310.FiniteTableModel.TerminalAddress line 38
Source documentation
Terminal addresses include the leaf name, preventing collisions between tables.
```
abbrev TerminalAddress {M d : ℕ} (b : Leaf M d → ℕ) :=
…
```
Mentions: OAI.Problem310.FiniteTableModel.Leaf
instance OAI.Problem310.FiniteTableModel.selectorAddressMeasurableSpace line 41
instance OAI.Problem310.FiniteTableModel.selectorAddressDiscreteMeasurableSpace line 43
instance OAI.Problem310.FiniteTableModel.terminalAddressMeasurableSpace line 45
instance OAI.Problem310.FiniteTableModel.terminalAddressDiscreteMeasurableSpace line 47
abbrev OAI.Problem310.FiniteTableModel.SelectorTable line 50
abbrev OAI.Problem310.FiniteTableModel.TerminalTable line 51
def OAI.Problem310.FiniteTableModel.selectorAddress line 54
Source documentation
The center exposure consults exactly one deterministic coordinate per selector table.
```
def selectorAddress {M d : ℕ} (b : Node M d → Fin M → ℕ)
    (P : Node M d) (i : Fin M) (x : ℝ) : SelectorAddress b :=
…
```
Mentions: OAI.Problem310.FiniteTableModel.Node, OAI.Problem310.FiniteTableModel.SelectorAddress
def OAI.Problem310.FiniteTableModel.terminalAddress line 59
Source documentation
The terminal coordinate read along the selected leaf.
```
def terminalAddress {M d : ℕ} (b : Leaf M d → ℕ)
    (L : Leaf M d) (x : ℝ) : TerminalAddress b :=
…
```
Mentions: OAI.Problem310.FiniteTableModel.Leaf, OAI.Problem310.FiniteTableModel.TerminalAddress
def OAI.Problem310.FiniteTableModel.selectorValue line 64
Source documentation
Selector values are extended to all lists; routing uses only valid nodes.
```
def selectorValue {M d : ℕ} (b : Node M d → Fin M → ℕ) (ω : SelectorTable b)
    (P : List (Child M)) (i : Fin M) (x : ℝ) : Bool :=
…
```
Mentions: OAI.Problem310.FiniteTableModel.Node, OAI.Problem310.FiniteTableModel.SelectorTable, OAI.Problem310.FiniteTableModel.Child
theorem OAI.Problem310.FiniteTableModel.selectorValue_valid line 68
lemma OAI.Problem310.FiniteTableModel.measurable_dyadicKey line 73
lemma OAI.Problem310.FiniteTableModel.dyadicKey_add_one line 82
lemma OAI.Problem310.FiniteTableModel.measurable_selectorAddress line 87
lemma OAI.Problem310.FiniteTableModel.measurable_terminalAddress line 92
lemma OAI.Problem310.FiniteTableModel.measurable_selectorValue line 97
lemma OAI.Problem310.FiniteTableModel.selectorAddress_add_one line 107
lemma OAI.Problem310.FiniteTableModel.terminalAddress_add_one line 112
lemma OAI.Problem310.FiniteTableModel.selectorValue_add_one line 117
lemma OAI.Problem310.FiniteTableModel.center_selectorAddress_injective line 123
Source documentation
Exposing the center reads distinct coordinates because table names are retained.
```
lemma center_selectorAddress_injective {M d : ℕ} (b : Node M d → Fin M → ℕ)
    (x : ℝ) : Function.Injective (fun e : Node M d × Fin M => selectorAddress b e.1 e.2 x) := by
…
```
Mentions: OAI.Problem310.FiniteTableModel.Node, OAI.Problem310.FiniteTableModel.selectorAddress
lemma OAI.Problem310.FiniteTableModel.selectorAddress_ne_center line 128
lemma OAI.Problem310.FiniteTableModel.dyadicKey_eq_of_refine line 136
lemma OAI.Problem310.FiniteTableModel.selectorValue_eq_of_key_eq line 144
Source documentation
Any selector lookup at a coarser resolution is determined by a finest key.
```
lemma selectorValue_eq_of_key_eq {M d : ℕ} (b : Node M d → Fin M → ℕ)
    (ω : SelectorTable b) (P : List (Child M)) (i : Fin M) (B : ℕ)
    (hlevel : ∀ h : P.length < d, b ⟨P, h⟩ i ≤ B) {x y : ℝ}
    (hkey : GridSeparation.dyadicKey B x = GridSeparation.dyadicKey B y) :
    selectorValue b ω P i x = selectorValue b ω P i y := by
…
```
Mentions: OAI.Problem310.FiniteTableModel.Node, OAI.Problem310.FiniteTableModel.SelectorTable, OAI.Problem310.FiniteTableModel.Child, OAI.Problem310.GridSeparation.dyadicKey, OAI.Problem310.FiniteTableModel.selectorValue
lemma OAI.Problem310.FiniteTableModel.terminal_lookup_eq_of_key_eq line 158
Source documentation
At a fixed leaf, the finer key also determines the terminal table lookup.
```
lemma terminal_lookup_eq_of_key_eq {M d : ℕ} (b : Leaf M d → ℕ)
    (ω : TerminalTable b) (L : Leaf M d) (B : ℕ) (hlevel : b L ≤ B) {x y : ℝ}
    (hkey : GridSeparation.dyadicKey B x = GridSeparation.dyadicKey B y) :
    ω (terminalAddress b L x) = ω (terminalAddress b L y) := by
…
```
Mentions: OAI.Problem310.FiniteTableModel.Leaf, OAI.Problem310.FiniteTableModel.TerminalTable, OAI.Problem310.GridSeparation.dyadicKey, OAI.Problem310.FiniteTableModel.terminalAddress