OAI/Combinatorics/TwoWayAutomata/Nesting.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.TwoWayComplementation.Diagram.loopClosure_subset_of_corner line 11
2. theorem OAI.TwoWayComplementation.Diagram.nested_forward_loop_absorption line 19

   Source documentation

   Two finite-path rearrangements for absorption under nesting.

   theorem nested_forward_loop_absorption {m : ℕ} (e d : Diagram m) (hd : d ∈ e.corner) :
       e.forward ○ d.loopClosure true ○ d.forward ⊆ d.loopClosure true ○ d.forward ∧
       d.forward ○ d.loopClosure true ○ e.forward ⊆ d.forward ○ d.loopClosure true := by
   …

   Mentions: OAI.TwoWayComplementation.Diagram

3. theorem OAI.TwoWayComplementation.Diagram.nested_through_loop_absorption line 87
4. theorem OAI.TwoWayComplementation.Diagram.nested_through_absorption line 99
5. theorem OAI.TwoWayComplementation.Diagram.nested_recurrence_absorption line 111

   Source documentation

   Mixed recurrent relations are absorbed under nesting.

   theorem nested_recurrence_absorption {m : ℕ} (e d : Diagram m) (hd : d ∈ e.corner)
       (positive : Bool) :
       e.recurrence positive ○ d.recurrence positive ⊆ d.recurrence positive ∧
       d.recurrence positive ○ e.recurrence positive ⊆ d.recurrence positive := by
   …

   Mentions: OAI.TwoWayComplementation.Diagram

6. theorem OAI.TwoWayComplementation.Diagram.corner_forward_factor line 135
7. theorem OAI.TwoWayComplementation.Diagram.corner_through_factor line 156
8. theorem OAI.TwoWayComplementation.Diagram.nested_recurrent_witness line 170

   Source documentation

   A recurrent loop in a nested corner contains two recurrent points of its parent.

   theorem nested_recurrent_witness {m : ℕ} (e d : Diagram m) (he : comp e e = e)
       (hd : d ∈ e.corner) {positive : Bool} {x : Fin m}
       (hxx : (x, x) ∈ d.recurrence positive) :
       ∃ p q, (p, p) ∈ e.recurrence positive ∧ (q, q) ∈ e.recurrence positive ∧
         (x, p) ∈ d.recurrence positive ∧ (p, x) ∈ d.recurrence positive ∧
         (x, q) ∈ d.recurrence positive ∧ (q, x) ∈ d.recurrence positive ∧
         (p, q) ∈ e.surviving d positive := by
   …

   Mentions: OAI.TwoWayComplementation.Diagram, OAI.TwoWayComplementation.Diagram.comp

9. theorem OAI.TwoWayComplementation.Diagram.nested_class_containment line 200

   Source documentation

   A new class contains a surviving old class or two distinct old classes.

   theorem nested_class_containment {m : ℕ} (e d : Diagram m)
       (he : comp e e = e) (hd : comp d d = d) (hde : d ∈ e.corner)
       {c : Bool × Set (Fin m)} (hc : c ∈ d.classes) :
       (∃ C ∈ e.classes, C.1 = c.1 ∧ C.2 ⊆ c.2 ∧ C ∉ e.missing d) ∨
         ∃ C ∈ e.classes, ∃ D ∈ e.classes,
           C ≠ D ∧ C.1 = c.1 ∧ D.1 = c.1 ∧ C.2 ⊆ c.2 ∧ D.2 ⊆ c.2 := by
   …

   Mentions: OAI.TwoWayComplementation.Diagram, OAI.TwoWayComplementation.Diagram.comp

10. theorem OAI.TwoWayComplementation.Diagram.nested_unprotected_loss line 234
11. theorem OAI.TwoWayComplementation.Diagram.nested_chain_bound line 266

    Source documentation

    A common initial missing set pays for all later losses.

    theorem nested_chain_bound {m k : ℕ} (b : ℕ → Diagram m)
        (hidemp : ∀ j ≤ k, comp (b j) (b j) = b j)
        (hnest : ∀ j < k, (b (j + 1), b j) ∈ nesting m)
        (J : Set (Bool × Set (Fin m)))
        (hJ : ∀ j ≤ k, (b 0).missing (b j) ⊆ J) :
        ∑ j ∈ Finset.range k, ((b j).missing (b (j + 1))).ncard ≤ 2 * J.ncard := by
    …

    Mentions: OAI.TwoWayComplementation.Diagram, OAI.TwoWayComplementation.Diagram.comp, OAI.TwoWayComplementation.Diagram.nesting, OAI.TwoWayComplementation.Diagram.missing