FiniteTreeConcreteCosts.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Concrete tagged cyclic-state versions of lem:finite-cost. The only input about a translated vector is its actual coordinate support. In particular no injectivity of the word map, period identity, or distortion hypothesis is used.

theorem OAI.TreeEdit.BinaryLower.FiniteTree.root_leaf_supported_script line 14
theorem OAI.TreeEdit.BinaryLower.FiniteTree.root_leaf_supported_cost line 34
Source documentation
The pointwise single-coordinate cost, for any value of the translation in that cyclic coordinate and at every state.
```
theorem root_leaf_supported_cost {m k : ℕ} (T : ℕ)
    (Q : Leaf m k → ℕ) (base ell : Leaf m k)
    (u : List (Fin m) → State Q) (z x : State Q)
    (hsupport : ∀ l : Leaf m k, l ≠ ell → z l = 0) :
    ed (nodeWord T (leafDecoder Q base) u k [] x)
      (nodeWord T (leafDecoder Q base) u k [] (x + z)) ≤ T ^ k :=
…
```
Mentions: OAI.TreeEdit.BinaryLower.FiniteTree.Leaf, OAI.TreeEdit.BinaryLower.FiniteTree.State, OAI.TreeEdit.ed, OAI.TreeEdit.BinaryLower.FiniteTree.nodeWord, OAI.TreeEdit.BinaryLower.FiniteTree.leafDecoder
theorem OAI.TreeEdit.BinaryLower.FiniteTree.root_leaf_supported_normalized_cost line 43
theorem OAI.TreeEdit.BinaryLower.FiniteTree.root_internal_supported_script line 58
theorem OAI.TreeEdit.BinaryLower.FiniteTree.root_internal_supported_cost line 79

theorem OAI.TreeEdit.BinaryLower.FiniteTree.root_internal_supported_normalized_cost line 93

Source documentation

Exactly the root-word normalized row-translation estimate, for the tagged cyclic-state decoder and a subtree-supported cheap vector.

theorem root_internal_supported_normalized_cost {m k : ℕ} (T : ℕ)
    (hm : 0 < m) (hT : 0 < T)
    (Q : Leaf m k → ℕ) (base : Leaf m k)
    (u : List (Fin m) → State Q) (h : ℕ) (q : List (Fin m))
    (hlen : h + 1 + q.length = k) (s : ℕ) (hs : s ≤ T)
    (hsupport : ∀ l : Leaf m k, ¬ q.IsPrefix l.val → u q l = 0)
    (x : State Q) :
    (ed (nodeWord T (leafDecoder Q base) u k [] x)
      (nodeWord T (leafDecoder Q base) u k [] (x + s • u q)) : ℝ) ≤
      (2 * (s : ℝ) / T) * (((m * T : ℕ) : ℝ) ^ k / (m : ℝ) ^ q.length) := by
…

Mentions: OAI.TreeEdit.BinaryLower.FiniteTree.Leaf, OAI.TreeEdit.BinaryLower.FiniteTree.State, OAI.TreeEdit.ed, OAI.TreeEdit.BinaryLower.FiniteTree.nodeWord, OAI.TreeEdit.BinaryLower.FiniteTree.leafDecoder