Graph.Markov­Equiv.Covered­Reversal

theorem flipEdge_sameImmoralities {a b : V} (hcov : G.IsCoveredEdge a b) : SameImmoralities G (flipEdge hcov) := by have hU : ∀ x y, G.UAdj x y ↔ (flipEdge hcov).UAdj x y := flipEdge_sameSkeleton hcov intro p q r constructor · rintro ⟨hpq, hrq, hnadj, hpr⟩ have hpq' : (flipEdge hcov).edge p q := by rw [flipEdge_edge]; left; refine ⟨hpq, ?_⟩ rintro ⟨hpa, hqb⟩ -- collider `a → b ← r`: covered forces `r → a`, contradicting non-adjacency rw [hpa] at hpr hnadj; rw [hqb] at hrq exact hnadj (inr ((hcov.2 r (Ne.symm hpr)).mpr hrq)) have hrq' : (flipEdge hcov).edge r q := by rw [flipEdge_edge]; left; refine ⟨hrq, ?_⟩ rintro ⟨hra, hqb⟩ -- collider `p → b ← a`: covered forces `p → a`, contradicting non-adjacency rw [hra] at hpr hnadj; rw [hqb] at hpq exact hnadj (inl ((hcov.2 p hpr).mpr hpq)) exact ⟨hpq', hrq', fun h => hnadj ((hU p r).mpr h), hpr⟩ · rintro ⟨hpq, hrq, hnadj, hpr⟩ rw [flipEdge_edge] at hpq hrq have hnadjG : ¬ G.UAdj p r := fun h => hnadj ((hU p r).mp h) have hpqG : G.edge p q := by rcases hpq with ⟨h, _⟩ | ⟨hpb, hqa⟩ · exact h · exfalso rcases hrq with ⟨hra, _⟩ | ⟨hrb, _⟩ · rw [hqa] at hra have hrne : r ≠ a := fun heq => G.irrefl _ (heq ▸ hra) apply hnadjG; rw [hpb]; exact inr ((hcov.2 r hrne).mp hra) · exact hpr (hpb.trans hrb.symm) have hrqG : G.edge r q := by rcases hrq with ⟨h, _⟩ | ⟨hrb, hqa⟩ · exact h · exfalso rcases hpq with ⟨hpa, _⟩ | ⟨hpb, _⟩ · rw [hqa] at hpa have hpne : p ≠ a := fun heq => G.irrefl _ (heq ▸ hpa) apply hnadjG; rw [hrb]; exact inl ((hcov.2 p hpne).mp hpa) · exact hpr (hpb.trans hrb.symm) exact ⟨hpqG, hrqG, hnadjG, hpr⟩

theorem isActiveWalk_flip_of_not_mem {a b : V} (hcov : G.IsCoveredEdge a b) {Z : Finset V} {p : List V} (hact : G.IsActiveWalk Z p) (hna : a ∉ p) : (flipEdge hcov).IsActiveWalk Z p := by obtain ⟨hadj, htri⟩ := hact refine ⟨fun i hi => ?_, fun i hi => ?_⟩ · exact (flipEdge_sameSkeleton hcov _ _).mp (hadj i hi) · let l := p.get ⟨i, by omega⟩ let m := p.get ⟨i + 1, by omega⟩ let r := p.get ⟨i + 2, hi⟩ have hla : l ≠ a := by intro h apply hna rw [← h] exact List.get_mem p ⟨i, by omega⟩ have hma : m ≠ a := by intro h apply hna rw [← h] exact List.get_mem p ⟨i + 1, by omega⟩ have hra : r ≠ a := by intro h apply hna rw [← h] exact List.get_mem p ⟨i + 2, hi⟩ have hciff : (flipEdge hcov).IsCollider l m r ↔ G.IsCollider l m r := flipEdge_isCollider_iff_of_ne_a hcov hla hma hra have hval := htri i hi change (if G.IsCollider l m r then m ∈ G.bbZAncestors Z else m ∉ Z) at hval change (if (flipEdge hcov).IsCollider l m r then m ∈ (flipEdge hcov).bbZAncestors Z else m ∉ Z) by_cases hC : G.IsCollider l m r · rw [if_pos ((hciff).mpr hC)] exact bbZAncestors_flip_of_ne hcov Z hma (by rwa [if_pos hC] at hval) · have hCF : ¬ (flipEdge hcov).IsCollider l m r := fun h => hC ((hciff).mp h) rw [if_neg hCF] rwa [if_neg hC] at hval

