Graph.DSep.Ordered­Local­SG

This interface exports the ordered-local derivation rules, the active-walk surgery and joining lemmas used by the peel induction, and the theorem that d-separation yields an ordered-local semi-graphoid derivation.

Defs 3 core · 4 supporting This file defines DAG.OrderedLocalSG, the triples generated from a DAG's ordered-local basis by symmetry, decomposition, weak union, and contraction. ★ OrderedLocalSG★ subset_random

Ordered-local semi-graphoid definitions

This file defines DAG.OrderedLocalSG, the triples generated from a DAG's ordered-local basis by symmetry, decomposition, weak union, and contraction. It also provides the ambient-set containment theorem and the ancestral-cardinality and topological-height measures used by the later peel induction.

inductive OrderedLocalSG reviewed
Causalean.Graph.DAG

For a finite vertex population with decidable equality, a directed acyclic graph on that population, and an ambient set of random vertices, the ordered-local semi-graphoid closure contains precisely the triples of finite vertex sets generated by the empty-set rule, the ordered-local basis, symmetry, decomposition, weak union, and contraction.

Definition (Lean source)
parameters
V :
Type u_1
shared
G :
DAG V
R :
Finset V
inductive
OrderedLocalSG G R :
Finset V → Finset V → Finset V → Prop
constructors
nil :
(Y Z : Finset V) (hY : Y ⊆ R) (hZ : Z ⊆ R) : OrderedLocalSG G R ∅ Y Z
basis :
(v : V) (hv : v ∈ R) (P : Finset V) (hP : P ⊆ R) (hND : P ⊆ G.nonDescendants v) (hPa : G.parents v ∩ R ⊆ P) : OrderedLocalSG G R {v} (P \ (G.parents v ∩ R)) (G.parents v ∩ R)
symm :
{X Y Z : Finset V} : OrderedLocalSG G R X Y Z → OrderedLocalSG G R Y X Z
decomp :
{X Y W Z : Finset V} : OrderedLocalSG G R X (Y ∪ W) Z → OrderedLocalSG G R X Y Z
weakUnion :
{X Y W Z : Finset V} : OrderedLocalSG G R X (Y ∪ W) Z → OrderedLocalSG G R X Y (Z ∪ W)
contract :
{X Y W Z : Finset V} : OrderedLocalSG G R X Y (Z ∪ W) → OrderedLocalSG G R X W Z → OrderedLocalSG G R X (Y ∪ W) Z
Causalean.Graph.DAG.OrderedLocalSG · Causalean/Graph/DSep/OrderedLocalSG/Defs.lean:32 · uses DAG
theorem subset_random reviewed
Causalean.Graph.DAG.OrderedLocalSG

For a finite directed acyclic graph, an ambient random set, and three query sets, if the query triple is derivable from the ordered-local semi-graphoid rules, then each query set is contained in the ambient random set.

Formal statement
hypotheses
V :
Type u_1
DAG V
Finset V
shared
h :
G.OrderedLocalSG R X Y Z
conclusion
conclusion 1
X ⊆ R
conclusion 2
Y ⊆ R
conclusion 3
Z ⊆ R
Proof (Lean source)
theorem OrderedLocalSG.subset_random {G : DAG V} {R X Y Z : Finset V} (h : G.OrderedLocalSG R X Y Z) : X ⊆ R ∧ Y ⊆ R ∧ Z ⊆ R := by induction h with | nil Y Z hY hZ => exact ⟨Finset.empty_subset _, hY, hZ⟩ | basis v hv P hP hND hPa => refine ⟨Finset.singleton_subset_iff.mpr hv, ?_, Finset.inter_subset_right⟩ exact (sdiff_subset).trans hP | symm _ ih => exact ⟨ih.2.1, ih.1, ih.2.2⟩ | decomp _ ih => exact ⟨ih.1, (subset_union_left).trans ih.2.1, ih.2.2⟩ | weakUnion _ ih => refine ⟨ih.1, (subset_union_left).trans ih.2.1, ?_⟩ exact union_subset ih.2.2 ((subset_union_right).trans ih.2.1) | contract _ _ ih1 ih2 => exact ⟨ih1.1, union_subset ih1.2.1 ih2.2.1, ih2.2.2⟩
Causalean.Graph.DAG.OrderedLocalSG.subset_random · Causalean/Graph/DSep/OrderedLocalSG/Defs.lean:63 · uses DAG , OrderedLocalSG
def peelMeasure reviewed
Causalean.Graph.DAG

For a finite directed acyclic graph and two endpoint sets plus random and fixed conditioning sets, the lexicographic peel measure pairs the size of the query's ancestral closure with the topological height of its random conditioning set.

