FiniteVectorRestrictions.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Coordinate restrictions of the finite subtree vectors.

theorem OAI.TreeEdit.BinaryLower.FiniteVectors.u_on_child line 13
Source documentation
On a child's subtree the parent's cheap vector equals that child's distinguished vector.
```
theorem u_on_child (p : Fin k → Fin m → ℕ) (j : ℕ) (hj : j < k)
    (a b : Leaf m k) (i : Fin m)
    (hab : Agrees (j + 1) (Function.update a ⟨j, hj⟩ i) b) :
    u p j a b = w p (j + 1) (Function.update a ⟨j, hj⟩ i) b := by
…
```
Mentions: OAI.TreeEdit.BinaryLower.FiniteVectors.Leaf, OAI.TreeEdit.BinaryLower.FiniteVectors.Agrees, OAI.TreeEdit.BinaryLower.FiniteVectors.u, OAI.TreeEdit.BinaryLower.FiniteVectors.w
theorem OAI.TreeEdit.BinaryLower.FiniteVectors.w_on_child line 21
Source documentation
The parent's distinguished vector restricts to R times the child's.
```
theorem w_on_child (p : Fin k → Fin m → ℕ) (j : ℕ) (hj : j < k)
    (a b : Leaf m k) (i : Fin m)
    (hab : Agrees (j + 1) (Function.update a ⟨j, hj⟩ i) b) :
    w p j a b = levelProduct p ⟨j, hj⟩ •
      w p (j + 1) (Function.update a ⟨j, hj⟩ i) b := by
…
```
Mentions: OAI.TreeEdit.BinaryLower.FiniteVectors.Leaf, OAI.TreeEdit.BinaryLower.FiniteVectors.Agrees, OAI.TreeEdit.BinaryLower.FiniteVectors.w, OAI.TreeEdit.BinaryLower.FiniteVectors.levelProduct
theorem OAI.TreeEdit.BinaryLower.FiniteVectors.u_off_subtree line 29
theorem OAI.TreeEdit.BinaryLower.FiniteVectors.w_off_subtree line 33
theorem OAI.TreeEdit.BinaryLower.FiniteVectors.translate_u_off_subtree line 39
Source documentation
A leaf coordinate outside a subtree is fixed by every integer multiple of its cheap vector.
```
theorem translate_u_off_subtree (p : Fin k → Fin m → ℕ) (j : ℕ)
    (a b : Leaf m k) (hab : ¬ Agrees j a b) (x : State p) (t : ℤ) :
    (x + t • u p j a) b = x b := by
…
```
Mentions: OAI.TreeEdit.BinaryLower.FiniteVectors.Leaf, OAI.TreeEdit.BinaryLower.FiniteVectors.Agrees, OAI.TreeEdit.BinaryLower.FiniteVectors.State, OAI.TreeEdit.BinaryLower.FiniteVectors.u
theorem OAI.TreeEdit.BinaryLower.FiniteVectors.translate_w_off_subtree line 45
Source documentation
The same support statement for the distinguished vector.
```
theorem translate_w_off_subtree (p : Fin k → Fin m → ℕ) (j : ℕ)
    (a b : Leaf m k) (hab : ¬ Agrees j a b) (x : State p) (t : ℤ) :
    (x + t • w p j a) b = x b := by
…
```
Mentions: OAI.TreeEdit.BinaryLower.FiniteVectors.Leaf, OAI.TreeEdit.BinaryLower.FiniteVectors.Agrees, OAI.TreeEdit.BinaryLower.FiniteVectors.State, OAI.TreeEdit.BinaryLower.FiniteVectors.w