OAI/Probability/FKMaps/Matching.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FKCRT.Inventory.liveAt line 11
2. lemma OAI.FKCRT.Inventory.mem_liveAt line 14
3. lemma OAI.FKCRT.Inventory.liveAt_sorted line 17
4. lemma OAI.FKCRT.Inventory.liveAt_zero line 20
5. lemma OAI.FKCRT.Inventory.liveAt_end line 21
6. lemma OAI.FKCRT.Inventory.liveAt_open line 27
7. lemma OAI.FKCRT.Inventory.liveAt_close line 50
8. lemma OAI.FKCRT.Inventory.liveAt_mate line 74
9. lemma OAI.FKCRT.Inventory.pop_map_erase line 77
10. lemma OAI.FKCRT.Inventory.matching_step_live line 96

    Source documentation

    For noncrossing same-colour arcs, the literal typed stack is the list of live openers in reverse chronological order. No choice of a stack matching is assumed.

    lemma matching_step_live (a : Perm (Fin N)) (ha : Function.Involutive a)
        (hf : ∀ x,a x≠x) (c : Fin N→Bool) (hc : ∀ x,c (a x)=c x)
        (hn : ∀ x y,c x=c y → x < y → y < a x → a x < a y → False) (i : Fin N) :
        stackTypedStep ((liveAt a i.val).map c)
          (if i < a i then .burger (c i) else .order (c i))=
            some ((liveAt a (i.val+1)).map c) := by
    …

    Mentions: OAI.FKCRT.Inventory.stackTypedStep, OAI.FKCRT.Inventory.liveAt

11. lemma OAI.FKCRT.Inventory.liveAt_first_colour line 127
12. lemma OAI.FKCRT.Inventory.head_map_eq_of_first line 142
13. lemma OAI.FKCRT.Inventory.head_eq_iff_greatest line 153
14. theorem OAI.FKCRT.Inventory.flexibleClosing_iff_no_later_cross line 173

    Source documentation

    The source's flexible-mark obstruction, with the strict first-occurrence order and both closing endpoints retained exactly.

    theorem flexibleClosing_iff_no_later_cross (a : Perm (Fin N)) (ha : Function.Involutive a)
        (c : Fin N→Bool) (hc : ∀ x,c (a x)=c x)
        (hn : ∀ x y,c x=c y → x < y → y < a x → a x < a y → False)
        (i : Fin N) (hi : a i < i) :
        flexibleClosing ((liveAt a i.val).map c) (.order (c i)) ↔
          ¬∃ j : Fin N,a i < j ∧ j < i ∧ i < a j := by
    …

    Mentions: OAI.FKCRT.Inventory.flexibleClosing, OAI.FKCRT.Inventory.liveAt

15. lemma OAI.FKCRT.Inventory.flexibleCount_ofFn line 204
16. theorem OAI.FKCRT.Inventory.matching_flexibleCount line 220

    Source documentation

    The complete flexible exponent of the actual identified word is the number of its matched pairs with no later-first crossing edge.

    theorem matching_flexibleCount {N : ℕ} (a : Perm (Fin N)) (ha : Function.Involutive a)
        (hf : ∀ x,a x≠x) (c : Fin N→Bool) (hc : ∀ x,c (a x)=c x)
        (hn : ∀ x y,c x=c y → x < y → y < a x → a x < a y → False) :
        flexibleCount (List.ofFn (fun i => if i<a i then .burger (c i) else .order (c i))) []=
          ∑ i : Fin N,if a i < i ∧ ¬∃ j : Fin N,a i < j ∧ j < i ∧ i < a j then 1 else 0 := by
    …

    Mentions: OAI.FKCRT.Inventory.flexibleCount

17. lemma OAI.FKCRT.Chords.componentDarts_mate line 252
18. def OAI.FKCRT.Chords.opener line 268
19. lemma OAI.FKCRT.Chords.opener_endpoints line 272
20. lemma OAI.FKCRT.Chords.gapIndex_mate line 280
21. def OAI.FKCRT.Chords.cornerDarts line 292
22. lemma OAI.FKCRT.Chords.cornerDarts_mate line 295
23. lemma OAI.FKCRT.Chords.component_card_even line 303
24. def OAI.FKCRT.Inventory.pairWord line 338
25. theorem OAI.FKCRT.Inventory.typedRun_closed_subword line 344

    Source documentation

    Any pair-closed ordered subword of a two-colour noncrossing matching is itself an actual successful inventory word. This applies both to a root crossing component and to each of its corner intervals.

    theorem typedRun_closed_subword (a : Perm (Fin N)) (ha : Function.Involutive a)
        (hf : ∀ x,a x≠x) (c : Fin N→Bool) (hc : ∀ x,c (a x)=c x)
        (hn : ∀ x y,c x=c y → x < y → y < a x → a x < a y → False)
        (l : List (Fin N)) (hl : l.Pairwise (·<·)) (hclosed : ∀ x∈l,a x∈l) :
        stackTypedRun (l.map (pairWord a c)) []=some [] := by
    …

    Mentions: OAI.FKCRT.Inventory.stackTypedRun, OAI.FKCRT.Inventory.pairWord

26. theorem OAI.FKCRT.Inventory.component_and_corners_empty line 378

    Source documentation

    Every root component and every one of its literal corner subwords reduce empty. The conclusion uses the full ordered subword, not independent fresh words postulated at a random cut.

    theorem component_and_corners_empty (a : Perm (Fin N)) (ha : Function.Involutive a)
        (hf : ∀ x,a x≠x) (c : Fin N→Bool) (hc : ∀ x,c (a x)=c x)
        (hn : ∀ x y,c x=c y → x < y → y < a x → a x < a y → False)
        (r : Chords.Opener a) (hr : r.val.val=0) :
        stackTypedRun (((List.finRange N).filter (fun d => decide (d∈Chords.componentDarts a r))).map
          (pairWord a c)) []=some [] ∧
        ∀ k,stackTypedRun (((List.finRange N).filter (fun d => decide (d∈Chords.cornerDarts a r k))).map
          (pairWord a c)) []=some [] := by
    …

    Mentions: OAI.FKCRT.Chords.Opener, OAI.FKCRT.Inventory.stackTypedRun, OAI.FKCRT.Chords.componentDarts, OAI.FKCRT.Inventory.pairWord, OAI.FKCRT.Chords.cornerDarts