Definition (Lean source)
parameters
V :
Type u_1
shared
G :
DAG V
X Y Zr Zf :
Finset V
def
peelMeasure G X Y Zr Zf :
ℕ × ℕ
given by
((G.ancestralSet (X ∪ Y ∪ Zr ∪ Zf)).card, Zr.sup (fun v => G.topoOrder v + 1))
Causalean.Graph.DAG.peelMeasure · Causalean/Graph/DSep/OrderedLocalSG/Defs.lean:90 · uses DAG
4 supporting declarations (lemmas, instances)
  • topoMax_mem_seed theorem — In a finite directed acyclic graph, a vertex in a seed set's ancestral closure that maximizes topological order there belongs to the seed set itself.
    hypotheses
    V :
    Type u_1
    shared
    G :
    DAG V
    shared
    Q :
    Finset V
    n :
    V
    hn :
    n ∈ G.ancestralSet Q
    hmax :
    ∀ m ∈ G.ancestralSet Q, G.topoOrder m ≤ G.topoOrder n
    conclusion
    n ∈ Q
    Proof (Lean source)
    theorem topoMax_mem_seed {Q : Finset V} {n : V} (hn : n ∈ G.ancestralSet Q) (hmax : ∀ m ∈ G.ancestralSet Q, G.topoOrder m ≤ G.topoOrder n) : n ∈ Q := by simp only [ancestralSet, mem_union, ancestorsSet, mem_filter, Finset.mem_univ, true_and] at hn rcases hn with hnQ | ⟨w, hwQ, haw⟩ · exact hnQ · -- `n` is a strict ancestor of `w ∈ Q`; but `w ∈ ancestralSet Q`, so -- `topoOrder w ≤ topoOrder n < topoOrder w`, contradiction. exfalso have hwAnc : w ∈ G.ancestralSet Q := G.subset_ancestralSet Q (by exact hwQ) have h1 : G.topoOrder w ≤ G.topoOrder n := hmax w hwAnc have h2 : G.topoOrder n < G.topoOrder w := G.isAncestor_topoOrder_lt haw omega
    Causalean.Graph.DAG.topoMax_mem_seed · Causalean/Graph/DSep/OrderedLocalSG/Defs.lean:105
  • ancestralSet_subset_of_subset_ancestralSet theorem — In a finite directed acyclic graph, if one set lies inside another set's ancestral closure, then the first set's ancestral closure remains inside the second set's ancestral closure.
    hypotheses
    V :
    Type u_1
    shared
    G :
    DAG V
    shared
    Q Q' :
    Finset V
    h :
    Q' ⊆ G.ancestralSet Q
    conclusion
    G.ancestralSet Q' ⊆ G.ancestralSet Q
    Proof (Lean source)
    theorem ancestralSet_subset_of_subset_ancestralSet {Q Q' : Finset V} (h : Q' ⊆ G.ancestralSet Q) : G.ancestralSet Q' ⊆ G.ancestralSet Q := by intro u hu simp only [ancestralSet, mem_union, ancestorsSet, mem_filter, Finset.mem_univ, true_and] at hu ⊢ rcases hu with huQ' | ⟨q', hq'Q', haq'⟩ · have := h huQ' simpa only [ancestralSet, mem_union, ancestorsSet, mem_filter, Finset.mem_univ, true_and] using this · have hq' := h hq'Q' simp only [ancestralSet, mem_union, ancestorsSet, mem_filter, Finset.mem_univ, true_and] at hq' rcases hq' with hq'Q | ⟨q, hqQ, haq'q⟩ · exact inr ⟨q', hq'Q, haq'⟩ · exact inr ⟨q, hqQ, G.isAncestor_trans haq' haq'q⟩
    Causalean.Graph.DAG.ancestralSet_subset_of_subset_ancestralSet · Causalean/Graph/DSep/OrderedLocalSG/Defs.lean:125
  • ancestralSet_card_lt_of_peel theorem — In a finite directed acyclic graph, let a selected vertex lie in a seed's ancestral closure and maximize topological order there. If a new seed lies in that closure but omits that vertex, then the new seed's ancestral closure has strictly smaller cardinality.
    hypotheses
    V :
    Type u_1
    shared
    G :
    DAG V
    shared
    Q Q' :
    Finset V
    n :
    V
    hnAnc :
    n ∈ G.ancestralSet Q
    hmax :
    ∀ m ∈ G.ancestralSet Q, G.topoOrder m ≤ G.topoOrder n
    hQ'sub :
    Q' ⊆ G.ancestralSet Q
    hnQ' :
    n ∉ Q'
    conclusion
    (G.ancestralSet Q').card < (G.ancestralSet Q).card
    Proof (Lean source)
    theorem ancestralSet_card_lt_of_peel {Q Q' : Finset V} {n : V} (hnAnc : n ∈ G.ancestralSet Q) (hmax : ∀ m ∈ G.ancestralSet Q, G.topoOrder m ≤ G.topoOrder n) (hQ'sub : Q' ⊆ G.ancestralSet Q) (hnQ' : n ∉ Q') : (G.ancestralSet Q').card < (G.ancestralSet Q).card := by apply Finset.card_lt_card rw [Finset.ssubset_iff_of_subset (G.ancestralSet_subset_of_subset_ancestralSet hQ'sub)] refine ⟨n, hnAnc, ?_⟩ intro hnAnc' -- `n ∈ ancestralSet Q'` means either `n ∈ Q'` or `n` is a strict ancestor of some -- `q' ∈ Q' ⊆ ancestralSet Q`; the hypotheses rule out both cases. simp only [ancestralSet, mem_union, ancestorsSet, mem_filter, Finset.mem_univ, true_and] at hnAnc' rcases hnAnc' with hnQ'' | ⟨q', hq'Q', haq'⟩ · exact hnQ' hnQ'' · have hq'Anc : q' ∈ G.ancestralSet Q := hQ'sub hq'Q' have h1 : G.topoOrder q' ≤ G.topoOrder n := hmax q' hq'Anc have h2 : G.topoOrder n < G.topoOrder q' := G.isAncestor_topoOrder_lt haq' omega
    Causalean.Graph.DAG.ancestralSet_card_lt_of_peel · Causalean/Graph/DSep/OrderedLocalSG/Defs.lean:144
  • sup_topoOrder_lt_of_peel theorem — In a finite directed acyclic graph, let a selected vertex maximize topological order in a seed's ancestral closure and belong to a random conditioning set. If a replacement set lies in the closure but omits the selected vertex, then its topological height is strictly smaller than that of the random conditioning set.
    hypotheses
    V :
    Type u_1
    shared
    G :
    DAG V
    shared
    Q Zr S :
    Finset V
    n :
    V
    hmax :
    ∀ m ∈ G.ancestralSet Q, G.topoOrder m ≤ G.topoOrder n
    hnZr :
    n ∈ Zr
    hSsub :
    S ⊆ G.ancestralSet Q
    hnS :
    n ∉ S
    conclusion
    (S.sup (fun v => G.topoOrder v + 1)) < (Zr.sup (fun v => G.topoOrder v + 1))
    Proof (Lean source)
    theorem sup_topoOrder_lt_of_peel {Q Zr S : Finset V} {n : V} (hmax : ∀ m ∈ G.ancestralSet Q, G.topoOrder m ≤ G.topoOrder n) (hnZr : n ∈ Zr) (hSsub : S ⊆ G.ancestralSet Q) (hnS : n ∉ S) : (S.sup (fun v => G.topoOrder v + 1)) < (Zr.sup (fun v => G.topoOrder v + 1)) := by have hZr_ge : G.topoOrder n + 1 ≤ Zr.sup (fun v => G.topoOrder v + 1) := Finset.le_sup (f := fun v => G.topoOrder v + 1) hnZr have hS_le : S.sup (fun v => G.topoOrder v + 1) ≤ G.topoOrder n := by rw [Finset.sup_le_iff] intro s hs have hsAnc : s ∈ G.ancestralSet Q := hSsub hs have hle : G.topoOrder s ≤ G.topoOrder n := hmax s hsAnc have hne : s ≠ n := fun h => hnS (h ▸ hs) have : G.topoOrder s ≠ G.topoOrder n := fun h => hne (G.topoOrder_injective h) omega omega
    Causalean.Graph.DAG.sup_topoOrder_lt_of_peel · Causalean/Graph/DSep/OrderedLocalSG/Defs.lean:168
Closure 1 core · 2 supporting This file carries out the well-founded peel induction proving orderedLocalSG_of_dSep_with_fixed: d-separation with random and fixed conditioning sets yields a derivation from the ordered-local basis and the semi-graphoid ★ orderedLocalSG_of_dSep_with_fixed

Closure of d-separation under the ordered-local rules

This file carries out the well-founded peel induction proving orderedLocalSG_of_dSep_with_fixed: d-separation with random and fixed conditioning sets yields a derivation from the ordered-local basis and the semi-graphoid rules. It also exposes a reachability lemma that extends an active walk by a forward directed arm.

theorem orderedLocalSG_of_dSep_with_fixed reviewed
Causalean.Graph.DAG

d-separation yields an ordered-local derivation. In a DAG G, suppose every vertex of Zf has no parents, i.e. Zf consists of fixed roots, Zf is disjoint from R, and X, Y, and Zr are each contained in R. If X and Y are d-separated by Zr ∪ Zf, then the conditional-independence triple "X ⊥ Y given Zr" is derivable from the ordered-local basis on R via the semi-graphoid axioms.

Formal statement
hypotheses
V :
Type u_1
shared
G :
DAG V
shared
R X Y Zr Zf :
Finset V
hFixedRoots :
∀ f ∈ Zf, G.parents f = ∅
hFR :
Disjoint Zf R
hX :
X ⊆ R
hY :
Y ⊆ R
hZr :
Zr ⊆ R
hdSep :
G.dSep X Y (Zr ∪ Zf)
conclusion
G.OrderedLocalSG R X Y Zr
Proof (Lean source)
theorem orderedLocalSG_of_dSep_with_fixed (R X Y Zr Zf : Finset V) (hFixedRoots : ∀ f ∈ Zf, G.parents f = ∅) (hFR : Disjoint Zf R) (hX : X ⊆ R) (hY : Y ⊆ R) (hZr : Zr ⊆ R) (hdSep : G.dSep X Y (Zr ∪ Zf)) : G.OrderedLocalSG R X Y Zr := by have hXY : Disjoint X Y := hdSep.1 have hXZ : Disjoint X Zr := hdSep.2.1.mono_right Finset.subset_union_left have hYZ : Disjoint Y Zr := hdSep.2.2.1.mono_right Finset.subset_union_left -- Trivial base case: an empty source set. rcases Finset.eq_empty_or_nonempty X with hXe | hXne · subst hXe; exact OrderedLocalSG.nil Y Zr hY hZr -- Abbreviate the query set and select a topological maximum of its ancestral set. set Q : Finset V := X ∪ Y ∪ Zr ∪ Zf with hQ_def have hQne : (G.ancestralSet Q).Nonempty := by obtain ⟨x, hx⟩ := hXne exact ⟨x, G.subset_ancestralSet Q (by simp only [hQ_def, mem_union]; exact inl (inl (inl hx)))⟩ obtain ⟨n, hnAnc, hmax⟩ := Finset.exists_max_image (G.ancestralSet Q) G.topoOrder hQne have hnQ : n ∈ Q := G.topoMax_mem_seed hnAnc hmax -- Membership facts used across the cases. have hnR_of_mem : ∀ {S : Finset V}, S ⊆ R → n ∈ S → n ∉ Zf := by intro S hSR hnS hnF exact (Finset.disjoint_left.mp hFR hnF) (hSR hnS) -- Reusable inclusions for the termination (card-drop) arguments. have hQanc : Q ⊆ G.ancestralSet Q := G.subset_ancestralSet Q have hParAnc : G.parents n ⊆ G.ancestralSet Q := by intro a ha exact G.mem_ancestralSet_of_isAncestor hnQ (isAncestor.edge (G.mem_parents.mp ha)) have hXsubQ : X ⊆ Q := by rw [hQ_def]; intro x hx; simp only [mem_union]; tauto have hYsubQ : Y ⊆ Q := by rw [hQ_def]; intro x hx; simp only [mem_union]; tauto have hZrsubQ : Zr ⊆ Q := by rw [hQ_def]; intro x hx; simp only [mem_union]; tauto have hZfsubQ : Zf ⊆ Q := by rw [hQ_def]; intro x hx; simp only [mem_union]; tauto have hXQ : X ⊆ G.ancestralSet Q := hXsubQ.trans hQanc have hYQ : Y ⊆ G.ancestralSet Q := hYsubQ.trans hQanc have hZrQ : Zr ⊆ G.ancestralSet Q := hZrsubQ.trans hQanc have hZfQ : Zf ⊆ G.ancestralSet Q := hZfsubQ.trans hQanc rw [hQ_def] at hnQ simp only [mem_union] at hnQ -- Case analysis on where the maximal node `n` sits. rcases hnQ with ((hnX | hnY) | hnZr) | hnZf · -- ===== Case n ∈ X ===== set X' : Finset V := X.erase n with hX'_def set A : Finset V := G.parents n ∩ R with hA_def set C : Finset V := Zr ∪ X' with hC_def set A0 : Finset V := A \ C with hA0_def have hnX' : n ∉ X' := Finset.notMem_erase n X have hnZf : n ∉ Zf := fun h => (hnR_of_mem hX hnX) h have hXins : X = insert n X' := (Finset.insert_erase hnX).symm have hX'R : X' ⊆ R := (Finset.erase_subset _ _).trans hX have hX'X : X' ⊆ X := Finset.erase_subset _ _ have hnY : n ∉ Y := fun h => (Finset.disjoint_left.mp hXY hnX) h have hnZr : n ∉ Zr := fun h => (Finset.disjoint_left.mp hXZ hnX) h have hCR : C ⊆ R := Finset.union_subset hZr hX'R have hAR : A ⊆ R := Finset.inter_subset_right have hA0R : A0 ⊆ R := (sdiff_subset).trans hAR -- `n` is not an ancestor of any query node (topological maximality). have hND_Q : ∀ w ∈ Q, ¬ G.isAncestor n w := by intro w hwQ hanc have h1 : G.topoOrder w ≤ G.topoOrder n := hmax w (G.subset_ancestralSet Q hwQ) have h2 : G.topoOrder n < G.topoOrder w := G.isAncestor_topoOrder_lt hanc omega -- ihX': drop `n` from the source. have ihX' : G.OrderedLocalSG R X' Y Zr := orderedLocalSG_of_dSep_with_fixed R X' Y Zr Zf hFixedRoots hFR hX'R hY hZr (G.dSep_subset_left hX'X hdSep) -- `dSep {n} Y (C ∪ Zf)`. have hCZf_eq : C ∪ Zf = (Zr ∪ Zf) ∪ X' := by rw [hC_def]; ext x; simp only [mem_union]; tauto have hdSepN : G.dSep {n} Y (C ∪ Zf) := by rw [hCZf_eq] apply G.dSep_source_to_cond (X := {n}) (S := X') · exact Finset.disjoint_singleton_left.mpr hnX' · rw [show ({n} : Finset V) ∪ X' = X by rw [hXins, Finset.insert_eq]] exact hdSep -- Parents disjoint from `Y`; hence `A0` (⊆ parents) too. have hParY : Disjoint (G.parents n) Y := G.parents_disjoint_of_dSep_singleton hdSepN have hAY : Disjoint A Y := hParY.mono_left Finset.inter_subset_left -- A2f: parents inherit the separation. have hA0_par : ∀ a ∈ A0, G.edge a n := by intro a ha have : a ∈ A := (Finset.mem_sdiff.mp ha).1 exact G.mem_parents.mp (Finset.mem_inter.mp this).1 have hA0_D : ∀ a ∈ A0, a ∉ C ∪ Zf := by intro a ha haCZf rw [mem_union] at haCZf rcases haCZf with haC | haZf · exact (Finset.mem_sdiff.mp ha).2 haC · exact (Finset.disjoint_left.mp hFR haZf) (hA0R ha) have hdSepA0 : G.dSep A0 Y (C ∪ Zf) := G.dSep_parents_of_maximal_source hdSepN hA0_par hA0_D -- ihA0. have ihA0 : G.OrderedLocalSG R A0 Y C := orderedLocalSG_of_dSep_with_fixed R A0 Y C Zf hFixedRoots hFR hA0R hY hCR hdSepA0 -- Basis at `n` with block `P = Y ∪ C ∪ A`. have hPR : Y ∪ C ∪ A ⊆ R := Finset.union_subset (Finset.union_subset hY hCR) hAR -- `Y ∪ C ⊆ Q` (used to inherit `¬ isAncestor n ·` from topo-maximality). have hYC_subQ : Y ∪ C ⊆ Q := by rw [hQ_def, hC_def] intro w hw simp only [mem_union] at hw ⊢ rcases hw with hY' | hZr' | hX'' · exact inl (inl (inr hY')) · exact inl (inr hZr') · exact inl (inl (inl (hX'X hX''))) have hPND : Y ∪ C ∪ A ⊆ G.nonDescendants n := by intro w hw rw [mem_union] at hw simp only [nonDescendants, mem_filter, Finset.mem_univ, true_and] rcases hw with hwYC | hwA · -- w ∈ Y ∪ C ⊆ Q: topo-maximal `n` is no ancestor of `w`, and `w ≠ n`. have hwQ : w ∈ Q := hYC_subQ hwYC refine ⟨hND_Q w hwQ, ?_⟩ rintro rfl rw [mem_union, hC_def, mem_union] at hwYC rcases hwYC with h | h | h exacts [hnY h, hnZr h, hnX' h] · -- w ∈ A = parents n ∩ R: `n` cannot be an ancestor of its own parent. have hwPar : w ∈ G.parents n := (Finset.mem_inter.mp hwA).1 have hedge : G.edge w n := G.mem_parents.mp hwPar refine ⟨fun hanc => ?_, fun hwn => G.irrefl n (hwn ▸ hedge)⟩ exact G.isAncestor_irrefl n (G.isAncestor_trans hanc (isAncestor.edge hedge)) have hAsubP : A ⊆ Y ∪ C ∪ A := Finset.subset_union_right have hPaR_sub : G.parents n ∩ R ⊆ Y ∪ C ∪ A := by rw [← hA_def]; exact hAsubP have hbasis := OrderedLocalSG.basis (G := G) (R := R) n (hX hnX) (Y ∪ C ∪ A) hPR hPND hPaR_sub -- `(Y ∪ C ∪ A) \ (parents n ∩ R) = Y ∪ (C \ A)`. have hsdiff_eq : (Y ∪ C ∪ A) \ (G.parents n ∩ R) = Y ∪ (C \ A) := by rw [← hA_def]; ext x simp only [mem_sdiff, mem_union] constructor · rintro ⟨(hY' | hC') | hA', hnA⟩ · exact inl hY' · exact inr ⟨hC', hnA⟩ · exact absurd hA' hnA · rintro (hY' | ⟨hC', hnA⟩) · exact ⟨Or.inl (inl hY'), fun hA' => (Finset.disjoint_left.mp hAY hA') hY'⟩ · exact ⟨Or.inl (inr hC'), hnA⟩ rw [hsdiff_eq, ← hA_def] at hbasis -- weakUnion: move `C \ A` into the condition; `A ∪ (C \ A) = C ∪ A0`. have hweak := OrderedLocalSG.weakUnion (W := C \ A) (Z := A) hbasis have hAC_eq : A ∪ (C \ A) = C ∪ A0 := by rw [hA0_def]; ext x simp only [mem_union, mem_sdiff]; tauto rw [hAC_eq] at hweak -- hweak : {n} ⊥ Y | (C ∪ A0). Fold with ihA0 to drop `A0`. have hstep2 : G.OrderedLocalSG R {n} Y C := by have h1 : G.OrderedLocalSG R Y {n} (C ∪ A0) := hweak.symm have h2 : G.OrderedLocalSG R Y A0 C := ihA0.symm have hc : G.OrderedLocalSG R Y ({n} ∪ A0) C := OrderedLocalSG.contract h1 h2 exact (OrderedLocalSG.decomp (W := A0) hc).symm -- Final fold with ihX': `{n}∪X' = X`. have h1 : G.OrderedLocalSG R Y {n} (Zr ∪ X') := by rw [← hC_def]; exact hstep2.symm have h2 : G.OrderedLocalSG R Y X' Zr := ihX'.symm have hc : G.OrderedLocalSG R Y ({n} ∪ X') Zr := OrderedLocalSG.contract h1 h2 rw [show ({n} : Finset V) ∪ X' = X by rw [hXins, Finset.insert_eq]] at hc exact hc.symm · -- ===== Case n ∈ Y ===== (mirror of the n ∈ X case with X ↔ Y) refine OrderedLocalSG.symm ?_ have hdSepYX : G.dSep Y X (Zr ∪ Zf) := G.dSep_symm _ _ _ hdSep set Y' : Finset V := Y.erase n with hY'_def set A : Finset V := G.parents n ∩ R with hA_def set C : Finset V := Zr ∪ Y' with hC_def set A0 : Finset V := A \ C with hA0_def have hnY' : n ∉ Y' := Finset.notMem_erase n Y have hnZf : n ∉ Zf := fun h => (hnR_of_mem hY hnY) h have hYins : Y = insert n Y' := (Finset.insert_erase hnY).symm have hY'R : Y' ⊆ R := (Finset.erase_subset _ _).trans hY have hY'Y : Y' ⊆ Y := Finset.erase_subset _ _ have hnX : n ∉ X := fun h => (Finset.disjoint_left.mp hXY h) hnY have hnZr : n ∉ Zr := fun h => (Finset.disjoint_left.mp hYZ hnY) h have hCR : C ⊆ R := Finset.union_subset hZr hY'R have hAR : A ⊆ R := Finset.inter_subset_right have hA0R : A0 ⊆ R := (sdiff_subset).trans hAR have hND_Q : ∀ w ∈ Q, ¬ G.isAncestor n w := by intro w hwQ hanc have h1 : G.topoOrder w ≤ G.topoOrder n := hmax w (G.subset_ancestralSet Q hwQ) have h2 : G.topoOrder n < G.topoOrder w := G.isAncestor_topoOrder_lt hanc omega have ihY' : G.OrderedLocalSG R Y' X Zr := orderedLocalSG_of_dSep_with_fixed R Y' X Zr Zf hFixedRoots hFR hY'R hX hZr (G.dSep_subset_left hY'Y hdSepYX) have hCZf_eq : C ∪ Zf = (Zr ∪ Zf) ∪ Y' := by rw [hC_def]; ext x; simp only [mem_union]; tauto have hdSepN : G.dSep {n} X (C ∪ Zf) := by rw [hCZf_eq] apply G.dSep_source_to_cond (X := {n}) (S := Y') · exact Finset.disjoint_singleton_left.mpr hnY' · rw [show ({n} : Finset V) ∪ Y' = Y by rw [hYins, Finset.insert_eq]] exact hdSepYX have hParX : Disjoint (G.parents n) X := G.parents_disjoint_of_dSep_singleton hdSepN have hAX : Disjoint A X := hParX.mono_left Finset.inter_subset_left have hA0_par : ∀ a ∈ A0, G.edge a n := by intro a ha have : a ∈ A := (Finset.mem_sdiff.mp ha).1 exact G.mem_parents.mp (Finset.mem_inter.mp this).1 have hA0_D : ∀ a ∈ A0, a ∉ C ∪ Zf := by intro a ha haCZf rw [mem_union] at haCZf rcases haCZf with haC | haZf · exact (Finset.mem_sdiff.mp ha).2 haC · exact (Finset.disjoint_left.mp hFR haZf) (hA0R ha) have hdSepA0 : G.dSep A0 X (C ∪ Zf) := G.dSep_parents_of_maximal_source hdSepN hA0_par hA0_D have ihA0 : G.OrderedLocalSG R A0 X C := orderedLocalSG_of_dSep_with_fixed R A0 X C Zf hFixedRoots hFR hA0R hX hCR hdSepA0 have hPR : X ∪ C ∪ A ⊆ R := Finset.union_subset (Finset.union_subset hX hCR) hAR have hXC_subQ : X ∪ C ⊆ Q := by rw [hQ_def, hC_def] intro w hw simp only [mem_union] at hw ⊢ rcases hw with hX' | hZr' | hY'' · exact inl (inl (inl hX')) · exact inl (inr hZr') · exact inl (inl (inr (hY'Y hY''))) have hPND : X ∪ C ∪ A ⊆ G.nonDescendants n := by intro w hw rw [mem_union] at hw simp only [nonDescendants, mem_filter, Finset.mem_univ, true_and] rcases hw with hwXC | hwA · have hwQ : w ∈ Q := hXC_subQ hwXC refine ⟨hND_Q w hwQ, ?_⟩ rintro rfl rw [mem_union, hC_def, mem_union] at hwXC rcases hwXC with h | h | h exacts [hnX h, hnZr h, hnY' h] · have hwPar : w ∈ G.parents n := (Finset.mem_inter.mp hwA).1 have hedge : G.edge w n := G.mem_parents.mp hwPar refine ⟨fun hanc => ?_, fun hwn => G.irrefl n (hwn ▸ hedge)⟩ exact G.isAncestor_irrefl n (G.isAncestor_trans hanc (isAncestor.edge hedge)) have hPaR_sub : G.parents n ∩ R ⊆ X ∪ C ∪ A := by rw [← hA_def]; exact Finset.subset_union_right -- … truncated; follow the source link for the rest …
Causalean.Graph.DAG.orderedLocalSG_of_dSep_with_fixed · Causalean/Graph/DSep/OrderedLocalSG/Closure.lean:270 · uses DAG , OrderedLocalSG , dSep , parents
2 supporting declarations (lemmas, instances)
  • branch_seed_eq theorem — For a finite vertex population, four vertex sets and a selected vertex, if the selected vertex belongs to the third set, then removing and reinserting it while forming the union leaves that union unchanged.
    hypotheses
    V :
    Type u_1
    Finset V
    V
    shared
    hn :
    n ∈ Zr
    conclusion
    a ∪ {n} ∪ (Zr.erase n ∪ b) ∪ c = a ∪ b ∪ Zr ∪ c
    Proof (Lean source)
    theorem branch_seed_eq {a b Zr c : Finset V} {n : V} (hn : n ∈ Zr) : a ∪ {n} ∪ (Zr.erase n ∪ b) ∪ c = a ∪ b ∪ Zr ∪ c := by ext x; simp only [mem_union, Finset.mem_singleton, Finset.mem_erase] constructor · rintro (((h | h) | (h | h)) | h) · exact inl (inl (inl h)) · exact inl (inr (h ▸ hn)) · exact inl (inr h.2) · exact inl (inl (inr h)) · exact inr h · rintro (((h | h) | h) | h) · exact inl (inl (inl h)) · exact inl (inr (inr h)) · by_cases hx : x = n · exact inl (inl (inr hx)) · exact inl (inr (inl ⟨hx, h⟩)) · exact inr h
    Causalean.Graph.DAG.branch_seed_eq · Causalean/Graph/DSep/OrderedLocalSG/Closure.lean:245
  • bbReachable_extend_directed_arm theorem — Given a directed acyclic graph, conditioning set, endpoints, and two walks, if the first walk has at least two vertices, begins at the first endpoint, ends at the seam vertex, and is active, while the second walk has at least two vertices, begins at the seam, ends at the final endpoint, follows directed edges, has no conditioned interior vertices, and the seam is not conditioned on, then the final endpoint is Bayes-ball reachable from the first.
    hypotheses
    V :
    Type u_1
    shared
    G :
    DAG V
    shared
    Z :
    Finset V
    a c b :
    V
    pa q :
    List V
    hpa_len :
    pa.length ≥ 2
    hpa_head :
    pa.head? = some a
    hpa_last :
    pa.getLast? = some c
    hpa_act :
    G.IsActiveWalk Z pa
    hq_len :
    q.length ≥ 2
    hq_head :
    q.head? = some c
    hq_last :
    q.getLast? = some b
    hq_edge :
    ∀ (i : ℕ) (hi : i + 1 < q.length), G.edge (q.get ⟨i, by omega⟩) (q.get ⟨i + 1, hi⟩)
    hq_int :
    ∀ (i : ℕ) (hi : i + 2 < q.length), q.get ⟨i + 1, by omega⟩ ∉ Z
    hcZ :
    c ∉ Z
    conclusion
    b ∈ G.bbReachableVertices Z ({a} : Finset V)
    Proof (Lean source)
    theorem bbReachable_extend_directed_arm {Z : Finset V} {a c b : V} {pa q : List V} (hpa_len : pa.length ≥ 2) (hpa_head : pa.head? = some a) (hpa_last : pa.getLast? = some c) (hpa_act : G.IsActiveWalk Z pa) (hq_len : q.length ≥ 2) (hq_head : q.head? = some c) (hq_last : q.getLast? = some b) (hq_edge : ∀ (i : ℕ) (hi : i + 1 < q.length), G.edge (q.get ⟨i, by omega⟩) (q.get ⟨i + 1, hi⟩)) (hq_int : ∀ (i : ℕ) (hi : i + 2 < q.length), q.get ⟨i + 1, by omega⟩ ∉ Z) (hcZ : c ∉ Z) : b ∈ G.bbReachableVertices Z ({a} : Finset V) := by have hq_act : G.IsActiveWalk Z q := G.isActiveWalk_of_directed hq_edge hq_int have hqne : q ≠ [] := by intro h; rw [h] at hq_len; simp at hq_len -- First edge of `q` points out of `c`. have hq_head_eq : q.get ⟨0, by omega⟩ = c := by have h := List.head?_eq_some_head hqne rw [hq_head] at h rw [List.get_eq_getElem, List.getElem_zero] exact Option.some_inj.mp h.symm have hseam_out : G.edge c (q.get ⟨1, by omega⟩) := by have he := hq_edge 0 (by omega) rwa [hq_head_eq] at he obtain ⟨_, hjhead, hjlast, hjact⟩ := G.chain_join_active hpa_len hpa_head hpa_last hpa_act hq_len hq_head hq_last hq_act hseam_out hcZ rw [G.bbReachableVertices_iff_activeWalk] exact ⟨a, mem_singleton_self a, pa ++ q.tail, by rw [List.length_append]; have := List.length_tail (l := q); omega, hjact, hjhead, hjlast⟩
    Causalean.Graph.DAG.bbReachable_extend_directed_arm · Causalean/Graph/DSep/OrderedLocalSG/Closure.lean:666
Path­Joining 1 core · 3 supporting This file develops the walk-composition tools for the ordered-local induction. ★ survive_or_splice

Joining active walks in the ordered-local peel

This file develops the walk-composition tools for the ordered-local induction. It joins active walks across non-collider seams, relates forward directed walks to ancestry, preserves activity under prefix extraction, and proves the survive-or-splice alternative used when a maximal conditioning vertex is removed.

theorem survive_or_splice reviewed
Causalean.Graph.DAG

For a finite directed acyclic graph, two endpoint sets, a conditioning set, an auxiliary set, an ambient ancestral query set, a walk, and its endpoints, if all relevant vertices lie in the ambient query set, the terminal vertex is topologically maximal in its ancestral closure, the initial vertex belongs to its endpoint set, the walk has at least two vertices, the walk is active under the cross-conditioning set, the walk begins at the stated initial vertex, and ends at the maximal vertex, then either an active walk can be spliced to the auxiliary endpoint set or an active walk survives to the maximal vertex with its last edge directed inward.

Formal statement
hypotheses
V :
Type u_1
shared
G :
DAG V
shared
S A W bigQ :
Finset V
p :
List V
a n :
V
hbigQ :
A ∪ {n} ∪ (S ∪ W) ⊆ bigQ
hmax :
∀ m ∈ G.ancestralSet bigQ, G.topoOrder m ≤ G.topoOrder n
haA :
a ∈ A
hlen :
p.length ≥ 2
hact :
G.IsActiveWalk (S ∪ W) p
hhead :
p.head? = some a
hlast :
p.getLast? = some n
conclusion
(∃ (q : List V) (w : V), w ∈ W ∧ q.length ≥ 2 ∧ G.IsActiveWalk (insert n S) q ∧ q.head? = some a ∧ q.getLast? = some w) ∨ (∃ (q : List V) (hq2 : q.length ≥ 2), G.IsActiveWalk (insert n S) q ∧ q.head? = some a ∧ q.getLast? = some n ∧ G.edge (q.get ⟨q.length - 2, by omega⟩) n)
Proof (Lean source)
theorem survive_or_splice {S A W bigQ : Finset V} {p : List V} {a n : V} (hbigQ : A ∪ {n} ∪ (S ∪ W) ⊆ bigQ) (hmax : ∀ m ∈ G.ancestralSet bigQ, G.topoOrder m ≤ G.topoOrder n) (haA : a ∈ A) (hlen : p.length ≥ 2) (hact : G.IsActiveWalk (S ∪ W) p) (hhead : p.head? = some a) (hlast : p.getLast? = some n) : (∃ (q : List V) (w : V), w ∈ W ∧ q.length ≥ 2 ∧ G.IsActiveWalk (insert n S) q ∧ q.head? = some a ∧ q.getLast? = some w) ∨ (∃ (q : List V) (hq2 : q.length ≥ 2), G.IsActiveWalk (insert n S) q ∧ q.head? = some a ∧ q.getLast? = some n ∧ G.edge (q.get ⟨q.length - 2, by omega⟩) n) := by -- Nodes of `p` lie in `ancestralSet bigQ`. have hpAnc : ∀ v ∈ p, v ∈ G.ancestralSet bigQ := by intro v hv have := G.activeWalk_nodes_are_ancestors haA (mem_singleton_self n) hact hhead hlast v hv exact G.ancestralSet_mono hbigQ this -- `n` is never an interior non-collider on `p` (topological maximality). have hno_n : ∀ (i : ℕ) (hi : i + 2 < p.length), p.get ⟨i + 1, by omega⟩ = n → G.IsCollider (p.get ⟨i, by omega⟩) (p.get ⟨i + 1, by omega⟩) (p.get ⟨i + 2, hi⟩) := by intro i hi hmn by_contra hC obtain ⟨hadj, _⟩ := hact have hout := G.nonCollider_has_outgoing (hadj i (by omega)) (hadj (i + 1) (by omega)) hC rcases hout with hedge | hedge <;> rw [hmn] at hedge · have h1 : G.topoOrder (p.get ⟨i, by omega⟩) ≤ G.topoOrder n := hmax _ (hpAnc _ (List.get_mem p ⟨i, by omega⟩)) have h2 := G.isAncestor_topoOrder_lt (isAncestor.edge hedge); omega · have h1 : G.topoOrder (p.get ⟨i + 1 + 1, by omega⟩) ≤ G.topoOrder n := hmax _ (hpAnc _ (List.get_mem p ⟨i + 1 + 1, by omega⟩)) have h2 := G.isAncestor_topoOrder_lt (isAncestor.edge hedge); omega -- Bad indices: interior colliders whose middle is NOT activated by `S` alone. classical let P : ℕ → Prop := fun i => ∃ (hi : i + 2 < p.length), G.IsCollider (p.get ⟨i, by omega⟩) (p.get ⟨i + 1, by omega⟩) (p.get ⟨i + 2, hi⟩) ∧ p.get ⟨i + 1, by omega⟩ ∉ G.ancestralSet S let Bad : Finset ℕ := (range p.length).filter P by_cases hBad : Bad.Nonempty · -- ===== SPLICE branch ===== refine inl ?_ set i₀ := Bad.min' hBad with hi₀_def have hi₀_mem : i₀ ∈ Bad := Bad.min'_mem hBad have hi₀_range : i₀ ∈ range p.length ∧ P i₀ := by have := hi₀_mem; simp only [Bad, mem_filter] at this; exact this obtain ⟨hi₀, hC₀, hcS₀⟩ := hi₀_range.2 set c := p.get ⟨i₀ + 1, by omega⟩ with hc_def -- Minimality: every interior collider strictly before `i₀` is `S`-activated. have hmin : ∀ (j : ℕ) (hj : j + 2 < p.length), j < i₀ → G.IsCollider (p.get ⟨j, by omega⟩) (p.get ⟨j + 1, by omega⟩) (p.get ⟨j + 2, hj⟩) → p.get ⟨j + 1, by omega⟩ ∈ G.ancestralSet S := by intro j hj hjlt hCj by_contra hnotanc have hjBad : j ∈ Bad := by simp only [Bad, mem_filter, Finset.mem_range] exact ⟨by omega, hj, hCj, hnotanc⟩ have := Bad.min'_le j hjBad rw [← hi₀_def] at this; omega -- The collider middle `c` is activated by `S ∪ W`. have hc_act : c ∈ G.ancestralSet (S ∪ W) := by have h := hact.2 i₀ hi₀ simp only at h rw [if_pos hC₀] at h exact h -- Prefix `q1 := p.take (i₀ + 2)`, ending at `c`, active given `insert n S`. set q1 := p.take (i₀ + 2) with hq1_def have hq1_len : q1.length = i₀ + 2 := by rw [hq1_def, List.length_take]; omega have hq1_get : ∀ (j : ℕ) (hj : j < q1.length), q1.get ⟨j, hj⟩ = p.get ⟨j, by rw [hq1_len] at hj; omega⟩ := by intro j hj; simp only [hq1_def, List.get_eq_getElem, List.getElem_take] have hq1_act_SW : G.IsActiveWalk (S ∪ W) q1 := G.isActiveWalk_take hact have hq1_head : q1.head? = some a := by have hq1ne : q1 ≠ [] := by intro h; rw [h] at hq1_len; simp at hq1_len rw [List.head?_eq_some_head hq1ne] have hh0 : q1.head hq1ne = q1.get ⟨0, by omega⟩ := by rw [List.get_eq_getElem, ← List.head_eq_getElem] rw [hh0, hq1_get 0 (by omega)] have hpne : p ≠ [] := by intro h; rw [h] at hlen; simp at hlen have hh := List.head?_eq_some_head hpne; rw [hhead] at hh have hpa : p.head hpne = a := Option.some_inj.mp hh.symm rw [show p.get ⟨0, by omega⟩ = p.head hpne by rw [List.get_eq_getElem, ← List.head_eq_getElem], hpa] have hq1_last : q1.getLast? = some c := by have hq1ne : q1 ≠ [] := by intro h; rw [h] at hq1_len; simp at hq1_len rw [getLast?_eq_some_getLast hq1ne] have heq : q1.getLast hq1ne = q1.get ⟨q1.length - 1, by omega⟩ := by rw [List.get_eq_getElem, ← List.getLast_eq_getElem] rw [heq, hq1_get (q1.length - 1) (by omega)] have hidx : q1.length - 1 = i₀ + 1 := by omega simp only [hidx, hc_def] -- Lift `q1` to `insert n S`. have hq1_collS : ∀ (i : ℕ) (hi : i + 2 < q1.length), G.IsCollider (q1.get ⟨i, by omega⟩) (q1.get ⟨i + 1, by omega⟩) (q1.get ⟨i + 2, hi⟩) → q1.get ⟨i + 1, by omega⟩ ∈ G.ancestralSet S := by intro i hi hC simp only [hq1_get] at hC ⊢ have hi_p : i + 2 < p.length := by rw [hq1_len] at hi; omega exact hmin i hi_p (by rw [hq1_len] at hi; omega) hC have hq1_no_n : ∀ (i : ℕ) (hi : i + 2 < q1.length), q1.get ⟨i + 1, by omega⟩ = n → G.IsCollider (q1.get ⟨i, by omega⟩) (q1.get ⟨i + 1, by omega⟩) (q1.get ⟨i + 2, hi⟩) := by intro i hi hmn simp only [hq1_get] at hmn ⊢ exact hno_n i (by rw [hq1_len] at hi; omega) hmn have hq1_act : G.IsActiveWalk (insert n S) q1 := G.lift_crosscond_to_insert hq1_act_SW hq1_collS hq1_no_n -- Peel `c`'s activation: `c ∈ W` or `c` is a strict ancestor of some `w0 ∈ W`. have hc_peel : c ∈ W ∨ ∃ w0 ∈ W, G.isAncestor c w0 := by simp only [ancestralSet, mem_union, ancestorsSet, mem_filter, Finset.mem_univ, true_and] at hc_act rcases hc_act with (hcS | hcW) | ⟨s, hsSW, hanc⟩ · exact absurd (G.subset_ancestralSet S hcS) hcS₀ · exact inl hcW · rcases hsSW with hsS | hsW · exact absurd (G.mem_ancestralSet_of_isAncestor hsS hanc) hcS₀ · exact inr ⟨s, hsW, hanc⟩ -- `c ∈ ancestralSet bigQ`, so `topoOrder c ≤ topoOrder n`; combined below. have hc_bigQ : c ∈ G.ancestralSet bigQ := hpAnc c (List.get_mem p ⟨i₀ + 1, by omega⟩) rcases hc_peel with hcW | ⟨w0, hw0W, hcw0⟩ · -- `c ∈ W`: the prefix `q1` already ends in `W`. exact ⟨q1, c, hcW, by rw [hq1_len]; omega, hq1_act, hq1_head, hq1_last⟩ · -- Descend `c → w0 ∈ W` and splice. have hw0_bigQ : w0 ∈ G.ancestralSet bigQ := G.subset_ancestralSet bigQ (hbigQ (by simp only [mem_union]; exact inr (inr hw0W))) have hw0n : G.topoOrder w0 ≤ G.topoOrder n := hmax w0 hw0_bigQ obtain ⟨dq, hdq2, hdq_head, hdq_last, hdq_act, hdq_first⟩ := G.descent_active_insert hcw0 hcS₀ hw0n -- Splice `q1 ++ dq.tail` at the non-collider `c`. have hcne : c ∉ insert n S := by rw [Finset.mem_insert, not_or] refine ⟨?_, fun hcS => hcS₀ (G.subset_ancestralSet S hcS)⟩ -- `c ≠ n`: `isAncestor c w0` with `topoOrder w0 ≤ topoOrder n` forces `c ≠ n`. intro hcn have h2 := G.isAncestor_topoOrder_lt hcw0 rw [hcn] at h2; omega obtain ⟨_, hjoin_head, hjoin_last, hjoin_act⟩ := G.chain_join_active (by rw [hq1_len]; omega) hq1_head hq1_last hq1_act hdq2 hdq_head hdq_last hdq_act hdq_first hcne refine ⟨q1 ++ dq.tail, w0, hw0W, ?_, hjoin_act, hjoin_head, hjoin_last⟩ rw [List.length_append]; rw [hq1_len]; omega · -- ===== SURVIVE branch ===== refine inr ?_ -- Every interior collider middle is `S`-activated (Bad empty). have hcollS : ∀ (i : ℕ) (hi : i + 2 < p.length), G.IsCollider (p.get ⟨i, by omega⟩) (p.get ⟨i + 1, by omega⟩) (p.get ⟨i + 2, hi⟩) → p.get ⟨i + 1, by omega⟩ ∈ G.ancestralSet S := by intro i hi hC by_contra hnotanc exact hBad ⟨i, by simp only [Bad, mem_filter, Finset.mem_range] exact ⟨by omega, hi, hC, hnotanc⟩⟩ have hact' : G.IsActiveWalk (insert n S) p := G.lift_crosscond_to_insert hact hcollS hno_n have hedge_in : G.edge (p.get ⟨p.length - 2, by omega⟩) n := G.last_edge_into_max hlen hact hlast hpAnc hmax exact ⟨p, hlen, hact', hhead, hlast, hedge_in⟩
Causalean.Graph.DAG.survive_or_splice · Causalean/Graph/DSep/OrderedLocalSG/PathJoining.lean:307 · uses DAG , IsActiveWalk , ancestralSet , topoOrder
3 supporting declarations (lemmas, instances)
  • chain_join_active theorem — In a finite directed acyclic graph, consider a conditioning set, joining vertex, endpoints, and two walks. If the first walk is active from the first endpoint to the join, the second is active from the join to the second endpoint, its first edge points out of the join, and the joining vertex is not conditioned on, then concatenating the walks gives an active walk between the endpoints.
    hypotheses
    V :
    Type u_1
    shared
    G :
    DAG V
    shared
    Z :
    Finset V
    m x y :
    V
    pa pb :
    List V
    hpa_len :
    pa.length ≥ 2
    hpa_head :
    pa.head? = some x
    hpa_last :
    pa.getLast? = some m
    hpa_act :
    G.IsActiveWalk Z pa
    hpb_len :
    pb.length ≥ 2
    hpb_head :
    pb.head? = some m
    hpb_last :
    pb.getLast? = some y
    hpb_act :
    G.IsActiveWalk Z pb
    hseam_out :
    G.edge m (pb.get ⟨1, by omega⟩)
    hmZ :
    m ∉ Z
    conclusion
    p :
    pa ++ pb.tail
    p.length ≥ 2
    p.head? = some x
    p.getLast? = some y
    G.IsActiveWalk Z p
    Proof (Lean source)
    theorem chain_join_active {Z : Finset V} {m x y : V} {pa pb : List V} (hpa_len : pa.length ≥ 2) (hpa_head : pa.head? = some x) (hpa_last : pa.getLast? = some m) (hpa_act : G.IsActiveWalk Z pa) (hpb_len : pb.length ≥ 2) (hpb_head : pb.head? = some m) (hpb_last : pb.getLast? = some y) (hpb_act : G.IsActiveWalk Z pb) (hseam_out : G.edge m (pb.get ⟨1, by omega⟩)) (hmZ : m ∉ Z) : let p := pa ++ pb.tail p.length ≥ 2 ∧ p.head? = some x ∧ p.getLast? = some y ∧ G.IsActiveWalk Z p := by have hpa_ne : pa ≠ [] := by intro h; rw [h] at hpa_len; simp at hpa_len have hpb_ne : pb ≠ [] := by intro h; rw [h] at hpb_len; simp at hpb_len -- pb.head = m have hpb_head_eq : pb.head hpb_ne = m := by have h := List.head?_eq_some_head hpb_ne; rw [hpb_head] at h exact (Option.some_inj.mp h.symm) -- pa.getLast = m have hpa_last_eq : pa.getLast hpa_ne = m := by have h := getLast?_eq_some_getLast hpa_ne; rw [hpa_last] at h exact (Option.some_inj.mp h.symm) -- pa.head = x have hpa_head_eq : pa.head hpa_ne = x := by have h := List.head?_eq_some_head hpa_ne; rw [hpa_head] at h exact (Option.some_inj.mp h.symm) -- pb.getLast = y have hpb_last_eq : pb.getLast hpb_ne = y := by have h := getLast?_eq_some_getLast hpb_ne; rw [hpb_last] at h exact (Option.some_inj.mp h.symm) -- pb = m :: pb.tail have hpb_decomp : pb = m :: pb.tail := by conv_lhs => rw [← List.cons_head_tail hpb_ne]; rw [hpb_head_eq] have hpb_tail_len : pb.tail.length = pb.length - 1 := List.length_tail have hpb_tail_ne : pb.tail ≠ [] := by rw [← List.length_pos_iff, hpb_tail_len]; omega set p := pa ++ pb.tail with hp_def set R := pa.length with hR_def have hp_len_eq : p.length = R + pb.tail.length := by simp only [hp_def, List.length_append, ← hR_def] have hp_len : p.length ≥ 2 := by rw [hp_len_eq]; omega have hp_head : p.head? = some x := by have : p.head? = pa.head? := List.head?_append_of_ne_nil _ hpa_ne rw [this, hpa_head] have hp_last : p.getLast? = some y := by have hlast_tail : pb.tail.getLast? = some y := by have heq : pb = [m] ++ pb.tail := by simpa using hpb_decomp have := getLast?_append_of_ne_nil [m] hpb_tail_ne rw [← heq] at this; rw [← this]; exact hpb_last simp only [hp_def, getLast?_append, hlast_tail]; rfl refine ⟨hp_len, hp_head, hp_last, ?_⟩ -- Index translation: p[k] = pa[k] for k < R; p[k] = pb[k-R+1] for k ≥ R. have hp_L : ∀ (k : ℕ) (hkR : k < R), p.get ⟨k, by rw [hp_len_eq]; omega⟩ = pa.get ⟨k, hkR⟩ := by intro k hkR simp only [hp_def, List.get_eq_getElem, List.getElem_append_left (h := hkR)] have hpb_tail_get : ∀ (j : ℕ) (hj1 : j < pb.tail.length) (hj2 : j + 1 < pb.length), pb.tail[j]'hj1 = pb[j + 1]'hj2 := by intro j hj1 hj2 have : pb[j + 1] = (m :: pb.tail)[j + 1]'(by rw [← hpb_decomp]; exact hj2) := by congr 1 rw [this]; simp [List.getElem_cons_succ] have hp_R : ∀ (k : ℕ) (hkL : R ≤ k) (hk : k < p.length), p.get ⟨k, hk⟩ = pb.get ⟨k - R + 1, by rw [hp_len_eq, hpb_tail_len] at hk; omega⟩ := by intro k hkL hk have hk_app : R ≤ k := hkL have htail_idx_lt : k - R < pb.tail.length := by rw [hp_len_eq] at hk; omega have hpget : p.get ⟨k, hk⟩ = pb.tail[k - R]'htail_idx_lt := by simp only [hp_def, List.get_eq_getElem] rw [List.getElem_append_right (by rw [← hR_def]; exact hk_app)] rw [hpget] rw [hpb_tail_get (k - R) htail_idx_lt (by rw [hpb_tail_len] at htail_idx_lt; omega)] simp [List.get_eq_getElem] -- pb[0] = m, pa[R-1] = m. have hpb_get_0 : pb.get ⟨0, by omega⟩ = m := by rw [List.get_eq_getElem, List.getElem_zero]; exact hpb_head_eq have hpa_get_last : pa.get ⟨R - 1, by omega⟩ = m := by rw [List.get_eq_getElem] have := List.getLast_eq_getElem hpa_ne rw [hpa_last_eq] at this rw [← this] refine ⟨?_, ?_⟩ · -- Adjacency. intro i hi rw [hp_len_eq] at hi by_cases hA1 : i + 1 < R · have hiR : i < R := by omega rw [hp_L i hiR, hp_L (i + 1) hA1] exact hpa_act.1 i hA1 · push_neg at hA1 by_cases hA2 : i + 1 = R · have hi_eq : i = R - 1 := by omega subst hi_eq have hiR : R - 1 < R := by omega rw [hp_L (R - 1) hiR] have hi1L : R ≤ R - 1 + 1 := by omega have hi1_lt : R - 1 + 1 < p.length := by rw [hp_len_eq]; exact hi rw [hp_R (R - 1 + 1) hi1L hi1_lt] rw [hpa_get_last] have h_yidx : R - 1 + 1 - R + 1 = 1 := by omega rw [show (⟨R - 1 + 1 - R + 1, by rw [hp_len_eq, hpb_tail_len] at hi1_lt; omega⟩ : Fin pb.length) = ⟨1, by omega⟩ from Fin.ext h_yidx] exact Or.inl hseam_out · have hiL : R ≤ i := by omega have hi1L : R ≤ i + 1 := by omega have hi_lt : i < p.length := by rw [hp_len_eq]; omega have hi1_lt : i + 1 < p.length := by rw [hp_len_eq]; exact hi rw [hp_R i hiL hi_lt, hp_R (i + 1) hi1L hi1_lt] have hidx : (i - R + 1) + 1 < pb.length := by omega have hadj := hpb_act.1 (i - R + 1) hidx have he : (i - R + 1) + 1 = (i + 1) - R + 1 := by omega rw [show (⟨(i - R + 1) + 1, hidx⟩ : Fin pb.length) = ⟨(i + 1) - R + 1, by omega⟩ from Fin.ext he] at hadj exact hadj · -- Collider condition. intro i hi rw [hp_len_eq] at hi by_cases hC1 : i + 2 < R · have hiR : i < R := by omega have hi1R : i + 1 < R := by omega rw [hp_L i hiR, hp_L (i + 1) hi1R, hp_L (i + 2) hC1] exact hpa_act.2 i hC1 · push_neg at hC1 by_cases hC2 : i + 2 = R · have hi_eq : i = R - 2 := by omega subst hi_eq have hiR : R - 2 < R := by omega have hi1R : R - 2 + 1 < R := by omega have hi2L : R ≤ R - 2 + 2 := by omega have hi2_lt : R - 2 + 2 < p.length := by rw [hp_len_eq]; exact hi rw [hp_L (R - 2) hiR, hp_L (R - 2 + 1) hi1R, hp_R (R - 2 + 2) hi2L hi2_lt] rw [show (⟨R - 2 + 1, by omega⟩ : Fin pa.length) = ⟨R - 1, by omega⟩ from Fin.ext (show R - 2 + 1 = R - 1 by omega)] rw [hpa_get_last] have h_ridx : R - 2 + 2 - R + 1 = 1 := by omega rw [show (⟨R - 2 + 2 - R + 1, by rw [hp_len_eq, hpb_tail_len] at hi2_lt; omega⟩ : Fin pb.length) = ⟨1, by omega⟩ from Fin.ext h_ridx] have hNotColl : ¬ G.IsCollider (pa.get ⟨R - 2, by omega⟩) m (pb.get ⟨1, by omega⟩) := by intro hColl exact (G.asymm hseam_out) hColl.2 rw [if_neg hNotColl] exact hmZ · by_cases hC3 : i + 1 = R · have hi_eq : i = R - 1 := by omega subst hi_eq have hiR : R - 1 < R := by omega have hi1L : R ≤ R - 1 + 1 := by omega have hi2L : R ≤ R - 1 + 2 := by omega have hi1_lt : R - 1 + 1 < p.length := by rw [hp_len_eq]; omega have hi2_lt : R - 1 + 2 < p.length := by rw [hp_len_eq]; exact hi rw [hp_L (R - 1) hiR, hp_R (R - 1 + 1) hi1L hi1_lt, hp_R (R - 1 + 2) hi2L hi2_lt] rw [hpa_get_last] rw [show (⟨R - 1 + 1 - R + 1, by omega⟩ : Fin pb.length) = ⟨1, by omega⟩ from Fin.ext (show R - 1 + 1 - R + 1 = 1 by omega)] rw [show (⟨R - 1 + 2 - R + 1, by omega⟩ : Fin pb.length) = ⟨2, by omega⟩ from Fin.ext (show R - 1 + 2 - R + 1 = 2 by omega)] have hpb0 := hpb_act.2 0 (by omega) rw [show (⟨0 + 1, by omega⟩ : Fin pb.length) = ⟨1, by omega⟩ from rfl, show (⟨0 + 2, by omega⟩ : Fin pb.length) = ⟨2, by omega⟩ from rfl] at hpb0 rw [hpb_get_0] at hpb0 exact hpb0 · have hiL : R ≤ i := by omega have hi1L : R ≤ i + 1 := by omega have hi2L : R ≤ i + 2 := by omega have hi_lt : i < p.length := by rw [hp_len_eq]; omega have hi1_lt : i + 1 < p.length := by rw [hp_len_eq]; omega have hi2_lt : i + 2 < p.length := by rw [hp_len_eq]; exact hi rw [hp_R i hiL hi_lt, hp_R (i + 1) hi1L hi1_lt, hp_R (i + 2) hi2L hi2_lt] have hjlen : (i - R + 1) + 2 < pb.length := by omega have hpbcoll := hpb_act.2 (i - R + 1) hjlen rw [show (⟨(i - R + 1) + 1, by omega⟩ : Fin pb.length) = ⟨(i + 1) - R + 1, by omega⟩ from Fin.ext (show (i-R+1)+1 = (i+1)-R+1 by omega), show (⟨(i - R + 1) + 2, hjlen⟩ : Fin pb.length) = ⟨(i + 2) - R + 1, by omega⟩ from Fin.ext (show (i-R+1)+2 = (i+2)-R+1 by omega)] at hpbcoll exact hpbcoll
    Causalean.Graph.DAG.chain_join_active · Causalean/Graph/DSep/OrderedLocalSG/PathJoining.lean:30
  • node_isAncestor_last_of_directed theorem — In a finite directed acyclic graph, consider a walk, its endpoint, and a selected position. If the walk is nontrivial, has the stated endpoint, follows forward directed edges, and the position lies on the walk, then the selected vertex is either the endpoint or its proper ancestor.
    hypotheses
    V :
    Type u_1
    shared
    G :
    DAG V
    shared
    q :
    List V
    w :
    V
    hlen :
    q.length ≥ 2
    hlast :
    q.getLast? = some w
    hedge :
    ∀ (i : ℕ) (hi : i + 1 < q.length), G.edge (q.get ⟨i, by omega⟩) (q.get ⟨i + 1, hi⟩)
    j :
    ℕ
    hj :
    j < q.length
    conclusion
    G.isAncestor (q.get ⟨j, hj⟩) w ∨ q.get ⟨j, hj⟩ = w
    Proof (Lean source)
    theorem node_isAncestor_last_of_directed {q : List V} {w : V} (hlen : q.length ≥ 2) (hlast : q.getLast? = some w) (hedge : ∀ (i : ℕ) (hi : i + 1 < q.length), G.edge (q.get ⟨i, by omega⟩) (q.get ⟨i + 1, hi⟩)) (j : ℕ) (hj : j < q.length) : G.isAncestor (q.get ⟨j, hj⟩) w ∨ q.get ⟨j, hj⟩ = w := by by_cases hjlast : j = q.length - 1 · right have hqne : q ≠ [] := by intro h; rw [h] at hlen; simp at hlen have hh := getLast?_eq_some_getLast hqne rw [hlast] at hh have hw_eq : q.getLast hqne = w := Option.some_inj.mp hh.symm have hidx : (⟨j, hj⟩ : Fin q.length) = ⟨q.length - 1, by omega⟩ := Fin.ext (by omega) rw [hidx, List.get_eq_getElem, ← hw_eq, List.getLast_eq_getElem] · have hj1 : j + 1 < q.length := by omega have he := hedge j hj1 rcases node_isAncestor_last_of_directed hlen hlast hedge (j + 1) hj1 with h | h · exact inl (G.isAncestor_trans (isAncestor.edge he) h) · exact inl (h ▸ isAncestor.edge he) termination_by q.length - j decreasing_by omega
    Causalean.Graph.DAG.node_isAncestor_last_of_directed · Causalean/Graph/DSep/OrderedLocalSG/PathJoining.lean:216
  • isActiveWalk_take theorem — In a finite directed acyclic graph, a conditioning set, walk, and prefix length with an active full walk have an active prefix.
    hypotheses
    V :
    Type u_1
    shared
    G :
    DAG V
    shared
    Z :
    Finset V
    p :
    List V
    k :
    ℕ
    hact :
    G.IsActiveWalk Z p
    conclusion
    G.IsActiveWalk Z (p.take k)
    Proof (Lean source)
    theorem isActiveWalk_take {Z : Finset V} {p : List V} {k : ℕ} (hact : G.IsActiveWalk Z p) : G.IsActiveWalk Z (p.take k) := by obtain ⟨hadj, hcoll⟩ := hact have hle : (p.take k).length ≤ p.length := by rw [List.length_take]; exact min_le_right k p.length have hget : ∀ (j : ℕ) (hj : j < (p.take k).length), (p.take k).get ⟨j, hj⟩ = p.get ⟨j, by omega⟩ := by intro j hj simp only [List.get_eq_getElem, List.getElem_take] refine ⟨fun i hi => ?_, fun i hi => ?_⟩ · rw [hget i (by omega), hget (i + 1) hi] exact hadj i (by omega) · rw [hget i (by omega), hget (i + 1) (by omega), hget (i + 2) hi] exact hcoll i (by omega)
    Causalean.Graph.DAG.isActiveWalk_take · Causalean/Graph/DSep/OrderedLocalSG/PathJoining.lean:290
Path­Surgery 1 core · 6 supporting This file proves the d-separation and active-walk transformations used when the ordered-local induction removes a topologically maximal vertex. ★ dSep_erase_maximal_random_condition

Walk surgery for the ordered-local peel

This file proves the d-separation and active-walk transformations used when the ordered-local induction removes a topologically maximal vertex. The results cover parent inheritance, erasing a maximal random conditioning vertex, changing a walk's conditioning set, orienting its final edge, and joining walks at a conditioned collider.

theorem dSep_erase_maximal_random_condition reviewed
Causalean.Graph.DAG

For a finite directed acyclic graph, two endpoint sets, random and fixed conditioning sets, and a selected vertex, if the vertex belongs to the random conditioning set, it is topologically maximal in the ancestral closure of the query, and the endpoint sets are d-separated by the full conditioning set, then erasing that vertex from the random conditioning set preserves the d-separation.

Formal statement
hypotheses
V :
Type u_1
shared
G :
DAG V
shared
X Y Zr Zf :
Finset V
n :
V
hnZr :
n ∈ Zr
hmax :
∀ m ∈ G.ancestralSet (X ∪ Y ∪ Zr ∪ Zf), G.topoOrder m ≤ G.topoOrder n
hdSep :
G.dSep X Y (Zr ∪ Zf)
conclusion
G.dSep X Y ((Zr.erase n) ∪ Zf)
Proof (Lean source)
theorem dSep_erase_maximal_random_condition {X Y Zr Zf : Finset V} {n : V} (hnZr : n ∈ Zr) (hmax : ∀ m ∈ G.ancestralSet (X ∪ Y ∪ Zr ∪ Zf), G.topoOrder m ≤ G.topoOrder n) (hdSep : G.dSep X Y (Zr ∪ Zf)) : G.dSep X Y ((Zr.erase n) ∪ Zf) := by refine ⟨hdSep.1, ?_, ?_, ?_⟩ · exact hdSep.2.1.mono_right (by intro z hz simp only [mem_union, Finset.mem_erase] at hz ⊢ rcases hz with hz | hz · exact inl hz.2 · exact inr hz) · exact hdSep.2.2.1.mono_right (by intro z hz simp only [mem_union, Finset.mem_erase] at hz ⊢ rcases hz with hz | hz · exact inl hz.2 · exact inr hz) rw [Finset.disjoint_left] intro y hyReach hyY -- Active walk `p : x → y` given `Z' ∪ Zf`. rw [G.bbReachableVertices_iff_activeWalk] at hyReach obtain ⟨x, hxX, p, hlen, hact, hhead, hlast⟩ := hyReach -- Every node of `p` lies in `ancestralSet Q` (Q = X∪Y∪Zr∪Zf). have hpAnc : ∀ v ∈ p, v ∈ G.ancestralSet (X ∪ Y ∪ Zr ∪ Zf) := by intro v hv have := G.activeWalk_nodes_are_ancestors hxX hyY hact hhead hlast v hv refine G.ancestralSet_mono ?_ this intro z hz simp only [mem_union, Finset.mem_erase] at hz ⊢ rcases hz with (h | h) | h | h exacts [inl (inl (inl h)), inl (inl (inr h)), inl (inr h.2), inr h] -- `n` is never a non-collider on `p` (it would force a strictly-larger node). have hno : ∀ (i : ℕ) (hi : i + 2 < p.length), p.get ⟨i + 1, by omega⟩ = n → G.IsCollider (p.get ⟨i, by omega⟩) (p.get ⟨i + 1, by omega⟩) (p.get ⟨i + 2, hi⟩) := by intro i hi hmn by_contra hC obtain ⟨hadj, _⟩ := hact have hadj_lm := hadj i (by omega) have hadj_mr := hadj (i + 1) (by omega) -- Outgoing edge from `m = n` to a path neighbour. have hout := G.nonCollider_has_outgoing hadj_lm hadj_mr hC rcases hout with hedge | hedge <;> rw [hmn] at hedge · have hAnc := hpAnc _ (List.get_mem p ⟨i, by omega⟩) have h1 : G.topoOrder (p.get ⟨i, by omega⟩) ≤ G.topoOrder n := hmax _ hAnc have h2 := G.isAncestor_topoOrder_lt (isAncestor.edge hedge) omega · have hAnc := hpAnc _ (List.get_mem p ⟨i + 1 + 1, by omega⟩) have h1 : G.topoOrder (p.get ⟨i + 1 + 1, by omega⟩) ≤ G.topoOrder n := hmax _ hAnc have h2 := G.isAncestor_topoOrder_lt (isAncestor.edge hedge) omega -- Hence `p` is active given `insert n (Z' ∪ Zf) = Zr ∪ Zf`, contradicting `hdSep`. have hact' : G.IsActiveWalk (insert n (Zr.erase n ∪ Zf)) p := G.isActiveWalk_insert_cond hact hno have hins : insert n (Zr.erase n ∪ Zf) = Zr ∪ Zf := by ext z; simp only [Finset.mem_insert, mem_union, Finset.mem_erase] constructor · rintro (rfl | (⟨_, h⟩ | h) ) exacts [inl hnZr, inl h, inr h] · rintro (h | h) · by_cases hz : z = n · exact inl hz · exact inr (inl ⟨hz, h⟩) · exact inr (inr h) rw [hins] at hact' have : y ∈ G.bbReachableVertices (Zr ∪ Zf) X := by rw [G.bbReachableVertices_iff_activeWalk] exact ⟨x, hxX, p, hlen, hact', hhead, hlast⟩ exact (Finset.disjoint_left.mp hdSep.2.2.2 this) hyY
Causalean.Graph.DAG.dSep_erase_maximal_random_condition · Causalean/Graph/DSep/OrderedLocalSG/PathSurgery.lean:132 · uses DAG , ancestralSet , dSep , topoOrder
6 supporting declarations (lemmas, instances)
  • parents_disjoint_of_dSep_singleton theorem — In a finite directed acyclic graph, if a vertex, target set, and conditioning set satisfy d-separation of the vertex from the target, then the vertex's parents are disjoint from the target set.
    hypotheses
    V :
    Type u_1
    shared
    G :
    DAG V
    shared
    n :
    V
    Y D :
    Finset V
    hdSep :
    G.dSep {n} Y D
    conclusion
    Disjoint (G.parents n) Y
    Proof (Lean source)
    theorem parents_disjoint_of_dSep_singleton {n : V} {Y D : Finset V} (hdSep : G.dSep {n} Y D) : Disjoint (G.parents n) Y := by rw [Finset.disjoint_left] intro a haPar haY -- The walk `[n, a]` is active given `D` (no interior vertex), from `n` to `a ∈ Y`. have hedge : G.edge a n := G.mem_parents.mp haPar have hact : G.IsActiveWalk D [n, a] := by refine ⟨fun i hi => ?_, fun i hi => ?_⟩ · -- length 2 ⟹ i = 0; the only adjacency is `UAdj n a`, from `edge a n`. have hi0 : i = 0 := by simp at hi; omega subst hi0 exact inr (by simpa using hedge) · -- length 2 ⟹ no interior triple simp only [List.length_cons, List.length_nil] at hi omega have hmem : a ∈ G.bbReachableVertices D {n} := by rw [G.bbReachableVertices_iff_activeWalk] exact ⟨n, mem_singleton_self n, [n, a], by simp, hact, rfl, rfl⟩ exact (Finset.disjoint_left.mp hdSep.2.2.2 hmem) haY
    Causalean.Graph.DAG.parents_disjoint_of_dSep_singleton · Causalean/Graph/DSep/OrderedLocalSG/PathSurgery.lean:33
  • dSep_parents_of_maximal_source theorem — In a finite directed acyclic graph, consider a source vertex, target set, conditioning set, and selected parent set. If the source is d-separated from the target, every selected vertex is a parent of the source, and none is conditioned on, then the selected parents are d-separated from the target under the same conditioning set.
    hypotheses
    V :
    Type u_1
    shared
    G :
    DAG V
    shared
    n :
    V
    Y D A0 :
    Finset V
    hdSep :
    G.dSep {n} Y D
    hA0_par :
    ∀ a ∈ A0, G.edge a n
    hA0_D :
    ∀ a ∈ A0, a ∉ D
    conclusion
    G.dSep A0 Y D
    Proof (Lean source)
    theorem dSep_parents_of_maximal_source {n : V} {Y D A0 : Finset V} (hdSep : G.dSep {n} Y D) (hA0_par : ∀ a ∈ A0, G.edge a n) (hA0_D : ∀ a ∈ A0, a ∉ D) : G.dSep A0 Y D := by refine ⟨?_, ?_, hdSep.2.2.1, ?_⟩ · exact (G.parents_disjoint_of_dSep_singleton hdSep).mono_left (by intro a ha exact G.mem_parents.mpr (hA0_par a ha)) · exact Finset.disjoint_left.mpr hA0_D rw [Finset.disjoint_left] intro y hyReach hyY -- Extract an active walk `a → … → y` for some `a ∈ A0`. rw [G.bbReachableVertices_iff_activeWalk] at hyReach obtain ⟨a, haA0, p, hlen, hact, hhead, hlast⟩ := hyReach -- `p` has length ≥ 2 and head `a`, so `p = a :: u :: r`. obtain ⟨u, r, hp⟩ : ∃ u r, p = a :: u :: r := by match p, hlen, hhead with | _ :: u :: r, _, hhead => exact ⟨u, r, by simp only [List.head?_cons, Option.some_inj] at hhead; subst hhead; rfl⟩ subst hp -- Prepend `n` via the edge `a → n`; `a` is a non-collider in `(n, a, u)`. have hedge : G.edge a n := hA0_par a haA0 have hnotcoll : ¬ G.IsCollider n a u := fun hC => G.asymm hedge hC.1 have htri : (if G.IsCollider n a u then a ∈ G.bbZAncestors D else a ∉ D) := by rw [if_neg hnotcoll]; exact hA0_D a haA0 have hact' : G.IsActiveWalk D (n :: a :: u :: r) := G.isActiveWalk_cons_of_active_triple (inr hedge) htri hact -- This new active walk witnesses `y ∈ bbReachableVertices D {n}`, contradiction. have hyReach' : y ∈ G.bbReachableVertices D {n} := by rw [G.bbReachableVertices_iff_activeWalk] refine ⟨n, mem_singleton_self n, n :: a :: u :: r, by simp, hact', rfl, ?_⟩ simpa using hlast exact (Finset.disjoint_left.mp hdSep.2.2.2 hyReach') hyY
    Causalean.Graph.DAG.dSep_parents_of_maximal_source · Causalean/Graph/DSep/OrderedLocalSG/PathSurgery.lean:57
  • isActiveWalk_insert_cond theorem — In a finite directed acyclic graph, consider a conditioning set, walk, and added vertex. If the walk is active and the added vertex can occur internally only as a collider, then the walk remains active after that vertex is added to the conditioning set.
    hypotheses
    V :
    Type u_1
    shared
    G :
    DAG V
    shared
    D :
    Finset V
    p :
    List V
    n :
    V
    hact :
    G.IsActiveWalk D p
    hno :
    ∀ (i : ℕ) (hi : i + 2 < p.length)
    if
    p.get ⟨i + 1, by omega⟩ = n
    then
    G.IsCollider (p.get ⟨i, by omega⟩) (p.get ⟨i + 1, by omega⟩) (p.get ⟨i + 2, hi⟩)
    conclusion
    G.IsActiveWalk (insert n D) p
    Proof (Lean source)
    theorem isActiveWalk_insert_cond {D : Finset V} {p : List V} {n : V} (hact : G.IsActiveWalk D p) (hno : ∀ (i : ℕ) (hi : i + 2 < p.length), p.get ⟨i + 1, by omega⟩ = n → G.IsCollider (p.get ⟨i, by omega⟩) (p.get ⟨i + 1, by omega⟩) (p.get ⟨i + 2, hi⟩)) : G.IsActiveWalk (insert n D) p := by obtain ⟨hadj, hcoll⟩ := hact refine ⟨hadj, fun i hi => ?_⟩ have hval := hcoll i hi simp only at hval ⊢ set l := p.get ⟨i, by omega⟩ set m := p.get ⟨i + 1, by omega⟩ set r := p.get ⟨i + 2, hi⟩ by_cases hC : G.IsCollider l m r · rw [if_pos hC] at hval ⊢ exact (G.ancestralSet_mono (Finset.subset_insert n D)) hval · rw [if_neg hC] at hval ⊢ rw [Finset.mem_insert, not_or] refine ⟨fun hmn => hC (hno i hi hmn), hval⟩
    Causalean.Graph.DAG.isActiveWalk_insert_cond · Causalean/Graph/DSep/OrderedLocalSG/PathSurgery.lean:102
  • lift_crosscond_to_insert theorem — In a finite directed acyclic graph, consider conditioning sets, a walk, and an added vertex. If the walk is active under both sets, every interior collider is activated by the first set, and the added vertex can occur internally only as a collider, then the walk is active when only the first set and added vertex are conditioned on.
    hypotheses
    V :
    Type u_1
    shared
    G :
    DAG V
    shared
    S W :
    Finset V
    p :
    List V
    n :
    V
    hact :
    G.IsActiveWalk (S ∪ W) p
    hcollS :
    ∀ (i : ℕ) (hi : i + 2 < p.length)
    if
    G.IsCollider (p.get ⟨i, by omega⟩) (p.get ⟨i + 1, by omega⟩) (p.get ⟨i + 2, hi⟩)
    then
    p.get ⟨i + 1, by omega⟩ ∈ G.ancestralSet S
    hno_n :
    ∀ (i : ℕ) (hi : i + 2 < p.length)
    if
    p.get ⟨i + 1, by omega⟩ = n
    then
    G.IsCollider (p.get ⟨i, by omega⟩) (p.get ⟨i + 1, by omega⟩) (p.get ⟨i + 2, hi⟩)
    conclusion
    G.IsActiveWalk (insert n S) p
    Proof (Lean source)
    theorem lift_crosscond_to_insert {S W : Finset V} {p : List V} {n : V} (hact : G.IsActiveWalk (S ∪ W) p) (hcollS : ∀ (i : ℕ) (hi : i + 2 < p.length), G.IsCollider (p.get ⟨i, by omega⟩) (p.get ⟨i + 1, by omega⟩) (p.get ⟨i + 2, hi⟩) → p.get ⟨i + 1, by omega⟩ ∈ G.ancestralSet S) (hno_n : ∀ (i : ℕ) (hi : i + 2 < p.length), p.get ⟨i + 1, by omega⟩ = n → G.IsCollider (p.get ⟨i, by omega⟩) (p.get ⟨i + 1, by omega⟩) (p.get ⟨i + 2, hi⟩)) : G.IsActiveWalk (insert n S) p := by obtain ⟨hadj, hcoll⟩ := hact refine ⟨hadj, fun i hi => ?_⟩ have hval := hcoll i hi simp only at hval ⊢ set l := p.get ⟨i, by omega⟩ with hl set m := p.get ⟨i + 1, by omega⟩ with hm set r := p.get ⟨i + 2, hi⟩ with hr by_cases hC : G.IsCollider l m r · rw [if_pos hC] at hval ⊢ show m ∈ G.bbZAncestors (insert n S) exact (G.ancestralSet_mono (Finset.subset_insert n S)) (hcollS i hi hC) · rw [if_neg hC] at hval ⊢ rw [Finset.mem_insert, not_or] refine ⟨fun hmn => hC (hno_n i hi hmn), fun hmS => hval (mem_union_left _ hmS)⟩
    Causalean.Graph.DAG.lift_crosscond_to_insert · Causalean/Graph/DSep/OrderedLocalSG/PathSurgery.lean:220
  • last_edge_into_max theorem — In a finite directed acyclic graph, consider a conditioning set, ancestral seed, active walk, and selected endpoint. If the walk is nontrivial, is active, ends at the selected vertex, lies in the seed's ancestral closure, and the endpoint maximizes topological order there, then the walk's final edge points into that endpoint.
    hypotheses
    V :
    Type u_1
    shared
    G :
    DAG V
    shared
    D bigQ :
    Finset V
    p :
    List V
    n :
    V
    hp_len :
    p.length ≥ 2
    hact :
    G.IsActiveWalk D p
    hlast :
    p.getLast? = some n
    hpAnc :
    ∀ v ∈ p, v ∈ G.ancestralSet bigQ
    hmax :
    ∀ m ∈ G.ancestralSet bigQ, G.topoOrder m ≤ G.topoOrder n
    conclusion
    G.edge (p.get ⟨p.length - 2, by omega⟩) n
    Proof (Lean source)
    theorem last_edge_into_max {D bigQ : Finset V} {p : List V} {n : V} (hp_len : p.length ≥ 2) (hact : G.IsActiveWalk D p) (hlast : p.getLast? = some n) (hpAnc : ∀ v ∈ p, v ∈ G.ancestralSet bigQ) (hmax : ∀ m ∈ G.ancestralSet bigQ, G.topoOrder m ≤ G.topoOrder n) : G.edge (p.get ⟨p.length - 2, by omega⟩) n := by -- The last adjacency is between `p[len-2]` and `p[len-1] = n`. have hadj := hact.1 (p.length - 2) (by omega) have hlast_get : p.get ⟨p.length - 2 + 1, by omega⟩ = n := by have hpne : p ≠ [] := by intro h; rw [h] at hp_len; simp at hp_len have h := getLast?_eq_some_getLast hpne rw [hlast] at h have hn_eq : p.getLast hpne = n := Option.some_inj.mp h.symm have hidx : (⟨p.length - 2 + 1, by omega⟩ : Fin p.length) = ⟨p.length - 1, by omega⟩ := Fin.ext (show p.length - 2 + 1 = p.length - 1 by omega) rw [hidx, List.get_eq_getElem, ← hn_eq, List.getLast_eq_getElem] rw [hlast_get] at hadj -- `hadj : UAdj p[len-2] n`. Rule out `edge n p[len-2]` by topo-maximality. rcases hadj with hin | hout · exact hin · exfalso have hAnc := hpAnc _ (List.get_mem p ⟨p.length - 2, by omega⟩) have h1 : G.topoOrder (p.get ⟨p.length - 2, by omega⟩) ≤ G.topoOrder n := hmax _ hAnc have h2 := G.isAncestor_topoOrder_lt (isAncestor.edge hout) omega
    Causalean.Graph.DAG.last_edge_into_max · Causalean/Graph/DSep/OrderedLocalSG/PathSurgery.lean:249
  • activeWalk_join_at_collider theorem — In a finite directed acyclic graph, consider a conditioning set, joining vertex, endpoints, and two walks. If the first walk is active from the first endpoint to the join, the second is active from the join to the second endpoint, both seam edges point into the join, and the joining vertex is conditioned on, then concatenating the walks gives an active walk between the endpoints.
    hypotheses
    V :
    Type u_1
    shared
    G :
    DAG V
    shared
    Z :
    Finset V
    n x y :
    V
    pa pb :
    List V
    hpa_len :
    pa.length ≥ 2
    hpa_head :
    pa.head? = some x
    hpa_last :
    pa.getLast? = some n
    hpa_act :
    G.IsActiveWalk Z pa
    hpb_len :
    pb.length ≥ 2
    hpb_head :
    pb.head? = some n
    hpb_last :
    pb.getLast? = some y
    hpb_act :
    G.IsActiveWalk Z pb
    hpa_in :
    G.edge (pa.get ⟨pa.length - 2, by omega⟩) n
    hpb_in :
    G.edge (pb.get ⟨1, by omega⟩) n
    hnZ :
    n ∈ Z
    conclusion
    p :
    pa ++ pb.tail
    p.length ≥ 2
    p.head? = some x
    p.getLast? = some y
    G.IsActiveWalk Z p
    Proof (Lean source)
    theorem activeWalk_join_at_collider {Z : Finset V} {n x y : V} {pa pb : List V} (hpa_len : pa.length ≥ 2) (hpa_head : pa.head? = some x) (hpa_last : pa.getLast? = some n) (hpa_act : G.IsActiveWalk Z pa) (hpb_len : pb.length ≥ 2) (hpb_head : pb.head? = some n) (hpb_last : pb.getLast? = some y) (hpb_act : G.IsActiveWalk Z pb) (hpa_in : G.edge (pa.get ⟨pa.length - 2, by omega⟩) n) (hpb_in : G.edge (pb.get ⟨1, by omega⟩) n) (hnZ : n ∈ Z) : let p := pa ++ pb.tail p.length ≥ 2 ∧ p.head? = some x ∧ p.getLast? = some y ∧ G.IsActiveWalk Z p := by have hpa_ne : pa ≠ [] := by intro h; rw [h] at hpa_len; simp at hpa_len have hpb_ne : pb ≠ [] := by intro h; rw [h] at hpb_len; simp at hpb_len -- pb.head = n have hpb_head_eq : pb.head hpb_ne = n := by have h := List.head?_eq_some_head hpb_ne; rw [hpb_head] at h exact (Option.some_inj.mp h.symm) -- pa.getLast = n have hpa_last_eq : pa.getLast hpa_ne = n := by have h := getLast?_eq_some_getLast hpa_ne; rw [hpa_last] at h exact (Option.some_inj.mp h.symm) -- pa.head = x have hpa_head_eq : pa.head hpa_ne = x := by have h := List.head?_eq_some_head hpa_ne; rw [hpa_head] at h exact (Option.some_inj.mp h.symm) -- pb.getLast = y have hpb_last_eq : pb.getLast hpb_ne = y := by have h := getLast?_eq_some_getLast hpb_ne; rw [hpb_last] at h exact (Option.some_inj.mp h.symm) -- pb = n :: pb.tail have hpb_decomp : pb = n :: pb.tail := by conv_lhs => rw [← List.cons_head_tail hpb_ne]; rw [hpb_head_eq] have hpb_tail_len : pb.tail.length = pb.length - 1 := List.length_tail have hpb_tail_ne : pb.tail ≠ [] := by rw [← List.length_pos_iff, hpb_tail_len]; omega set p := pa ++ pb.tail with hp_def set R := pa.length with hR_def have hp_len_eq : p.length = R + pb.tail.length := by simp only [hp_def, List.length_append, ← hR_def] have hp_len : p.length ≥ 2 := by rw [hp_len_eq]; omega have hp_head : p.head? = some x := by have : p.head? = pa.head? := List.head?_append_of_ne_nil _ hpa_ne rw [this, hpa_head] have hp_last : p.getLast? = some y := by have hlast_tail : pb.tail.getLast? = some y := by have heq : pb = [n] ++ pb.tail := by simpa using hpb_decomp have := getLast?_append_of_ne_nil [n] hpb_tail_ne rw [← heq] at this; rw [← this]; exact hpb_last simp only [hp_def, getLast?_append, hlast_tail]; rfl refine ⟨hp_len, hp_head, hp_last, ?_⟩ -- Index translation: p[k] = pa[k] for k < R; p[k] = pb[k-R+1] for k ≥ R. have hp_L : ∀ (k : ℕ) (hkR : k < R), p.get ⟨k, by rw [hp_len_eq]; omega⟩ = pa.get ⟨k, hkR⟩ := by intro k hkR simp only [hp_def, List.get_eq_getElem, List.getElem_append_left (h := hkR)] have hpb_tail_get : ∀ (j : ℕ) (hj1 : j < pb.tail.length) (hj2 : j + 1 < pb.length), pb.tail[j]'hj1 = pb[j + 1]'hj2 := by intro j hj1 hj2 have : pb[j + 1] = (n :: pb.tail)[j + 1]'(by rw [← hpb_decomp]; exact hj2) := by congr 1 rw [this]; simp [List.getElem_cons_succ] have hp_R : ∀ (k : ℕ) (hkL : R ≤ k) (hk : k < p.length), p.get ⟨k, hk⟩ = pb.get ⟨k - R + 1, by rw [hp_len_eq, hpb_tail_len] at hk; omega⟩ := by intro k hkL hk have hk_app : R ≤ k := hkL have htail_idx_lt : k - R < pb.tail.length := by rw [hp_len_eq] at hk; omega have hpget : p.get ⟨k, hk⟩ = pb.tail[k - R]'htail_idx_lt := by simp only [hp_def, List.get_eq_getElem] rw [List.getElem_append_right (by rw [← hR_def]; exact hk_app)] rw [hpget] rw [hpb_tail_get (k - R) htail_idx_lt (by rw [hpb_tail_len] at htail_idx_lt; omega)] simp [List.get_eq_getElem] -- pb[0] = n, pa[R-1] = n. have hpb_get_0 : pb.get ⟨0, by omega⟩ = n := by rw [List.get_eq_getElem, List.getElem_zero]; exact hpb_head_eq have hpa_get_last : pa.get ⟨R - 1, by omega⟩ = n := by rw [List.get_eq_getElem] have := List.getLast_eq_getElem hpa_ne rw [hpa_last_eq] at this rw [← this] refine ⟨?_, ?_⟩ · -- Adjacency. intro i hi rw [hp_len_eq] at hi by_cases hA1 : i + 1 < R · -- Both in pa. have hiR : i < R := by omega rw [hp_L i hiR, hp_L (i + 1) hA1] exact hpa_act.1 i hA1 · push_neg at hA1 by_cases hA2 : i + 1 = R · -- Seam at i = R-1: UAdj(pa[R-1]=n, pb.tail[0]=pb[1]). have hi_eq : i = R - 1 := by omega subst hi_eq have hiR : R - 1 < R := by omega rw [hp_L (R - 1) hiR] have hi1L : R ≤ R - 1 + 1 := by omega have hi1_lt : R - 1 + 1 < p.length := by rw [hp_len_eq]; exact hi rw [hp_R (R - 1 + 1) hi1L hi1_lt] rw [hpa_get_last] have h_yidx : R - 1 + 1 - R + 1 = 1 := by omega rw [show (⟨R - 1 + 1 - R + 1, by rw [hp_len_eq, hpb_tail_len] at hi1_lt; omega⟩ : Fin pb.length) = ⟨1, by omega⟩ from Fin.ext h_yidx] -- UAdj n pb[1] from edge pb[1] → n. exact inr hpb_in · -- Both in pb.tail. i ≥ R. have hiL : R ≤ i := by omega have hi1L : R ≤ i + 1 := by omega have hi_lt : i < p.length := by rw [hp_len_eq]; omega have hi1_lt : i + 1 < p.length := by rw [hp_len_eq]; exact hi rw [hp_R i hiL hi_lt, hp_R (i + 1) hi1L hi1_lt] have hidx : (i - R + 1) + 1 < pb.length := by omega have hadj := hpb_act.1 (i - R + 1) hidx have he : (i - R + 1) + 1 = (i + 1) - R + 1 := by omega rw [show (⟨(i - R + 1) + 1, hidx⟩ : Fin pb.length) = ⟨(i + 1) - R + 1, by omega⟩ from Fin.ext he] at hadj exact hadj · -- Collider condition. intro i hi rw [hp_len_eq] at hi by_cases hC1 : i + 2 < R · -- All three in pa. have hiR : i < R := by omega have hi1R : i + 1 < R := by omega rw [hp_L i hiR, hp_L (i + 1) hi1R, hp_L (i + 2) hC1] exact hpa_act.2 i hC1 · push_neg at hC1 by_cases hC2 : i + 2 = R · -- Seam collider: middle = pa[R-1] = n. Triple (pa[R-2], n, pb[1]). have hi_eq : i = R - 2 := by omega subst hi_eq have hiR : R - 2 < R := by omega have hi1R : R - 2 + 1 < R := by omega have hi2L : R ≤ R - 2 + 2 := by omega have hi2_lt : R - 2 + 2 < p.length := by rw [hp_len_eq]; exact hi rw [hp_L (R - 2) hiR, hp_L (R - 2 + 1) hi1R, hp_R (R - 2 + 2) hi2L hi2_lt] rw [show (⟨R - 2 + 1, by omega⟩ : Fin pa.length) = ⟨R - 1, by omega⟩ from Fin.ext (show R - 2 + 1 = R - 1 by omega)] rw [hpa_get_last] have h_ridx : R - 2 + 2 - R + 1 = 1 := by omega rw [show (⟨R - 2 + 2 - R + 1, by rw [hp_len_eq, hpb_tail_len] at hi2_lt; omega⟩ : Fin pb.length) = ⟨1, by omega⟩ from Fin.ext h_ridx] -- left = pa[R-2]; edge into n is hpa_in (pa[R-2]→n); right = pb[1], edge pb[1]→n. have hLeq : pa.get ⟨R - 2, by omega⟩ = pa.get ⟨pa.length - 2, by omega⟩ := by congr 1 have hColl : G.IsCollider (pa.get ⟨R - 2, by omega⟩) n (pb.get ⟨1, by omega⟩) := by refine ⟨?_, hpb_in⟩ rw [hLeq]; exact hpa_in rw [if_pos hColl] -- n ∈ bbZAncestors Z since n ∈ Z. show n ∈ G.bbZAncestors Z exact G.subset_ancestralSet Z hnZ · by_cases hC3 : i + 1 = R · -- Straddle: middle = pb.tail[0] = pb[1]. Triple (pa[R-1]=n, pb[1], pb[2]) = pb's index 0. have hi_eq : i = R - 1 := by omega subst hi_eq have hiR : R - 1 < R := by omega have hi1L : R ≤ R - 1 + 1 := by omega have hi2L : R ≤ R - 1 + 2 := by omega have hi1_lt : R - 1 + 1 < p.length := by rw [hp_len_eq]; omega have hi2_lt : R - 1 + 2 < p.length := by rw [hp_len_eq]; exact hi rw [hp_L (R - 1) hiR, hp_R (R - 1 + 1) hi1L hi1_lt, hp_R (R - 1 + 2) hi2L hi2_lt] rw [hpa_get_last] rw [show (⟨R - 1 + 1 - R + 1, by omega⟩ : Fin pb.length) = ⟨1, by omega⟩ from Fin.ext (show R - 1 + 1 - R + 1 = 1 by omega)] rw [show (⟨R - 1 + 2 - R + 1, by omega⟩ : Fin pb.length) = ⟨2, by omega⟩ from Fin.ext (show R - 1 + 2 - R + 1 = 2 by omega)] -- This matches pb's collider clause at index 0 (triple pb[0]=n, pb[1], pb[2]). have hpb0 := hpb_act.2 0 (by omega) rw [show (⟨0 + 1, by omega⟩ : Fin pb.length) = ⟨1, by omega⟩ from rfl, show (⟨0 + 2, by omega⟩ : Fin pb.length) = ⟨2, by omega⟩ from rfl] at hpb0 rw [hpb_get_0] at hpb0 exact hpb0 · -- All three in pb.tail. i ≥ R. have hiL : R ≤ i := by omega have hi1L : R ≤ i + 1 := by omega have hi2L : R ≤ i + 2 := by omega have hi_lt : i < p.length := by rw [hp_len_eq]; omega have hi1_lt : i + 1 < p.length := by rw [hp_len_eq]; omega have hi2_lt : i + 2 < p.length := by rw [hp_len_eq]; exact hi rw [hp_R i hiL hi_lt, hp_R (i + 1) hi1L hi1_lt, hp_R (i + 2) hi2L hi2_lt] have hjlen : (i - R + 1) + 2 < pb.length := by omega have hpbcoll := hpb_act.2 (i - R + 1) hjlen rw [show (⟨(i - R + 1) + 1, by omega⟩ : Fin pb.length) = ⟨(i + 1) - R + 1, by omega⟩ from Fin.ext (show (i-R+1)+1 = (i+1)-R+1 by omega), show (⟨(i - R + 1) + 2, hjlen⟩ : Fin pb.length) = ⟨(i + 2) - R + 1, by omega⟩ from Fin.ext (show (i-R+1)+2 = (i+2)-R+1 by omega)] at hpbcoll exact hpbcoll
    Causalean.Graph.DAG.activeWalk_join_at_collider · Causalean/Graph/DSep/OrderedLocalSG/PathSurgery.lean:280