OAI/Probability/FKMaps/MapCycles.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.FKCRT.MapCycles.formPerm_cut line 13
2. lemma OAI.FKCRT.MapCycles.swap_mul_formPerm_cut line 30
3. lemma OAI.FKCRT.MapCycles.sameCycle_formPerm_of_mem line 37
4. lemma OAI.FKCRT.MapCycles.pow_eq_on_list line 47
5. lemma OAI.FKCRT.MapCycles.sameCycle_of_list line 57
6. abbrev OAI.FKCRT.MapCycles.Orbits line 63
7. lemma OAI.FKCRT.MapCycles.card_orbits_eq_of_lists line 68

   Source documentation

   A partition into nonempty cyclic lists counts all orbits, including fixed points. The local action condition makes this independent of a chosen representative of the quotient.

   lemma card_orbits_eq_of_lists [Finite α] {β : Type*} [Finite β]
       (p : Perm α) (l : β → List α) (hn : ∀ i, (l i).Nodup)
       (hne : ∀ i, ∃ x, x ∈ l i)
       (hc : ∀ x, ∃! i, x ∈ l i)
       (hp : ∀ i x, x ∈ l i → p x = (l i).formPerm x) :
       Nat.card (Orbits p) = Nat.card β := by
   …

   Mentions: OAI.FKCRT.MapCycles.Orbits

8. def OAI.FKCRT.MapCycles.orbitList line 104

   Source documentation

   Canonical cyclic list, retaining one-element fixed cycles.

   def orbitList [Fintype α] (p : Perm α) (x : α) : List α :=
   …

