Locally good patterns

The two directions of the support condition of the polytopes:

• goodP_map: the pattern of a good set of words (in particular of a subgroup) on a set of words closed under shortening is locally good;
• extW_not_mem_badSet: the set of words of a locally good pattern avoids every bad set whose words it contains (Lemma I:941 (2): a limit of such patterns is carried by Good s).

def MIPRE.Tailored.Sofic.Measure.badWords : Unit ⊕ SubgroupTestValue.Word × SubgroupTestValue.Word × ℕ × Bool ⊕ SubgroupTestValue.Word × SubgroupTestValue.Word ⊕ SubgroupTestValue.Word × SubgroupTestValue.Word × ℕ × Bool → List SubgroupTestValue.Word

The words of a bad set.

Equations

• MIPRE.Tailored.Sofic.Measure.badWords (Sum.inl val) = [[]]
• MIPRE.Tailored.Sofic.Measure.badWords (Sum.inr (Sum.inl (u₁, u₂, i, c))) = [u₁ ++ (i, c) :: (i, !c) :: u₂]
• MIPRE.Tailored.Sofic.Measure.badWords (Sum.inr (Sum.inr (Sum.inl (u, v)))) = [u, v, u ++ MIPRE.Tailored.Sofic.invW v]
• MIPRE.Tailored.Sofic.Measure.badWords (Sum.inr (Sum.inr (Sum.inr (u₁, u₂, i, c)))) = [u₁ ++ (i, c) :: u₂]

theorem MIPRE.Tailored.Sofic.Measure.mem_wordsUpTo_of_sublist {L n : ℕ} {u v : SubgroupTestValue.Word} (hu : u ∈ wordsUpTo L n) (h : List.Sublist v u) : v ∈ wordsUpTo L n

Deleting letters keeps a word among the words up to a length.

theorem MIPRE.Tailored.Sofic.Measure.sublist_take_append_drop (u : SubgroupTestValue.Word) (j k : ℕ) (hjk : j ≤ k) : (List.take j u ++ List.drop k u).Sublist u

theorem MIPRE.Tailored.Sofic.Measure.eq_of_cancel2 {u : SubgroupTestValue.Word} {j : ℕ} (h : cancel2 u j = true) : u = List.take j u ++ List.getD u j (0, false) :: ((List.getD u j (0, false)).1, !(List.getD u j (0, false)).2) :: List.drop (j + 2) u

The decomposition of a word at a cancelling pair.

theorem MIPRE.Tailored.Sofic.Measure.eq_of_drop1 {s : ℕ} {u : SubgroupTestValue.Word} {j : ℕ} (h : drop1 s u j = true) : u = List.take j u ++ List.getD u j (0, false) :: List.drop (j + 1) u ∧ s ≤ (List.getD u j (0, false)).1

theorem MIPRE.Tailored.Sofic.Measure.goodP_map {s L n : ℕ} {A : WordSpace} (hA : A ∈ Good s) : goodP s (wordsUpTo L n) (List.map A (wordsUpTo L n)) = true

The pattern of a good set of words is locally good.

theorem MIPRE.Tailored.Sofic.Measure.cancel2_append (u₁ u₂ : SubgroupTestValue.Word) (i : ℕ) (c : Bool) : cancel2 (u₁ ++ (i, c) :: (i, !c) :: u₂) (List.length u₁) = true

theorem MIPRE.Tailored.Sofic.Measure.drop1_append {s : ℕ} (u₁ u₂ : SubgroupTestValue.Word) {i : ℕ} (c : Bool) (hi : s ≤ i) : drop1 s (u₁ ++ (i, c) :: u₂) (List.length u₁) = true

theorem MIPRE.Tailored.Sofic.Measure.extW_not_mem_badSet {s L n : ℕ} {p : List Bool} (hp : goodP s (wordsUpTo L n) p = true) (b : Unit ⊕ SubgroupTestValue.Word × SubgroupTestValue.Word × ℕ × Bool ⊕ SubgroupTestValue.Word × SubgroupTestValue.Word ⊕ SubgroupTestValue.Word × SubgroupTestValue.Word × ℕ × Bool) (hb : ∀ w ∈ badWords b, w ∈ wordsUpTo L n) : extW (wordsUpTo L n) p ∉ badSet s b

A locally good pattern avoids the bad sets within its words.