theorem markovEquiv_flipEdge {a b : V} (hcov : G.IsCoveredEdge a b) : MarkovEquiv G (flipEdge hcov) := by intro X Y Z by_cases hXY : Disjoint X Y · by_cases hXZ : Disjoint X Z · by_cases hYZ : Disjoint Y Z · have hAP : G.HasActiveWalk X Y Z ↔ (flipEdge hcov).HasActiveWalk X Y Z := by constructor · exact hasActiveWalk_flipEdge_of_isCoveredEdge hcov X Y Z hXY · intro hp have hp₂ : (flipEdge (flipEdge_isCoveredEdge_back hcov)).HasActiveWalk X Y Z := @hasActiveWalk_flipEdge_of_isCoveredEdge V _ _ (flipEdge hcov) b a (flipEdge_isCoveredEdge_back hcov) X Y Z hXY hp exact (hasActiveWalk_edge_congr (flipEdge_flipEdge_edge hcov) X Y Z).mp hp₂ apply not_iff_not.mp calc ¬ G.dSep X Y Z ↔ G.HasActiveWalk X Y Z := not_dSep_iff_hasActiveWalk G X Y Z hXY hXZ hYZ _ ↔ (flipEdge hcov).HasActiveWalk X Y Z := hAP _ ↔ ¬ (flipEdge hcov).dSep X Y Z := (not_dSep_iff_hasActiveWalk (flipEdge hcov) X Y Z hXY hXZ hYZ).symm · exact iff_of_false (fun h => hYZ h.2.2.1) (fun h => hYZ h.2.2.1) · exact iff_of_false (fun h => hXZ h.2.1) (fun h => hXZ h.2.1) · exact iff_of_false (fun h => hXY h.1) (fun h => hXY h.1)