9. lemma OAI.FKCRT.MapCycles.nodup_orbitList line 107
10. lemma OAI.FKCRT.MapCycles.mem_orbitList line 112
11. lemma OAI.FKCRT.MapCycles.orbitList_action line 121
12. def OAI.FKCRT.MapCycles.splitFamily line 134

    Source documentation

    Splitting one part of a finite list partition into two consecutive, nonempty pieces adds exactly one block, without discarding fixed points.

    def splitFamily {β : Type*} [DecidableEq β] (l : β → List α) (i₀ : β)
        (L R : List α) : ({i : β // i ≠ i₀} ⊕ Bool) → List α
      | Sum.inl i => l i
      | Sum.inr false => L
      | Sum.inr true => R
    
    omit [DecidableEq α] in

13. lemma OAI.FKCRT.MapCycles.splitFamily_partition line 141
14. lemma OAI.FKCRT.MapCycles.card_orbits_cut line 182
15. lemma OAI.FKCRT.MapCycles.orbitList_eq_cons line 239
16. theorem OAI.FKCRT.MapCycles.card_orbits_swap_of_sameCycle line 255

    Source documentation

    Swapping two distinct members of one orbit cuts that orbit into two. In particular one-element vertex/face cycles are not lost in the count.

    theorem card_orbits_swap_of_sameCycle [Fintype α] (p : Perm α) {a b : α}
        (hab : a ≠ b) (hs : p.SameCycle a b) :
        Nat.card (Orbits (swap a b * p)) = Nat.card (Orbits p) + 1 := by
    …

    Mentions: OAI.FKCRT.MapCycles.Orbits

17. lemma OAI.FKCRT.MapCycles.sameCycle_swap_of_not_sameCycle line 288
18. theorem OAI.FKCRT.MapCycles.card_orbits_swap_of_not_sameCycle line 319

    Source documentation

    Swapping members of distinct orbits joins precisely those two orbits.

    theorem card_orbits_swap_of_not_sameCycle [Fintype α] (p : Perm α) {a b : α}
        (hs : ¬ p.SameCycle a b) :
        Nat.card (Orbits (swap a b * p)) + 1 = Nat.card (Orbits p) := by
    …

    Mentions: OAI.FKCRT.MapCycles.Orbits

19. theorem OAI.FKCRT.MapCycles.card_orbits_swap_le line 328

    Source documentation

    Each edge transposition changes Euler's orbit count by exactly one.

    theorem card_orbits_swap_le [Fintype α] (p : Perm α) (a b : α) :
        Nat.card (Orbits (swap a b * p)) ≤ Nat.card (Orbits p) + 1 := by
    …

    Mentions: OAI.FKCRT.MapCycles.Orbits

20. lemma OAI.FKCRT.MapCycles.sameCycle_mono line 351
21. lemma OAI.FKCRT.MapCycles.sameCycle_le_vertexJoin line 363

    Source documentation

    Swapping the outputs at two distinct rotation cycles preserves every old vertex incidence and merges the indicated two vertices.

    lemma sameCycle_le_vertexJoin (p : Perm α) {a b : α} (h : ¬p.SameCycle a b)
        {x y : α} (hxy : p.SameCycle x y) : (swap a b*p).SameCycle x y := by
    …

22. def OAI.FKCRT.MapCycles.JoinRel line 380
23. lemma OAI.FKCRT.MapCycles.JoinRel.refl line 385
24. lemma OAI.FKCRT.MapCycles.JoinRel.symm line 389
25. lemma OAI.FKCRT.MapCycles.JoinRel.trans line 395
26. lemma OAI.FKCRT.MapCycles.JoinRel.step line 406
27. theorem OAI.FKCRT.MapCycles.sameCycle_vertexJoin_iff line 419

    Source documentation

    Exact vertex equivalence after one-vertex gluing. In particular no additional vertices are identified, including fixed points and loop blocks.

    theorem sameCycle_vertexJoin_iff (p : Perm α) {a b : α} (h : ¬p.SameCycle a b) (x y : α) :
        (swap a b*p).SameCycle x y ↔ JoinRel p a b x y := by
    …

    Mentions: OAI.FKCRT.MapCycles.JoinRel

28. lemma OAI.FKCRT.MapCycles.sameCycle_partition line 449
29. lemma OAI.FKCRT.MapCycles.not_sameCycle_partition line 458
30. theorem OAI.FKCRT.MapCycles.vertexJoin_inside_iff line 464

    Source documentation

    The inclusion of either block's vertices remains injective under the actual vertex-rotation cut/join.

    theorem vertexJoin_inside_iff {p : Perm α} {S : Set α}
        (hp : ∀ d,p d∈S ↔ d∈S) {a b x y : α} (ha : a∈S) (hb : b∉S)
        (hx : x∈S) (hy : y∈S) : (swap a b*p).SameCycle x y ↔ p.SameCycle x y := by
    …

31. theorem OAI.FKCRT.MapCycles.vertexJoin_outside_iff line 477
32. theorem OAI.FKCRT.MapCycles.vertexJoin_cross_iff line 486

    Source documentation

    A vertex in one block coincides with a vertex in the other block if and only if both are their respective attachment poles.

    theorem vertexJoin_cross_iff {p : Perm α} {S : Set α}
        (hp : ∀ d,p d∈S ↔ d∈S) {a b x y : α} (ha : a∈S) (hb : b∉S)
        (hx : x∈S) (hy : y∉S) : (swap a b*p).SameCycle x y ↔ p.SameCycle x a ∧ p.SameCycle y b := by
    …

33. lemma OAI.FKCRT.MapCycles.formPerm_other_mem_iff line 501
34. theorem OAI.FKCRT.MapCycles.contour_vertex_join line 517

    Source documentation

    The literal combined contour rotation is a one-vertex join of the separate rotations. The flip permutation can be the actual first-colour matching; only its proved locality is required.

    theorem contour_vertex_join (a b : α) (L R : List α)
        (hn : (a::(L++b::R)).Nodup) (e : Perm α)
        (he : ∀ x,e x∈a::L ↔ x∈a::L) :
        let p := (a::L).formPerm*(b::R).formPerm*e
    …