theorem isActiveWalk_swapPath_of_no_obstruct {a b : V} (hcov : G.IsCoveredEdge a b) {Z : Finset V} {p : List V} (hact : G.IsActiveWalk Z p) (hfork : ∀ (j : ℕ) (hj : j + 2 < p.length), ¬ G.FlipObstruct a b (p.get ⟨j, by omega⟩) (p.get ⟨j + 1, by omega⟩) (p.get ⟨j + 2, hj⟩)) : (flipEdge hcov).IsActiveWalk Z (swapPath hcov Z p) := by obtain ⟨hadj, htri⟩ := hact constructor · -- adjacency intro i hi have hi1 : i + 1 < p.length := by simpa using hi have hi0 : i < p.length := by omega have hG : G.UAdj (p.get ⟨i, hi0⟩) (p.get ⟨i + 1, hi1⟩) := hadj i (by simpa using hi) rcases swapPath_get_eq hcov Z p i (by omega) hi0 with hvi | ⟨hvi, hai, _, _, hcoli, _⟩ · rcases swapPath_get_eq hcov Z p (i + 1) (by omega) hi1 with hvi1 | ⟨hvi1, hai1, _, _, hcol1, _⟩ · rw [hvi, hvi1]; exact (flipEdge_sameSkeleton hcov _ _).mp hG · -- i+1 swapped: its left collider arm gives `p i → a`, covered ⟹ `p i → b` rw [hvi, hvi1] have harm : G.edge (p.get ⟨i, hi0⟩) a := by have h := hcol1.1 simp only [Nat.add_sub_cancel] at h rw [hai1] at h; exact h have hne : p.get ⟨i, hi0⟩ ≠ a := fun h => G.irrefl a (h ▸ harm) have hb : G.edge (p.get ⟨i, hi0⟩) b := (hcov.2 _ hne).mp harm exact inl ((flipEdge_edge_iff_of_ne_a hcov hne hcov.ne.symm).mpr hb) · -- i swapped: its right collider arm gives `p (i+1) → a`, covered ⟹ `p (i+1) → b` have harm : G.edge (p.get ⟨i + 1, hi1⟩) a := by have h := hcoli.2; rw [hai] at h; exact h have hne1 : p.get ⟨i + 1, hi1⟩ ≠ a := fun h => G.irrefl a (h ▸ harm) have hb : G.edge (p.get ⟨i + 1, hi1⟩) b := (hcov.2 _ hne1).mp harm rcases swapPath_get_eq hcov Z p (i + 1) (by omega) hi1 with hvi1 | ⟨_, hai1, _, _, _⟩ · rw [hvi, hvi1] exact inr ((flipEdge_edge_iff_of_ne_a hcov hne1 hcov.ne.symm).mpr hb) · exact absurd hai1 hne1 · -- collider / activation conditions intro j hj have hjl : j + 2 < p.length := by simpa using hj have hj0 : j < p.length := by omega have hj1 : j + 1 < p.length := by omega have hjtri := htri j (by simpa using hj) have hob := hfork j (by simpa using hj) rcases swapPath_get_eq hcov Z p (j + 1) (by omega) hj1 with hmid | ⟨hmidb, hmida, _, _, hmcol, hmanc⟩ · -- middle kept by_cases hmida : p.get ⟨j + 1, hj1⟩ = a · -- A1: middle = a (kept). Under `hfork`, `a` is a flip-collider iff it is a G-collider, -- because a `b` neighbour of `a` would otherwise be a flip-obstructing triple. have hjne : p.get ⟨j, hj0⟩ ≠ a := by intro h have hu := hadj j (by omega); rw [h, hmida] at hu rcases hu with he | he <;> exact G.irrefl a he have hj2ne : p.get ⟨j + 2, hjl⟩ ≠ a := by intro h have hu := hadj (j + 1) (by omega); rw [hmida, h] at hu rcases hu with he | he <;> exact G.irrefl a he rcases swapPath_get_eq hcov Z p j (by omega) hj0 with hvj | ⟨_, haj, _⟩ on_goal 2 => exact absurd haj hjne rcases swapPath_get_eq hcov Z p (j + 2) (by omega) hjl with hvj2 | ⟨_, haj2, _⟩ on_goal 2 => exact absurd haj2 hj2ne have hcoll_iff : (flipEdge hcov).IsCollider (p.get ⟨j, hj0⟩) a (p.get ⟨j + 2, hjl⟩) ↔ G.IsCollider (p.get ⟨j, hj0⟩) a (p.get ⟨j + 2, hjl⟩) := by constructor · rintro ⟨hL, hR⟩ rw [flipEdge_edge] at hL hR have hLa : G.edge (p.get ⟨j, hj0⟩) a := by rcases hL with ⟨he, _⟩ | ⟨hlb, _⟩ · exact he · exact (hob (inl ⟨hmida, hlb, hR.elim (fun h => inl h.1) (fun h => inr h.1)⟩)).elim have hRa : G.edge (p.get ⟨j + 2, hjl⟩) a := by rcases hR with ⟨he, _⟩ | ⟨hrb, _⟩ · exact he · exact (hob (inr (inl ⟨hmida, hrb, inl hLa⟩))).elim exact ⟨hLa, hRa⟩ · rintro ⟨hL, hR⟩ exact ⟨by rw [flipEdge_edge]; exact inl ⟨hL, fun h => hjne h.1⟩, by rw [flipEdge_edge]; exact inl ⟨hR, fun h => hj2ne h.1⟩⟩ simp only [hvj, hvj2, hmid, hmida] by_cases hC : G.IsCollider (p.get ⟨j, hj0⟩) a (p.get ⟨j + 2, hjl⟩) · rw [if_pos (hcoll_iff.mpr hC)] by_contra hanc have hb : (swapPath hcov Z p).get ⟨j + 1, by simpa using hj1⟩ = b := swapPath_get_b_of hcov Z p (j + 1) (by simpa using hj1) hj1 (by omega) (by omega) hmida hanc (by simpa only [Nat.add_sub_cancel, hmida] using hC) rw [hmid, hmida] at hb exact hcov.ne hb · rw [if_neg (fun h => hC (hcoll_iff.mp h))] have hcG : ¬ G.IsCollider (p.get ⟨j, hj0⟩) (p.get ⟨j + 1, hj1⟩) (p.get ⟨j + 2, hjl⟩) := by rw [hmida]; exact hC have ht := hjtri; rw [if_neg hcG] at ht; rwa [hmida] at ht · -- A2: middle m = p[j+1] ≠ a (kept) rw [hmid] -- `m ∉ Z` from the original triple, used in every non-collider branch have hmnotZ_of : ¬ G.IsCollider (p.get ⟨j, hj0⟩) (p.get ⟨j + 1, hj1⟩) (p.get ⟨j + 2, hjl⟩) → p.get ⟨j + 1, hj1⟩ ∉ Z := fun hc => by have ht := hjtri; rw [if_neg hc] at ht; exact ht -- helper: a swapped side gives `m → a`, hence the side has no flip-edge into `m`, -- and the original triple is not a collider, so `m ∉ Z`. have swapped_side : G.edge (p.get ⟨j + 1, hj1⟩) a → ¬ (flipEdge hcov).edge b (p.get ⟨j + 1, hj1⟩) := by intro hma hbm have hmb : p.get ⟨j + 1, hj1⟩ ≠ b := by intro h; rw [h] at hma; exact G.asymm hcov.1 hma have hmne : p.get ⟨j + 1, hj1⟩ ≠ a := fun h => G.irrefl a (h ▸ hma) exact absurd ((flipEdge_edge_into_iff hcov hmida hmb b).mp hbm) (G.asymm ((hcov.2 (p.get ⟨j + 1, hj1⟩) hmne).mp hma)) rcases swapPath_get_eq hcov Z p j (by omega) hj0 with hvj | ⟨hvjb, hvja, _, _, hvjcol, _⟩ · rcases swapPath_get_eq hcov Z p (j + 2) (by omega) hjl with hvj2 | ⟨hvj2b, hvj2a, _, _, hvj2col, _⟩ · -- both sides kept: collider status and activation transfer by_cases hmb : p.get ⟨j + 1, hj1⟩ = b · -- middle is `b`. Under `hfork`, flip-collider ↔ G-collider at `b`: an `a` -- neighbour would otherwise destroy the collider (a flip-obstructing triple). have hbiff : (flipEdge hcov).IsCollider (p.get ⟨j, hj0⟩) (p.get ⟨j + 1, hj1⟩) (p.get ⟨j + 2, hjl⟩) ↔ G.IsCollider (p.get ⟨j, hj0⟩) (p.get ⟨j + 1, hj1⟩) (p.get ⟨j + 2, hjl⟩) := by constructor · rintro ⟨hL, hR⟩ rw [flipEdge_edge, hmb] at hL hR refine ⟨?_, ?_⟩ · rcases hL with ⟨he, _⟩ | ⟨_, hba⟩ · rw [hmb]; exact he · exact absurd hba.symm hcov.ne · rcases hR with ⟨he, _⟩ | ⟨_, hba⟩ · rw [hmb]; exact he · exact absurd hba.symm hcov.ne · rintro ⟨hL, hR⟩ rw [hmb] at hL hR have hjna : p.get ⟨j, hj0⟩ ≠ a := fun h => hob (inr (inr (inl ⟨hmb, h, hR⟩))) have hj2na : p.get ⟨j + 2, hjl⟩ ≠ a := fun h => hob (inr (inr (inr ⟨hmb, h, hL⟩))) exact ⟨by rw [flipEdge_edge, hmb]; exact inl ⟨hL, fun h => hjna h.1⟩, by rw [flipEdge_edge, hmb]; exact inl ⟨hR, fun h => hj2na h.1⟩⟩ rw [hvj, hvj2] by_cases hC : G.IsCollider (p.get ⟨j, hj0⟩) (p.get ⟨j + 1, hj1⟩) (p.get ⟨j + 2, hjl⟩) · rw [if_pos (hbiff.mpr hC)] have hmG : p.get ⟨j + 1, hj1⟩ ∈ G.bbZAncestors Z := by have ht := hjtri; rwa [if_pos hC] at ht rw [hmb]; exact bbZAncestors_flip_of_b hcov Z (by rw [← hmb]; exact hmG) · rw [if_neg (fun h => hC (hbiff.mp h))] exact hmnotZ_of hC · -- middle ∉ {a, b}: edges into it are flip-invariant have hiffL := flipEdge_edge_into_iff hcov hmida hmb (p.get ⟨j, hj0⟩) have hiffR := flipEdge_edge_into_iff hcov hmida hmb (p.get ⟨j + 2, hjl⟩) rw [hvj, hvj2] by_cases hC : G.IsCollider (p.get ⟨j, hj0⟩) (p.get ⟨j + 1, hj1⟩) (p.get ⟨j + 2, hjl⟩) · rw [if_pos ⟨hiffL.mpr hC.1, hiffR.mpr hC.2⟩] have hmG : p.get ⟨j + 1, hj1⟩ ∈ G.bbZAncestors Z := by have ht := hjtri; rwa [if_pos hC] at ht exact bbZAncestors_flip_of_ne hcov Z hmida hmG · rw [if_neg (fun h => hC ⟨hiffL.mp h.1, hiffR.mp h.2⟩)] exact hmnotZ_of hC · -- j+2 swapped: p[j+2]=a, collider at j+2 gives m → a have hma : G.edge (p.get ⟨j + 1, hj1⟩) a := by have h := hvj2col.1; rw [hvj2a] at h; exact h have hGc : ¬ G.IsCollider (p.get ⟨j, hj0⟩) (p.get ⟨j + 1, hj1⟩) (p.get ⟨j + 2, hjl⟩) := fun h => G.asymm hma (hvj2a ▸ h.2) rw [hvj2b, if_neg (fun h => swapped_side hma h.2)] exact hmnotZ_of hGc · -- j swapped: p[j]=a, collider at j gives m → a have hma : G.edge (p.get ⟨j + 1, hj1⟩) a := by have h := hvjcol.2; rw [hvja] at h; exact h have hGc : ¬ G.IsCollider (p.get ⟨j, hj0⟩) (p.get ⟨j + 1, hj1⟩) (p.get ⟨j + 2, hjl⟩) := fun h => G.asymm hma (hvja ▸ h.1) rw [hvjb, if_neg (fun h => swapped_side hma h.1)] exact hmnotZ_of hGc · -- middle swapped to b: p[j+1]=a, G-collider at j+1, a ∉ bbZAncestors_flip have harmL : G.edge (p.get ⟨j, hj0⟩) a := by have h := hmcol.1; simp only [Nat.add_sub_cancel] at h; rw [hmida] at h; exact h have harmR : G.edge (p.get ⟨j + 2, hjl⟩) a := by have h := hmcol.2; rw [hmida] at h; exact h have hjne : p.get ⟨j, hj0⟩ ≠ a := fun h => G.irrefl a (h ▸ harmL) have hj2ne : p.get ⟨j + 2, hjl⟩ ≠ a := fun h => G.irrefl a (h ▸ harmR) have hbL : G.edge (p.get ⟨j, hj0⟩) b := (hcov.2 _ hjne).mp harmL have hbR : G.edge (p.get ⟨j + 2, hjl⟩) b := (hcov.2 _ hj2ne).mp harmR rcases swapPath_get_eq hcov Z p j (by omega) hj0 with hvj | ⟨_, haj, _⟩ · rcases swapPath_get_eq hcov Z p (j + 2) (by omega) hjl with hvj2 | ⟨_, haj2, _⟩ · have hcolF : (flipEdge hcov).IsCollider (p.get ⟨j, hj0⟩) b (p.get ⟨j + 2, hjl⟩) := ⟨(flipEdge_edge_iff_of_ne_a hcov hjne hcov.ne.symm).mpr hbL, (flipEdge_edge_iff_of_ne_a hcov hj2ne hcov.ne.symm).mpr hbR⟩ have haG : a ∈ G.bbZAncestors Z := by have hc : G.IsCollider (p.get ⟨j, hj0⟩) (p.get ⟨j + 1, hj1⟩) (p.get ⟨j + 2, hjl⟩) := by rw [hmida]; exact ⟨harmL, harmR⟩ have ht := hjtri; rw [if_pos hc] at ht; rwa [hmida] at ht simp only [hmidb, hvj, hvj2] rw [if_pos hcolF] exact bbZAncestors_flip_of_lost hcov Z haG hmanc · exact absurd haj2 hj2ne · exact absurd haj hjne