SCM.ID.Density.QFactor

hX :

X ⊆ D

hY :

Y ⊆ D

hZ :

Z ⊆ D

μ :

Measure (ValuesOn D (swigΩ Ω))

StandardBorelSpace (ValuesOn D (swigΩ Ω))

def

KernelObsCondIndepOn D X Y Z hX hY hZ μ :

Prop

given by

CondIndepFun (comap (valuesProjection hZ) inferInstance) (comap_valuesProjection_le hZ) (valuesProjection hX) (valuesProjection hY) μ

Causalean.SCM.ID.KernelObsCondIndepOn · Causalean/SCM/ID/Density/QFactor/Defs.lean:101 · uses SWIGNode , instMeasurableSpaceSwigΩ , swigΩ , ValuesOn

def KernelGlobalMarkovOn reviewed

Causalean.SCM.ID

For a finite node-label set, measurable node-value spaces, a SWIG graph, a finite coordinate set, and a finite measure on its coordinate-value space, the kernel global Markov property means that every three pairwise disjoint coordinate blocks contained in that set which are d-separated in the graph are conditionally independent under the measure, provided the coordinate-value space is standard Borel.

Definition (Lean source)

parameters

N :

Type u_1

N → Type u_2

shared

H :

D :

μ :

Measure (ValuesOn D (swigΩ Ω))

StandardBorelSpace (ValuesOn D (swigΩ Ω))

X Y Z :

hX :

X ⊆ D

hY :

Y ⊆ D

hZ :

Z ⊆ D

Disjoint X Y

Disjoint X Z

Disjoint Y Z

H.dag.dSep X Y Z

def

KernelGlobalMarkovOn H D μ :

Prop

given by

KernelObsCondIndepOn D X Y Z hX hY hZ μ

Causalean.SCM.ID.KernelGlobalMarkovOn · Causalean/SCM/ID/Density/QFactor/Defs.lean:125 · uses SWIGGraph , SWIGNode , instMeasurableSpaceSwigΩ , swigΩ , ValuesOn

def tianPrefixStepDensity reviewed

Causalean.SCM.ID

For a finite node-label set, measurable node-value spaces, a SWIG graph, a finite node set, a finite measure on its value assignments, a family of reference measures, and a position in the graph's ordering of that set, Tian's prefix-step density maps each assignment of the selected nodes to the Radon–Nikodym density of the selected node's conditional distribution given its preceding nodes, relative to its reference measure; the selected node's value space is required to be nonempty and standard Borel.

Definition (Lean source)

parameters

N :

Type u_1

N → Type u_2

shared

G :

D :

μ :

Measure (ValuesOn D (swigΩ Ω))

ref :

i :

Fin D.card

StandardBorelSpace (ValuesOn ({(G.nodesAt D i).val} : Finset (SWIGNode N)) (swigΩ Ω))

Nonempty (ValuesOn ({(G.nodesAt D i).val} : Finset (SWIGNode N)) (swigΩ Ω))

def

tianPrefixStepDensity G D μ ref i :

ValuesOn D (swigΩ Ω) → ENNReal

given by

fun x

=> ((condDistrib (valuesProjection (show ({(G.nodesAt D i).val} : Finset (SWIGNode N)) ⊆ D from by intro v hv rw [Finset.mem_singleton] at hv exact hv ▸ (G.nodesAt D i).property)) (valuesProjection (G.prefixIn_subset D i.val)) μ) (valuesProjection (G.prefixIn_subset D i.val) x)).rnDeriv (jointRef ref ({(G.nodesAt D i).val} : Finset (SWIGNode N))) (valuesProjection (show ({(G.nodesAt D i).val} : Finset (SWIGNode N)) ⊆ D from by intro v hv rw [Finset.mem_singleton] at hv exact hv ▸ (G.nodesAt D i).property) x)

Causalean.SCM.ID.tianPrefixStepDensity · Causalean/SCM/ID/Density/QFactor/Defs.lean:146 · uses SWIGGraph , nodesAt , SWIGNode , instMeasurableSpaceSwigΩ , swigΩ , ValuesOn , ReferenceMeasures

def tianDistrictDensity reviewed

Causalean.SCM.ID

For a finite node-label set, measurable node-value spaces, a SWIG graph, a finite node set, a finite measure on its value assignments, a family of reference measures, and a selected node set, Tian's district density maps each node assignment to the product of the prefix-step densities for exactly those ordered nodes that lie in the selected set; every singleton node-value space in the ordering is required to be nonempty and standard Borel.

Definition (Lean source)

parameters

N :

Type u_1

N → Type u_2

shared

G :

D :

μ :

Measure (ValuesOn D (swigΩ Ω))

ref :

S :

∀ (k : ℕ) (hk : k < D.card),

StandardBorelSpace (ValuesOn ({(G.nodesAt D ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))

∀ (k : ℕ) (hk : k < D.card),

Nonempty (ValuesOn ({(G.nodesAt D ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))

def

tianDistrictDensity G D μ ref S :

ValuesOn D (swigΩ Ω) → ENNReal

given by

fun x

=> ∏ i ∈ Finset.univ.filter (fun i : Fin D.card => (G.nodesAt D i).val ∈ S), tianPrefixStepDensity G D μ ref i x

Causalean.SCM.ID.tianDistrictDensity · Causalean/SCM/ID/Density/QFactor/Defs.lean:185 · uses SWIGGraph , nodesAt , SWIGNode , instMeasurableSpaceSwigΩ , swigΩ , ValuesOn , ReferenceMeasures

def tianDensityProduct reviewed

Causalean.SCM.ID

For a finite node-label set, measurable node-value spaces, a SWIG graph, a finite node set, a finite measure on its value assignments, and a family of reference measures, Tian's full prefix-chain density maps each node assignment to the product of the prefix-step densities for every node in the graph's ordering; every singleton node-value space in that ordering is required to be nonempty and standard Borel.

Definition (Lean source)

parameters

N :

Type u_1

N → Type u_2

shared

G :

D :

μ :

Measure (ValuesOn D (swigΩ Ω))

ref :

∀ (k : ℕ) (hk : k < D.card),

StandardBorelSpace (ValuesOn ({(G.nodesAt D ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))

∀ (k : ℕ) (hk : k < D.card),

Nonempty (ValuesOn ({(G.nodesAt D ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))

def

tianDensityProduct G D μ ref :

ValuesOn D (swigΩ Ω) → ENNReal

given by

fun x => ∏ i : Fin D.card, tianPrefixStepDensity G D μ ref i x

Causalean.SCM.ID.tianDensityProduct · Causalean/SCM/ID/Density/QFactor/Defs.lean:213 · uses SWIGGraph , nodesAt , SWIGNode , instMeasurableSpaceSwigΩ , swigΩ , ValuesOn , ReferenceMeasures

theorem prod_tianDistrictDensity_eq_tianDensityProduct reviewed

Causalean.SCM.ID

For a finite acyclic graph with measurable node-value spaces, a finite node set, evidence that it is exactly the observed set, a finite law on that set, and coordinate reference measures, the full prefix-chain density equals the product of Tian's district densities over all c-components.

Formal statement

hypotheses

N :

Type u_1

N → Type u_2

shared

H :

D :

hD :

H.observed = D

μ :

Measure (ValuesOn D (swigΩ Ω))

ref :

∀ (k : ℕ) (hk : k < D.card),

StandardBorelSpace (ValuesOn ({(H.nodesAt D ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))

∀ (k : ℕ) (hk : k < D.card),

Nonempty (ValuesOn ({(H.nodesAt D ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))

conclusion

(fun x => ∏ S ∈ H.cComponentSet, tianDistrictDensity H D μ ref S x)

= fun x => tianDensityProduct H D μ ref x

Proof (Lean source)

theorem prod_tianDistrictDensity_eq_tianDensityProduct (H : SWIGGraph N) (D : Finset (SWIGNode N)) (hD : H.observed = D) (μ : Measure (ValuesOn D (swigΩ Ω))) (ref : ReferenceMeasures Ω) [IsFiniteMeasure μ] [∀ (k : ℕ) (hk : k < D.card), StandardBorelSpace (ValuesOn ({(H.nodesAt D ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ (k : ℕ) (hk : k < D.card), Nonempty (ValuesOn ({(H.nodesAt D ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] : (fun x => ∏ S ∈ H.cComponentSet, tianDistrictDensity H D μ ref S x) = fun x => tianDensityProduct H D μ ref x := by classical funext x have hmaps : ∀ i ∈ (Finset.univ : Finset (Fin D.card)), H.cComponentOf (H.nodesAt D i).val ∈ H.cComponentSet := by intro i _ exact Finset.mem_image.mpr ⟨(H.nodesAt D i).val, hD.symm ▸ (H.nodesAt D i).property, rfl⟩ unfold tianDensityProduct tianDistrictDensity rw [← Finset.prod_fiberwise_of_maps_to hmaps (fun i => tianPrefixStepDensity H D μ ref i x)] refine Finset.prod_congr rfl ?_ intro S hS refine Finset.prod_congr ?_ (fun i _ => rfl) ext i simp only [mem_filter, Finset.mem_univ, true_and] exact mem_cComponent_iff_cComponentOf_eq H (hD.symm ▸ (H.nodesAt D i).property) hS

Causalean.SCM.ID.prod_tianDistrictDensity_eq_tianDensityProduct · Causalean/SCM/ID/Density/QFactor/Defs.lean:234 · uses SWIGGraph , cComponentSet , nodesAt , SWIGNode , instMeasurableSpaceSwigΩ , swigΩ , ValuesOn , tianDensityProduct , tianDistrictDensity , ReferenceMeasures

1 supporting declaration (lemmas, instances)

prefixIn_obsParentClosed lemma — Topological prefixes of an observed-parent-closed set remain observed-parent-closed.

hypotheses

N :

Type u_1
N → Type u_2
shared

M :

SCM N Ω

X :

Finset N

hObs :

∀ D ∈ X, SWIGNode.random D ∈ M.observed

hFix :

∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed

Y :

Finset (SWIGNode N)

k :

ℕ

conclusion

(M.fixSet X hObs hFix).ObsParentClosed (((M.fixSet X hObs hFix).toSWIGGraph.induce (SCM.ID.fixAncestralSet M X hObs hFix Y)).prefixIn (SCM.ID.fixObservedAncestralSet M X hObs hFix Y) k)

Proof (Lean source)

lemma prefixIn_obsParentClosed (M : SCM N Ω) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (Y : Finset (SWIGNode N)) (k : ℕ) : (M.fixSet X hObs hFix).ObsParentClosed (((M.fixSet X hObs hFix).toSWIGGraph.induce (SCM.ID.fixAncestralSet M X hObs hFix Y)).prefixIn (SCM.ID.fixObservedAncestralSet M X hObs hFix Y) k) := by classical let M' := M.fixSet X hObs hFix let A := SCM.ID.fixAncestralSet M X hObs hFix Y let D := SCM.ID.fixObservedAncestralSet M X hObs hFix Y let H := M'.toSWIGGraph.induce A have hDclosed : M'.ObsParentClosed D := by simpa [M', D] using (SCM.ID.fixObservedAncestralSet_obsParent_closed M X hObs hFix Y) refine ⟨?_, ?_⟩ · intro v hv exact hDclosed.1 (H.prefixIn_subset D k hv) · intro v hv w hwObs hEdge have hvD : v ∈ D := H.prefixIn_subset D k hv have hwD : w ∈ D := hDclosed.2 v hvD w hwObs hEdge rcases Finset.mem_filter.mp hv with ⟨hvD₀, hvIdxLt₀⟩ have hvIdxLt : (H.nodeIndex D ⟨v, hvD⟩).val < k := by have hsub : (⟨v, hvD⟩ : {v // v ∈ D}) = ⟨v, hvD₀⟩ := Subtype.ext rfl simpa [SWIGGraph.prefixIn, hsub, hvD₀] using hvIdxLt₀ have hEdgeH : H.dag.edge w v := by have hwA : w ∈ A := (Finset.mem_inter.mp hwD).1 have hvA : v ∈ A := (Finset.mem_inter.mp hvD).1 have hvObs : v ∈ M'.observed := hDclosed.1 hvD dsimp [H, M', A, SWIGGraph.induce, SWIGGraph.inducedDag, SWIGGraph.inducedEdge] refine ⟨hEdge, ?_, ?_⟩ · exact mem_union_left _ (mem_union_right _ (Finset.mem_inter.mpr ⟨hwA, hwObs⟩)) · exact mem_union_left _ (mem_union_right _ (Finset.mem_inter.mpr ⟨hvA, hvObs⟩)) have hTopo : H.dag.topoOrder w < H.dag.topoOrder v := H.dag.topoOrder_lt w v hEdgeH letI := H.topoLinearOrder have hSubtypeLt : (⟨w, hwD⟩ : {v // v ∈ D}) < ⟨v, hvD⟩ := by change H.dag.topoOrder w < H.dag.topoOrder v exact hTopo have hIndexLt : (H.nodeIndex D ⟨w, hwD⟩).val < (H.nodeIndex D ⟨v, hvD⟩).val := by have hIndexLtFin : H.nodeIndex D ⟨w, hwD⟩ < H.nodeIndex D ⟨v, hvD⟩ := by simpa [SWIGGraph.nodeIndex] using ((D.orderIsoOfFin rfl).symm.strictMono hSubtypeLt) simpa [SWIGGraph.nodeIndex] using hIndexLtFin change w ∈ D.filter (fun v => if h : v ∈ D then (H.nodeIndex D ⟨v, h⟩).val < k else False) exact Finset.mem_filter.mpr ⟨hwD, by simpa [hwD] using lt_trans hIndexLt hvIdxLt⟩

Causalean.SWIGGraph.prefixIn_obsParentClosed · Causalean/SCM/ID/Density/QFactor/Defs.lean:38

PrefixLemmas 1 core · 12 supporting This file proves the topological-prefix closure and component-intersection facts needed to factor qLocalMass along successive prefixes. ★ qLocalMass_prefixIn_eq_prod_induce_components

Prefix and component lemmas for q-factor recovery

This file proves the topological-prefix closure and component-intersection facts needed to factor qLocalMass along successive prefixes. It also provides the fixed-edge fact used when the ambient model is replaced by a do-model.

lemma qLocalMass_prefixIn_eq_prod_induce_components reviewed

Causalean.SCM.ID

For a finite structural causal model with finite measurable node-value spaces, a fixed-node assignment, an observed node set, evidence that it is observed, a prefix length, and an observed realization, the local q-mass of the induced graph's prefix factors into the local q-masses of its intersections with the induced c-components.

Formal statement

hypotheses

N :

Type u_1

N → Type u_2

shared

∀ n, Fintype (Ω n)

∀ n, MeasurableSingletonClass (Ω n)

M :

SCM N Ω

s :

M.FixedValues

A :

hA :

A ⊆ M.observed

k :

ℕ

x :

ValuesOn M.observed (swigΩ Ω)

conclusion

H :

M.toSWIGGraph.induce A

M.qLocalMass s (H.prefixIn A k) (fun _ hv => hA (H.prefixIn_subset A k hv)) x

= ∏ C ∈ H.cComponentSet, M.qLocalMass s (C ∩ H.prefixIn A k) (fun _ hv => hA (H.prefixIn_subset A k (mem_of_mem_inter_right hv))) x

Proof (Lean source)

lemma qLocalMass_prefixIn_eq_prod_induce_components [∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)] (M : SCM N Ω) (s : M.FixedValues) (A : Finset (SWIGNode N)) (hA : A ⊆ M.observed) (k : ℕ) (x : ValuesOn M.observed (swigΩ Ω)) : let H := M.toSWIGGraph.induce A M.qLocalMass s (H.prefixIn A k) (fun _ hv => hA (H.prefixIn_subset A k hv)) x = ∏ C ∈ H.cComponentSet, M.qLocalMass s (C ∩ H.prefixIn A k) (fun _ hv => hA (H.prefixIn_subset A k (mem_of_mem_inter_right hv))) x := by classical let H := M.toSWIGGraph.induce A have hHobs : H.observed = A := by simp [H, SWIGGraph.induce, Finset.inter_eq_left.mpr hA] have h𝒞obs : ∀ U ∈ H.cComponentSet, U ⊆ M.observed := by intro U hU v hv exact hA (hHobs ▸ H.cComponentSet_subset_observed U hU hv) have hcover : H.prefixIn A k ⊆ H.cComponentSet.sup id := by intro v hv have hvObs : v ∈ H.observed := by rw [hHobs] exact H.prefixIn_subset A k hv rw [Finset.mem_sup] exact ⟨H.cComponentOf v, (by rw [SWIGGraph.cComponentSet, mem_image] exact ⟨v, hvObs, rfl⟩), H.mem_cComponentOf_self hvObs⟩ have hblock : (↑H.cComponentSet : Set (Finset (SWIGNode N))).Pairwise (fun U U' => Disjoint (M.latentBlock U) (M.latentBlock U')) := by intro U hU V hV hne exact latentBlock_pairwise_disjoint_induce_components M A hU hV hne have hfac := M.qLocalMass_prod_inter_of_latentBlock_disjoint s (H.prefixIn A k) (fun _ hv => hA (H.prefixIn_subset A k hv)) H.cComponentSet h𝒞obs hcover hblock x calc M.qLocalMass s (H.prefixIn A k) (fun _ hv => hA (H.prefixIn_subset A k hv)) x = ∏ C ∈ H.cComponentSet, if hC : C ∈ H.cComponentSet then M.qLocalMass s (C ∩ H.prefixIn A k) (fun _ hv => h𝒞obs C hC (mem_of_mem_inter_left hv)) x else 1 := by simpa [H] using hfac _ = ∏ C ∈ H.cComponentSet, M.qLocalMass s (C ∩ H.prefixIn A k) (fun _ hv => hA (H.prefixIn_subset A k (mem_of_mem_inter_right hv))) x := by refine Finset.prod_congr rfl ?_ intro C hC simp [hC]

Causalean.SCM.ID.qLocalMass_prefixIn_eq_prod_induce_components · Causalean/SCM/ID/Density/QFactor/PrefixLemmas.lean:178 · uses SWIGGraph , cComponentSet , induce , prefixIn , prefixIn_subset , SWIGNode , instDecidableEqSWIGNode , swigΩ , ValuesOn , SCM , FixedValues , qLocalMass

12 supporting declarations (lemmas, instances)

mem_prefixIn_iff lemma — Membership in a graph-ordered prefix of D is exactly index membership below the prefix length.

hypotheses

N :

Type u_1
shared

H :

SWIGGraph N

D :

Finset (SWIGNode N)

n :

ℕ

v :

SWIGNode N

conclusion

v ∈ H.prefixIn D n ↔ ∃ h : v ∈ D, (H.nodeIndex D ⟨v, h⟩).val < n

Proof (Lean source)

lemma mem_prefixIn_iff (H : SWIGGraph N) (D : Finset (SWIGNode N)) (n : ℕ) (v : SWIGNode N) : v ∈ H.prefixIn D n ↔ ∃ h : v ∈ D, (H.nodeIndex D ⟨v, h⟩).val < n := by unfold SWIGGraph.prefixIn constructor · intro hv rcases Finset.mem_filter.mp hv with ⟨hD, hltif⟩ exact ⟨hD, by simpa [hD] using hltif⟩ · rintro ⟨hD, hlt⟩ exact Finset.mem_filter.mpr ⟨hD, by simpa [hD] using hlt⟩

Causalean.SCM.ID.mem_prefixIn_iff · Causalean/SCM/ID/Density/QFactor/PrefixLemmas.lean:39
prefixIn_zero lemma — The D-prefix of length zero is empty.

hypotheses

N :

Type u_1
shared

H :

SWIGGraph N

D :

Finset (SWIGNode N)

conclusion

H.prefixIn D 0 = ∅

Proof (Lean source)

lemma prefixIn_zero (H : SWIGGraph N) (D : Finset (SWIGNode N)) : H.prefixIn D 0 = ∅ := by ext v constructor · intro hv rcases (mem_prefixIn_iff H D 0 v).mp hv with ⟨_, hlt⟩ omega · simp

Causalean.SCM.ID.prefixIn_zero · Causalean/SCM/ID/Density/QFactor/PrefixLemmas.lean:53
nodesAt_mem_prefixIn_iff lemma — The node at index i belongs to the first n D-nodes iff i < n.

hypotheses

N :

Type u_1
shared

H :

SWIGGraph N

D :

Finset (SWIGNode N)

n :

ℕ

i :

Fin D.card

conclusion

(H.nodesAt D i).val ∈ H.prefixIn D n ↔ i.val < n

Proof (Lean source)

lemma nodesAt_mem_prefixIn_iff (H : SWIGGraph N) (D : Finset (SWIGNode N)) (n : ℕ) (i : Fin D.card) : (H.nodesAt D i).val ∈ H.prefixIn D n ↔ i.val < n := by rw [mem_prefixIn_iff] constructor · rintro ⟨hD, hlt⟩ have hidx : H.nodeIndex D ⟨(H.nodesAt D i).val, hD⟩ = i := by have hsub : (⟨(H.nodesAt D i).val, hD⟩ : {v // v ∈ D}) = H.nodesAt D i := Subtype.ext rfl rw [hsub] simp [SWIGGraph.nodeIndex, SWIGGraph.nodesAt] rwa [hidx] at hlt · intro hlt exact ⟨(H.nodesAt D i).property, by have hidx : H.nodeIndex D (H.nodesAt D i) = i := by simp [SWIGGraph.nodeIndex, SWIGGraph.nodesAt] simpa [hidx] using hlt⟩

Causalean.SCM.ID.nodesAt_mem_prefixIn_iff · Causalean/SCM/ID/Density/QFactor/PrefixLemmas.lean:63
prefixIn_card lemma — The full D-prefix is D.

hypotheses

N :

Type u_1
shared

H :

SWIGGraph N

D :

Finset (SWIGNode N)

conclusion

H.prefixIn D D.card = D

Proof (Lean source)

lemma prefixIn_card (H : SWIGGraph N) (D : Finset (SWIGNode N)) : H.prefixIn D D.card = D := by ext v constructor · exact fun hv => H.prefixIn_subset D D.card hv · intro hv exact (mem_prefixIn_iff H D D.card v).mpr ⟨hv, (H.nodeIndex D ⟨v, hv⟩).isLt⟩

Causalean.SCM.ID.prefixIn_card · Causalean/SCM/ID/Density/QFactor/PrefixLemmas.lean:84
prefixIn_mono lemma — Prefix sets are monotone in the prefix length.

hypotheses

N :

Type u_1
shared

H :

SWIGGraph N

D :

Finset (SWIGNode N)

m k :

ℕ

h :

m ≤ k

conclusion

H.prefixIn D m ⊆ H.prefixIn D k

Proof (Lean source)

lemma prefixIn_mono (H : SWIGGraph N) (D : Finset (SWIGNode N)) {m k : ℕ} (h : m ≤ k) : H.prefixIn D m ⊆ H.prefixIn D k := by intro v hv rcases (mem_prefixIn_iff H D m v).mp hv with ⟨hD, hlt⟩ exact (mem_prefixIn_iff H D k v).mpr ⟨hD, lt_of_lt_of_le hlt h⟩

Causalean.SCM.ID.prefixIn_mono · Causalean/SCM/ID/Density/QFactor/PrefixLemmas.lean:94
nodesAt_not_mem_prefixIn lemma — The next D-node is not in the previous D-prefix.

hypotheses

N :

Type u_1
shared

H :

SWIGGraph N

D :

Finset (SWIGNode N)

n :

ℕ

hn :

n < D.card

conclusion

(H.nodesAt D ⟨n, hn⟩).val ∉ H.prefixIn D n

Proof (Lean source)

lemma nodesAt_not_mem_prefixIn (H : SWIGGraph N) (D : Finset (SWIGNode N)) {n : ℕ} (hn : n < D.card) : (H.nodesAt D ⟨n, hn⟩).val ∉ H.prefixIn D n := by rw [nodesAt_mem_prefixIn_iff H D n ⟨n, hn⟩] exact Nat.lt_irrefl n

Causalean.SCM.ID.nodesAt_not_mem_prefixIn · Causalean/SCM/ID/Density/QFactor/PrefixLemmas.lean:102
prefixIn_succ lemma — The successor D-prefix is obtained by adjoining the next D-node.

hypotheses

N :

Type u_1
shared

H :

SWIGGraph N

D :

Finset (SWIGNode N)

n :

ℕ

hn :

n < D.card

conclusion

H.prefixIn D (n + 1) = H.prefixIn D n ∪ {(H.nodesAt D ⟨n, hn⟩).val}

Proof (Lean source)

lemma prefixIn_succ (H : SWIGGraph N) (D : Finset (SWIGNode N)) {n : ℕ} (hn : n < D.card) : H.prefixIn D (n + 1) = H.prefixIn D n ∪ {(H.nodesAt D ⟨n, hn⟩).val} := by ext v constructor · intro hv rcases (mem_prefixIn_iff H D (n + 1) v).mp hv with ⟨hD, hlt⟩ by_cases hlt_n : (H.nodeIndex D ⟨v, hD⟩).val < n · exact mem_union_left _ ((mem_prefixIn_iff H D n v).mpr ⟨hD, hlt_n⟩) · have hidx_val : (H.nodeIndex D ⟨v, hD⟩).val = n := by omega have hidx : H.nodeIndex D ⟨v, hD⟩ = ⟨n, hn⟩ := Fin.ext hidx_val have hv_eq : v = (H.nodesAt D ⟨n, hn⟩).val := by have hround : H.nodesAt D (H.nodeIndex D ⟨v, hD⟩) = ⟨v, hD⟩ := by simp [SWIGGraph.nodeIndex, SWIGGraph.nodesAt] rw [hidx] at hround exact congrArg val hround.symm exact mem_union_right _ (by simp [hv_eq]) · intro hv rcases Finset.mem_union.mp hv with hvpre | hvlast · rcases (mem_prefixIn_iff H D n v).mp hvpre with ⟨hD, hlt⟩ exact (mem_prefixIn_iff H D (n + 1) v).mpr ⟨hD, by omega⟩ · have hv_eq : v = (H.nodesAt D ⟨n, hn⟩).val := by simpa using hvlast subst hv_eq rw [nodesAt_mem_prefixIn_iff H D (n + 1) ⟨n, hn⟩] exact lt_succ_self n

Causalean.SCM.ID.prefixIn_succ · Causalean/SCM/ID/Density/QFactor/PrefixLemmas.lean:109
prefixIn_disjoint_singleton_next lemma — The previous D-prefix is disjoint from the singleton next node.

hypotheses

N :

Type u_1
shared

H :

SWIGGraph N

D :

Finset (SWIGNode N)

n :

ℕ

hn :

n < D.card

conclusion

Disjoint (H.prefixIn D n) ({(H.nodesAt D ⟨n, hn⟩).val} : Finset (SWIGNode N))

Proof (Lean source)

lemma prefixIn_disjoint_singleton_next (H : SWIGGraph N) (D : Finset (SWIGNode N)) {n : ℕ} (hn : n < D.card) : Disjoint (H.prefixIn D n) ({(H.nodesAt D ⟨n, hn⟩).val} : Finset (SWIGNode N)) := by rw [Finset.disjoint_singleton_right] exact nodesAt_not_mem_prefixIn H D hn

Causalean.SCM.ID.prefixIn_disjoint_singleton_next · Causalean/SCM/ID/Density/QFactor/PrefixLemmas.lean:137
prefixIn_parent_closed_induce_observed lemma — In an induced set of observed variables, every topological prefix contains all parents within that set of each variable it contains.

hypotheses

N :

Type u_1
N → Type u_2
shared

M :

SCM N Ω

A :

Finset (SWIGNode N)

hA :

A ⊆ M.observed

k :

ℕ

v ∈ A :

w ∈ (M.toSWIGGraph.induce A).prefixIn A k :

M.dag.edge v w

conclusion

v ∈ (M.toSWIGGraph.induce A).prefixIn A k

Proof (Lean source)

lemma prefixIn_parent_closed_induce_observed (M : SCM N Ω) (A : Finset (SWIGNode N)) (hA : A ⊆ M.observed) (k : ℕ) : ∀ v ∈ A, ∀ w ∈ (M.toSWIGGraph.induce A).prefixIn A k, M.dag.edge v w → v ∈ (M.toSWIGGraph.induce A).prefixIn A k := by classical intro v hvA w hwPre hEdge let H := M.toSWIGGraph.induce A have hwA : w ∈ A := H.prefixIn_subset A k hwPre have hEdgeH : H.dag.edge v w := by dsimp [H, SWIGGraph.induce] rw [SWIGGraph.inducedDag_edge_iff] refine ⟨hEdge, ?_, ?_⟩ · simp [hvA, hA hvA] · simp [hwA, hA hwA] have hTopo : H.dag.topoOrder v < H.dag.topoOrder w := H.dag.topoOrder_lt v w hEdgeH rcases (mem_prefixIn_iff H A k w).mp hwPre with ⟨hwA', hwIdxLt⟩ letI := H.topoLinearOrder have hSubtypeLt : (⟨v, hvA⟩ : {v // v ∈ A}) < ⟨w, hwA'⟩ := by change H.dag.topoOrder v < H.dag.topoOrder w exact hTopo have hIndexLt : (H.nodeIndex A ⟨v, hvA⟩).val < (H.nodeIndex A ⟨w, hwA'⟩).val := by have hIndexLtFin : H.nodeIndex A ⟨v, hvA⟩ < H.nodeIndex A ⟨w, hwA'⟩ := by simpa [SWIGGraph.nodeIndex] using ((A.orderIsoOfFin rfl).symm.strictMono hSubtypeLt) simpa [SWIGGraph.nodeIndex] using hIndexLtFin exact (mem_prefixIn_iff H A k v).mpr ⟨hvA, lt_trans hIndexLt hwIdxLt⟩

Causalean.SCM.ID.prefixIn_parent_closed_induce_observed · Causalean/SCM/ID/Density/QFactor/PrefixLemmas.lean:145
cComponent_inter_prefixIn_succ_eq_of_ne lemma — Given a finite structural causal model, a graph, a node set, and two districts, if the first and second sets are districts, the node set is observed, the next prefix node lies in the first district, and the districts differ, then intersecting the second district with the prefix is unchanged at that step.

hypotheses

N :

Type u_1
N → Type u_2
shared

M :

SCM N Ω

H :

SWIGGraph N

D :

Finset (SWIGNode N)

S C :

Finset (SWIGNode N)

hScomp :

S ∈ M.toSWIGGraph.cComponentSet

hCcomp :

C ∈ M.toSWIGGraph.cComponentSet

i :

Fin D.card

hDobs :

D ⊆ M.observed

hiS :

(H.nodesAt D i).val ∈ S

hCS :

C ≠ S

conclusion

C ∩ H.prefixIn D (i.val + 1) = C ∩ H.prefixIn D i.val

Proof (Lean source)

lemma cComponent_inter_prefixIn_succ_eq_of_ne (M : SCM N Ω) (H : SWIGGraph N) (D : Finset (SWIGNode N)) {S C : Finset (SWIGNode N)} (hScomp : S ∈ M.toSWIGGraph.cComponentSet) (hCcomp : C ∈ M.toSWIGGraph.cComponentSet) {i : Fin D.card} (hDobs : D ⊆ M.observed) (hiS : (H.nodesAt D i).val ∈ S) (hCS : C ≠ S) : C ∩ H.prefixIn D (i.val + 1) = C ∩ H.prefixIn D i.val := by classical ext v constructor · intro hv rcases Finset.mem_inter.mp hv with ⟨hvC, hvpre⟩ rw [prefixIn_succ H D i.isLt] at hvpre rcases Finset.mem_union.mp hvpre with hvold | hvnew · exact Finset.mem_inter.mpr ⟨hvC, hvold⟩ · have hvnode : v = (H.nodesAt D i).val := by simpa using hvnew subst hvnode have hnodeObs : (H.nodesAt D i).val ∈ M.observed := hDobs (H.nodesAt D i).property have hSC : S = C := by exact (mem_cComponent_iff_cComponentOf_eq M.toSWIGGraph hnodeObs hCcomp).mp hvC ▸ ((mem_cComponent_iff_cComponentOf_eq M.toSWIGGraph hnodeObs hScomp).mp hiS).symm exact False.elim (hCS hSC.symm) · intro hv rcases Finset.mem_inter.mp hv with ⟨hvC, hvpre⟩ exact Finset.mem_inter.mpr ⟨hvC, prefixIn_mono H D (le_succ i.val) hvpre⟩

Causalean.SCM.ID.cComponent_inter_prefixIn_succ_eq_of_ne · Causalean/SCM/ID/Density/QFactor/PrefixLemmas.lean:240
family_inter_prefixIn_succ_eq_of_ne lemma — Given a finite graph, node set, two families, and a prefix index, if the next prefix node lies in the first family and the families are disjoint, then intersecting the second family with the prefix is unchanged at that step.

hypotheses

N :

Type u_1
shared

H :

SWIGGraph N

D :

Finset (SWIGNode N)

S C :

Finset (SWIGNode N)

i :

Fin D.card

hiS :

(H.nodesAt D i).val ∈ S

hdisj :

Disjoint C S

conclusion

C ∩ H.prefixIn D (i.val + 1) = C ∩ H.prefixIn D i.val

Proof (Lean source)

lemma family_inter_prefixIn_succ_eq_of_ne (H : SWIGGraph N) (D : Finset (SWIGNode N)) {S C : Finset (SWIGNode N)} {i : Fin D.card} (hiS : (H.nodesAt D i).val ∈ S) (hdisj : Disjoint C S) : C ∩ H.prefixIn D (i.val + 1) = C ∩ H.prefixIn D i.val := by classical ext v constructor · intro hv rcases Finset.mem_inter.mp hv with ⟨hvC, hvpre⟩ rw [prefixIn_succ H D i.isLt] at hvpre rcases Finset.mem_union.mp hvpre with hvold | hvnew · exact Finset.mem_inter.mpr ⟨hvC, hvold⟩ · have hvnode : v = (H.nodesAt D i).val := by simpa using hvnew subst hvnode exact False.elim (Finset.disjoint_left.mp hdisj hvC hiS) · intro hv rcases Finset.mem_inter.mp hv with ⟨hvC, hvpre⟩ exact Finset.mem_inter.mpr ⟨hvC, prefixIn_mono H D (le_succ i.val) hvpre⟩

Causalean.SCM.ID.family_inter_prefixIn_succ_eq_of_ne · Causalean/SCM/ID/Density/QFactor/PrefixLemmas.lean:277
cComponent_inter_prefixIn_succ_eq_of_node_not_mem lemma — Given a finite graph, node set, component, and prefix index, if the next prefix node is outside the component, then the component's intersection with the prefix is unchanged at that step.

hypotheses

N :

Type u_1
shared

H :

SWIGGraph N

D :

Finset (SWIGNode N)

S :

Finset (SWIGNode N)

i :

Fin D.card

hiS :

(H.nodesAt D i).val ∉ S

conclusion

S ∩ H.prefixIn D (i.val + 1) = S ∩ H.prefixIn D i.val

Proof (Lean source)

lemma cComponent_inter_prefixIn_succ_eq_of_node_not_mem (H : SWIGGraph N) (D : Finset (SWIGNode N)) {S : Finset (SWIGNode N)} {i : Fin D.card} (hiS : (H.nodesAt D i).val ∉ S) : S ∩ H.prefixIn D (i.val + 1) = S ∩ H.prefixIn D i.val := by classical ext v constructor · intro hv rcases Finset.mem_inter.mp hv with ⟨hvS, hvpre⟩ rw [prefixIn_succ H D i.isLt] at hvpre rcases Finset.mem_union.mp hvpre with hvold | hvnew · exact Finset.mem_inter.mpr ⟨hvS, hvold⟩ · have hvnode : v = (H.nodesAt D i).val := by simpa using hvnew subst hvnode exact False.elim (hiS hvS) · intro hv rcases Finset.mem_inter.mp hv with ⟨hvS, hvpre⟩ exact Finset.mem_inter.mpr ⟨hvS, prefixIn_mono H D (le_succ i.val) hvpre⟩

Causalean.SCM.ID.cComponent_inter_prefixIn_succ_eq_of_node_not_mem · Causalean/SCM/ID/Density/QFactor/PrefixLemmas.lean:302

RatioProduct 1 core · 7 supporting This file shows how ratios of prefix q-mass products isolate a selected component. ★ identifyMassRec_qLocalMass

Prefix-ratio products for recursive q-factor recovery

This file shows how ratios of prefix q-mass products isolate a selected component. It culminates in district extraction and the correspondence between identifyMassRec and the local q-mass recovered along an IDENTIFY certificate.

theorem identifyMassRec_qLocalMass reviewed

Causalean.SCM.ID

For a finite structural causal model with finite measurable node-value spaces, a fixed-node assignment, positive observational atom masses, source and target districts, evidence that the source is observed, a recursive c-factor reachability certificate from source to target, and an observed realization, the observational IDENTIFY recursion recovers the target district's local q-mass from the source district's local q-mass.

Formal statement

hypotheses

N :

Type u_1

N → Type u_2

shared

∀ n, Fintype (Ω n)

∀ n, MeasurableSingletonClass (Ω n)

M :

SCM N Ω

s :

M.FixedValues

hpos :

DiscreteID.PositiveMass (M.obsKernel s)

T C :

hT :

T ⊆ M.observed

hReach :

CFactorReachableRec M.toSWIGGraph T C

x :

ValuesOn M.observed (swigΩ Ω)

conclusion

identifyMassRec M.observed M.toSWIGGraph T C hT (M.qLocalMass s T hT) x

= M.qLocalMass s C (fun _ hv => hT (hReach.target_subset hv)) x

Proof (Lean source)

theorem identifyMassRec_qLocalMass [∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)] (M : SCM N Ω) (s : M.FixedValues) (hpos : DiscreteID.PositiveMass (M.obsKernel s)) (T C : Finset (SWIGNode N)) (hT : T ⊆ M.observed) (hReach : CFactorReachableRec M.toSWIGGraph T C) (x : ValuesOn M.observed (swigΩ Ω)) : identifyMassRec M.observed M.toSWIGGraph T C hT (M.qLocalMass s T hT) x = M.qLocalMass s C (fun _ hv => hT (hReach.target_subset hv)) x := by classical induction hReach generalizing x with | base hne hCT hproject => rename_i T₀ C₀ rw [SCM.identifyMassRec_base M M.toSWIGGraph T₀ C₀ hT (M.qLocalMass s T₀ hT) hproject] have hclosed : ∀ v ∈ T₀, ∀ w ∈ C₀, M.dag.edge v w → v ∈ C₀ := by have hclosedA := inducedAncestral_parent_closed M.toSWIGGraph (T := T₀) (C := C₀) (by simpa using hT) intro v hvT w hwC hEdge have hwA : w ∈ inducedAncestral M.toSWIGGraph T₀ C₀ := by simpa [hproject] using hwC have hvA := hclosedA v hvT w hwA hEdge simpa [hproject] using hvA exact M.qLocalMass_marginalize_ancestralClosed s T₀ C₀ hT hCT hclosed x | step hne hCT hnotC hnotT hrec ih => rename_i T₀ C₀ let A := inducedAncestral M.toSWIGGraph T₀ C₀ let C₁ := containingCComponent (M.toSWIGGraph.induce A) C₀ let hA : A ⊆ M.observed := fun _ hv => hT (inducedAncestral_subset_left M.toSWIGGraph T₀ C₀ hv) let hC₁obs : C₁ ⊆ M.observed := fun _ hv => hT (inducedAncestral_subset_left M.toSWIGGraph T₀ C₀ (containingCComponent_induce_subset M.toSWIGGraph A C₀ hv)) have hCobs : C₀ ⊆ M.toSWIGGraph.observed := by intro v hv simpa using hT (hCT hv) have hCA : C₀ ⊆ A := subset_inducedAncestral M.toSWIGGraph hCT hCobs have hC₁mem : C₁ ∈ (M.toSWIGGraph.induce A).cComponentSet := by simp only [C₁, containingCComponent, dif_pos hne, SWIGGraph.cComponentSet] have hchooseA : hne.choose ∈ A := hCA hne.choose_spec have hchooseObs : hne.choose ∈ M.toSWIGGraph.observed := hCobs hne.choose_spec have hchooseInd : hne.choose ∈ (M.toSWIGGraph.induce A).observed := by simp [SWIGGraph.induce, hchooseA, hchooseObs] exact Finset.mem_image.mpr ⟨hne.choose, hchooseInd, rfl⟩ have hmarg : marginalizeOn M.observed (T₀ \ A) (fun _ hv => hT ((Finset.mem_sdiff.mp hv).1)) (M.qLocalMass s T₀ hT) = M.qLocalMass s A hA := by funext y have hclosedA : ∀ v ∈ T₀, ∀ w ∈ A, M.dag.edge v w → v ∈ A := by simpa [A] using inducedAncestral_parent_closed M.toSWIGGraph (T := T₀) (C := C₀) (by simpa using hT) exact M.qLocalMass_marginalize_ancestralClosed s T₀ A hT (inducedAncestral_subset_left M.toSWIGGraph T₀ C₀) hclosedA y have hextract : extractDistrict M.observed (M.toSWIGGraph.induce A) A C₁ hA (M.qLocalMass s A hA) = M.qLocalMass s C₁ hC₁obs := by funext y calc extractDistrict M.observed (M.toSWIGGraph.induce A) A C₁ hA (M.qLocalMass s A hA) y = M.qLocalMass s C₁ (fun _ hv => hA (by have hHobs : (M.toSWIGGraph.induce A).observed = A := by simp [SWIGGraph.induce, Finset.inter_eq_left.mpr hA] exact hHobs ▸ (M.toSWIGGraph.induce A).cComponentSet_subset_observed C₁ hC₁mem hv)) y := by exact extractDistrict_qLocalMass M s A C₁ hA hC₁mem hpos y _ = M.qLocalMass s C₁ hC₁obs y := by exact qLocalMass_obsProof_irrel M s C₁ _ _ y rw [SCM.identifyMassRec_step M M.toSWIGGraph T₀ C₀ hT (M.qLocalMass s T₀ hT) hnotC hnotT] change identifyMassRec M.observed M.toSWIGGraph C₁ C₀ hC₁obs (extractDistrict M.observed (M.toSWIGGraph.induce A) A C₁ hA (marginalizeOn M.observed (T₀ \ A) (fun _ hv => hT ((Finset.mem_sdiff.mp hv).1)) (M.qLocalMass s T₀ hT))) x = _ rw [hmarg, hextract] calc identifyMassRec M.observed M.toSWIGGraph C₁ C₀ hC₁obs (M.qLocalMass s C₁ hC₁obs) x = M.qLocalMass s C₀ (fun _ hv => hC₁obs (hrec.target_subset hv)) x := by exact ih hC₁obs x _ = M.qLocalMass s C₀ (fun _ hv => hT ((CFactorReachableRec.step hne hCT hnotC hnotT hrec).target_subset hv)) x := by exact qLocalMass_obsProof_irrel M s C₀ _ _ x

Causalean.SCM.ID.identifyMassRec_qLocalMass · Causalean/SCM/ID/Density/QFactor/RatioProduct.lean:572 · uses SWIGNode , instMeasurableSpaceSwigΩ , swigΩ , ValuesOn , SCM , FixedValues , CFactorReachableRec , target_subset , PositiveMass , ObservedValues , identifyMassRec , obsKernel , qLocalMass

7 supporting declarations (lemmas, instances)

prefixIn_qProduct_ratio_eq_component_ratio_of_family lemma — In a product over an abstract pairwise-disjoint family, the prefix-ratio step at a node of S cancels every factor except the S factor.

hypotheses

N :

Type u_1
N → Type u_2
shared

∀ n, Fintype (Ω n)

∀ n, MeasurableSingletonClass (Ω n)

M :

SCM N Ω

H :

SWIGGraph N

D :

Finset (SWIGNode N)

s :

M.FixedValues

𝒞 :

Finset (Finset (SWIGNode N))

S :

Finset (SWIGNode N)

hS𝒞 :

S ∈ 𝒞

hdisj :

∀ C ∈ 𝒞
if
C ≠ S
then
Disjoint C S

i :

Fin D.card

hDobs :

D ⊆ M.observed

hiS :

(H.nodesAt D i).val ∈ S

hpos :

DiscreteID.PositiveMass (M.obsKernel s)

x :

ValuesOn M.observed (swigΩ Ω)

conclusion

(∏ C ∈ 𝒞, M.qLocalMass s (C ∩ H.prefixIn D (i.val + 1)) (fun _ hv => hDobs (H.prefixIn_subset D (i.val + 1) (mem_of_mem_inter_right hv))) x) / (∏ C ∈ 𝒞, M.qLocalMass s (C ∩ H.prefixIn D i.val) (fun _ hv => hDobs (H.prefixIn_subset D i.val (mem_of_mem_inter_right hv))) x)
= M.qLocalMass s (S ∩ H.prefixIn D (i.val + 1)) (fun _ hv => hDobs (H.prefixIn_subset D (i.val + 1) (mem_of_mem_inter_right hv))) x / M.qLocalMass s (S ∩ H.prefixIn D i.val) (fun _ hv => hDobs (H.prefixIn_subset D i.val (mem_of_mem_inter_right hv))) x

Proof (Lean source)

lemma prefixIn_qProduct_ratio_eq_component_ratio_of_family [∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)] (M : SCM N Ω) (H : SWIGGraph N) (D : Finset (SWIGNode N)) (s : M.FixedValues) (𝒞 : Finset (Finset (SWIGNode N))) (S : Finset (SWIGNode N)) (hS𝒞 : S ∈ 𝒞) (hdisj : ∀ C ∈ 𝒞, C ≠ S → Disjoint C S) (i : Fin D.card) (hDobs : D ⊆ M.observed) (hiS : (H.nodesAt D i).val ∈ S) (hpos : DiscreteID.PositiveMass (M.obsKernel s)) (x : ValuesOn M.observed (swigΩ Ω)) : (∏ C ∈ 𝒞, M.qLocalMass s (C ∩ H.prefixIn D (i.val + 1)) (fun _ hv => hDobs (H.prefixIn_subset D (i.val + 1) (mem_of_mem_inter_right hv))) x) / (∏ C ∈ 𝒞, M.qLocalMass s (C ∩ H.prefixIn D i.val) (fun _ hv => hDobs (H.prefixIn_subset D i.val (mem_of_mem_inter_right hv))) x) = M.qLocalMass s (S ∩ H.prefixIn D (i.val + 1)) (fun _ hv => hDobs (H.prefixIn_subset D (i.val + 1) (mem_of_mem_inter_right hv))) x / M.qLocalMass s (S ∩ H.prefixIn D i.val) (fun _ hv => hDobs (H.prefixIn_subset D i.val (mem_of_mem_inter_right hv))) x := by classical let f₁ : Finset (SWIGNode N) → ENNReal := fun C => M.qLocalMass s (C ∩ H.prefixIn D (i.val + 1)) (fun _ hv => hDobs (H.prefixIn_subset D (i.val + 1) (mem_of_mem_inter_right hv))) x let f₀ : Finset (SWIGNode N) → ENNReal := fun C => M.qLocalMass s (C ∩ H.prefixIn D i.val) (fun _ hv => hDobs (H.prefixIn_subset D i.val (mem_of_mem_inter_right hv))) x have hrest : ∏ C ∈ 𝒞 \ {S}, f₁ C = ∏ C ∈ 𝒞 \ {S}, f₀ C := by refine Finset.prod_congr rfl ?_ intro C hC have hC𝒞 : C ∈ 𝒞 := (Finset.mem_sdiff.mp hC).1 have hCne : C ≠ S := by intro h exact (Finset.mem_sdiff.mp hC).2 (by simp [h]) simp [f₁, f₀, family_inter_prefixIn_succ_eq_of_ne H D hiS (hdisj C hC𝒞 hCne)] have hsplit₁ : (∏ C ∈ 𝒞, f₁ C) = f₁ S * ∏ C ∈ 𝒞 \ {S}, f₁ C := by exact Finset.prod_eq_mul_prod_diff_singleton S f₁ (by intro h; exact False.elim (h hS𝒞)) have hsplit₀ : (∏ C ∈ 𝒞, f₀ C) = f₀ S * ∏ C ∈ 𝒞 \ {S}, f₀ C := by exact Finset.prod_eq_mul_prod_diff_singleton S f₀ (by intro h; exact False.elim (h hS𝒞)) have hr0 : (∏ C ∈ 𝒞 \ {S}, f₀ C) ≠ 0 := by exact Finset.prod_ne_zero_iff.mpr (by intro C _hC exact M.qLocalMass_pos_of_positiveObs s hpos (C ∩ H.prefixIn D i.val) (fun _ hv => hDobs (H.prefixIn_subset D i.val (mem_of_mem_inter_right hv))) x) have hrtop : (∏ C ∈ 𝒞 \ {S}, f₀ C) ≠ ∞ := by exact Finset.prod_ne_top_of_ne_top _ f₀ (by intro C _hC exact qLocalMass_ne_top M s (C ∩ H.prefixIn D i.val) (fun _ hv => hDobs (H.prefixIn_subset D i.val (mem_of_mem_inter_right hv))) x) change (∏ C ∈ 𝒞, f₁ C) / (∏ C ∈ 𝒞, f₀ C) = f₁ S / f₀ S rw [hsplit₁, hsplit₀, hrest] exact ENNReal.div_mul_common hr0 hrtop

Causalean.SCM.ID.prefixIn_qProduct_ratio_eq_component_ratio_of_family · Causalean/SCM/ID/Density/QFactor/RatioProduct.lean:39
prefixIn_qProduct_ratio_eq_component_ratio_of_ne_zero lemma — Given a finite structural causal model, graph, observed node set, fixed assignment, district, prefix index, and observed assignment, if the set is a district, the node set is observed, the next prefix node lies in that district, and the product of all other district factors is nonzero, then the ratio of successive full prefix products equals the corresponding ratio for that district.

hypotheses

N :

Type u_1
N → Type u_2
shared

∀ n, Fintype (Ω n)

∀ n, MeasurableSingletonClass (Ω n)

M :

SCM N Ω

H :

SWIGGraph N

D :

Finset (SWIGNode N)

s :

M.FixedValues

S :

Finset (SWIGNode N)

hScomp :

S ∈ M.toSWIGGraph.cComponentSet

i :

Fin D.card

hDobs :

D ⊆ M.observed

hiS :

(H.nodesAt D i).val ∈ S

x :

ValuesOn M.observed (swigΩ Ω)

hrest0 :

(∏ C ∈ M.toSWIGGraph.cComponentSet \ {S}, M.qLocalMass s (C ∩ H.prefixIn D i.val) (fun _ hv => hDobs (H.prefixIn_subset D i.val (mem_of_mem_inter_right hv))) x)
≠ 0

conclusion

(∏ C ∈ M.toSWIGGraph.cComponentSet, M.qLocalMass s (C ∩ H.prefixIn D (i.val + 1)) (fun _ hv => hDobs (H.prefixIn_subset D (i.val + 1) (mem_of_mem_inter_right hv))) x) / (∏ C ∈ M.toSWIGGraph.cComponentSet, M.qLocalMass s (C ∩ H.prefixIn D i.val) (fun _ hv => hDobs (H.prefixIn_subset D i.val (mem_of_mem_inter_right hv))) x)
= M.qLocalMass s (S ∩ H.prefixIn D (i.val + 1)) (fun _ hv => hDobs (H.prefixIn_subset D (i.val + 1) (mem_of_mem_inter_right hv))) x / M.qLocalMass s (S ∩ H.prefixIn D i.val) (fun _ hv => hDobs (H.prefixIn_subset D i.val (mem_of_mem_inter_right hv))) x

Proof (Lean source)

lemma prefixIn_qProduct_ratio_eq_component_ratio_of_ne_zero [∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)] (M : SCM N Ω) (H : SWIGGraph N) (D : Finset (SWIGNode N)) (s : M.FixedValues) (S : Finset (SWIGNode N)) (hScomp : S ∈ M.toSWIGGraph.cComponentSet) (i : Fin D.card) (hDobs : D ⊆ M.observed) (hiS : (H.nodesAt D i).val ∈ S) (x : ValuesOn M.observed (swigΩ Ω)) (hrest0 : (∏ C ∈ M.toSWIGGraph.cComponentSet \ {S}, M.qLocalMass s (C ∩ H.prefixIn D i.val) (fun _ hv => hDobs (H.prefixIn_subset D i.val (mem_of_mem_inter_right hv))) x) ≠ 0) : (∏ C ∈ M.toSWIGGraph.cComponentSet, M.qLocalMass s (C ∩ H.prefixIn D (i.val + 1)) (fun _ hv => hDobs (H.prefixIn_subset D (i.val + 1) (mem_of_mem_inter_right hv))) x) / (∏ C ∈ M.toSWIGGraph.cComponentSet, M.qLocalMass s (C ∩ H.prefixIn D i.val) (fun _ hv => hDobs (H.prefixIn_subset D i.val (mem_of_mem_inter_right hv))) x) = M.qLocalMass s (S ∩ H.prefixIn D (i.val + 1)) (fun _ hv => hDobs (H.prefixIn_subset D (i.val + 1) (mem_of_mem_inter_right hv))) x / M.qLocalMass s (S ∩ H.prefixIn D i.val) (fun _ hv => hDobs (H.prefixIn_subset D i.val (mem_of_mem_inter_right hv))) x := by classical let f₁ : Finset (SWIGNode N) → ENNReal := fun C => M.qLocalMass s (C ∩ H.prefixIn D (i.val + 1)) (fun _ hv => hDobs (H.prefixIn_subset D (i.val + 1) (mem_of_mem_inter_right hv))) x let f₀ : Finset (SWIGNode N) → ENNReal := fun C => M.qLocalMass s (C ∩ H.prefixIn D i.val) (fun _ hv => hDobs (H.prefixIn_subset D i.val (mem_of_mem_inter_right hv))) x have hrest : ∏ C ∈ M.toSWIGGraph.cComponentSet \ {S}, f₁ C = ∏ C ∈ M.toSWIGGraph.cComponentSet \ {S}, f₀ C := by refine Finset.prod_congr rfl ?_ intro C hC have hCcomp : C ∈ M.toSWIGGraph.cComponentSet := (Finset.mem_sdiff.mp hC).1 have hCne : C ≠ S := by intro h exact (Finset.mem_sdiff.mp hC).2 (by simp [h]) simp [f₁, f₀, cComponent_inter_prefixIn_succ_eq_of_ne M H D hScomp hCcomp hDobs hiS hCne] have hsplit₁ : (∏ C ∈ M.toSWIGGraph.cComponentSet, f₁ C) = f₁ S * ∏ C ∈ M.toSWIGGraph.cComponentSet \ {S}, f₁ C := by exact Finset.prod_eq_mul_prod_diff_singleton S f₁ (by intro h; exact False.elim (h hScomp)) have hsplit₀ : (∏ C ∈ M.toSWIGGraph.cComponentSet, f₀ C) = f₀ S * ∏ C ∈ M.toSWIGGraph.cComponentSet \ {S}, f₀ C := by exact Finset.prod_eq_mul_prod_diff_singleton S f₀ (by intro h; exact False.elim (h hScomp)) have hrtop : (∏ C ∈ M.toSWIGGraph.cComponentSet \ {S}, f₀ C) ≠ ∞ := by exact Finset.prod_ne_top_of_ne_top _ f₀ (by intro C _hC exact qLocalMass_ne_top M s (C ∩ H.prefixIn D i.val) (fun _ hv => hDobs (H.prefixIn_subset D i.val (mem_of_mem_inter_right hv))) x) change (∏ C ∈ M.toSWIGGraph.cComponentSet, f₁ C) / (∏ C ∈ M.toSWIGGraph.cComponentSet, f₀ C) = f₁ S / f₀ S rw [hsplit₁, hsplit₀, hrest] exact ENNReal.div_mul_common hrest0 hrtop

Causalean.SCM.ID.prefixIn_qProduct_ratio_eq_component_ratio_of_ne_zero · Causalean/SCM/ID/Density/QFactor/RatioProduct.lean:111
prefixIn_qProduct_ratio_eq_component_ratio_of_family_of_ne_zero lemma — Nonzero-denominator variant of prefixIn_qProduct_ratio_eq_component_ratio_of_family.

hypotheses

N :

Type u_1
N → Type u_2
shared

∀ n, Fintype (Ω n)

∀ n, MeasurableSingletonClass (Ω n)

M :

SCM N Ω

H :

SWIGGraph N

D :

Finset (SWIGNode N)

s :

M.FixedValues

𝒞 :

Finset (Finset (SWIGNode N))

S :

Finset (SWIGNode N)

hS𝒞 :

S ∈ 𝒞

hdisj :

∀ C ∈ 𝒞
if
C ≠ S
then
Disjoint C S

i :

Fin D.card

hDobs :

D ⊆ M.observed

hiS :

(H.nodesAt D i).val ∈ S

x :

ValuesOn M.observed (swigΩ Ω)

hrest0 :

(∏ C ∈ 𝒞 \ {S}, M.qLocalMass s (C ∩ H.prefixIn D i.val) (fun _ hv => hDobs (H.prefixIn_subset D i.val (mem_of_mem_inter_right hv))) x)
≠ 0

conclusion

(∏ C ∈ 𝒞, M.qLocalMass s (C ∩ H.prefixIn D (i.val + 1)) (fun _ hv => hDobs (H.prefixIn_subset D (i.val + 1) (mem_of_mem_inter_right hv))) x) / (∏ C ∈ 𝒞, M.qLocalMass s (C ∩ H.prefixIn D i.val) (fun _ hv => hDobs (H.prefixIn_subset D i.val (mem_of_mem_inter_right hv))) x)
= M.qLocalMass s (S ∩ H.prefixIn D (i.val + 1)) (fun _ hv => hDobs (H.prefixIn_subset D (i.val + 1) (mem_of_mem_inter_right hv))) x / M.qLocalMass s (S ∩ H.prefixIn D i.val) (fun _ hv => hDobs (H.prefixIn_subset D i.val (mem_of_mem_inter_right hv))) x

Proof (Lean source)

lemma prefixIn_qProduct_ratio_eq_component_ratio_of_family_of_ne_zero [∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)] (M : SCM N Ω) (H : SWIGGraph N) (D : Finset (SWIGNode N)) (s : M.FixedValues) (𝒞 : Finset (Finset (SWIGNode N))) (S : Finset (SWIGNode N)) (hS𝒞 : S ∈ 𝒞) (hdisj : ∀ C ∈ 𝒞, C ≠ S → Disjoint C S) (i : Fin D.card) (hDobs : D ⊆ M.observed) (hiS : (H.nodesAt D i).val ∈ S) (x : ValuesOn M.observed (swigΩ Ω)) (hrest0 : (∏ C ∈ 𝒞 \ {S}, M.qLocalMass s (C ∩ H.prefixIn D i.val) (fun _ hv => hDobs (H.prefixIn_subset D i.val (mem_of_mem_inter_right hv))) x) ≠ 0) : (∏ C ∈ 𝒞, M.qLocalMass s (C ∩ H.prefixIn D (i.val + 1)) (fun _ hv => hDobs (H.prefixIn_subset D (i.val + 1) (mem_of_mem_inter_right hv))) x) / (∏ C ∈ 𝒞, M.qLocalMass s (C ∩ H.prefixIn D i.val) (fun _ hv => hDobs (H.prefixIn_subset D i.val (mem_of_mem_inter_right hv))) x) = M.qLocalMass s (S ∩ H.prefixIn D (i.val + 1)) (fun _ hv => hDobs (H.prefixIn_subset D (i.val + 1) (mem_of_mem_inter_right hv))) x / M.qLocalMass s (S ∩ H.prefixIn D i.val) (fun _ hv => hDobs (H.prefixIn_subset D i.val (mem_of_mem_inter_right hv))) x := by classical let f₁ : Finset (SWIGNode N) → ENNReal := fun C => M.qLocalMass s (C ∩ H.prefixIn D (i.val + 1)) (fun _ hv => hDobs (H.prefixIn_subset D (i.val + 1) (mem_of_mem_inter_right hv))) x let f₀ : Finset (SWIGNode N) → ENNReal := fun C => M.qLocalMass s (C ∩ H.prefixIn D i.val) (fun _ hv => hDobs (H.prefixIn_subset D i.val (mem_of_mem_inter_right hv))) x have hrest : ∏ C ∈ 𝒞 \ {S}, f₁ C = ∏ C ∈ 𝒞 \ {S}, f₀ C := by refine Finset.prod_congr rfl ?_ intro C hC have hC𝒞 : C ∈ 𝒞 := (Finset.mem_sdiff.mp hC).1 have hCne : C ≠ S := by intro h exact (Finset.mem_sdiff.mp hC).2 (by simp [h]) simp [f₁, f₀, family_inter_prefixIn_succ_eq_of_ne H D hiS (hdisj C hC𝒞 hCne)] have hsplit₁ : (∏ C ∈ 𝒞, f₁ C) = f₁ S * ∏ C ∈ 𝒞 \ {S}, f₁ C := by exact Finset.prod_eq_mul_prod_diff_singleton S f₁ (by intro h; exact False.elim (h hS𝒞)) have hsplit₀ : (∏ C ∈ 𝒞, f₀ C) = f₀ S * ∏ C ∈ 𝒞 \ {S}, f₀ C := by exact Finset.prod_eq_mul_prod_diff_singleton S f₀ (by intro h; exact False.elim (h hS𝒞)) have hrtop : (∏ C ∈ 𝒞 \ {S}, f₀ C) ≠ ∞ := by exact Finset.prod_ne_top_of_ne_top _ f₀ (by intro C _hC exact qLocalMass_ne_top M s (C ∩ H.prefixIn D i.val) (fun _ hv => hDobs (H.prefixIn_subset D i.val (mem_of_mem_inter_right hv))) x) change (∏ C ∈ 𝒞, f₁ C) / (∏ C ∈ 𝒞, f₀ C) = f₁ S / f₀ S rw [hsplit₁, hsplit₀, hrest] exact ENNReal.div_mul_common hrest0 hrtop

Causalean.SCM.ID.prefixIn_qProduct_ratio_eq_component_ratio_of_family_of_ne_zero · Causalean/SCM/ID/Density/QFactor/RatioProduct.lean:183
component_qLocalMass_ratio_product_prefixIn_of_ne_zero lemma — Given a finite structural causal model, graph, node set, fixed assignment, district, and observed assignment, if the district is observed, it lies in the node set, and all of its prefix local masses are nonzero, then the product of its successive prefix-mass ratios equals its full local mass.

hypotheses

N :

Type u_1
N → Type u_2
shared

∀ n, Fintype (Ω n)

∀ n, MeasurableSingletonClass (Ω n)

M :

SCM N Ω

H :

SWIGGraph N

D :

Finset (SWIGNode N)

s :

M.FixedValues

S :

Finset (SWIGNode N)

hS :

S ⊆ M.observed

hSD :

S ⊆ D

x :

ValuesOn M.observed (swigΩ Ω)

hne :

∀ k ≤ D.card,
M.qLocalMass s (S ∩ H.prefixIn D k) (fun _ hv => hS (mem_of_mem_inter_left hv)) x
≠ 0

conclusion

(∏ i ∈ Finset.univ.filter (fun i : Fin D.card => (H.nodesAt D i).val ∈ S), M.qLocalMass s (S ∩ H.prefixIn D (i.val + 1)) (fun _ hv => hS (mem_of_mem_inter_left hv)) x / M.qLocalMass s (S ∩ H.prefixIn D i.val) (fun _ hv => hS (mem_of_mem_inter_left hv)) x)
= M.qLocalMass s S hS x

Proof (Lean source)

lemma component_qLocalMass_ratio_product_prefixIn_of_ne_zero [∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)] (M : SCM N Ω) (H : SWIGGraph N) (D : Finset (SWIGNode N)) (s : M.FixedValues) (S : Finset (SWIGNode N)) (hS : S ⊆ M.observed) (hSD : S ⊆ D) (x : ValuesOn M.observed (swigΩ Ω)) (hne : ∀ k ≤ D.card, M.qLocalMass s (S ∩ H.prefixIn D k) (fun _ hv => hS (mem_of_mem_inter_left hv)) x ≠ 0) : (∏ i ∈ Finset.univ.filter (fun i : Fin D.card => (H.nodesAt D i).val ∈ S), M.qLocalMass s (S ∩ H.prefixIn D (i.val + 1)) (fun _ hv => hS (mem_of_mem_inter_left hv)) x / M.qLocalMass s (S ∩ H.prefixIn D i.val) (fun _ hv => hS (mem_of_mem_inter_left hv)) x) = M.qLocalMass s S hS x := by classical let hPrefObs : ∀ k, S ∩ H.prefixIn D k ⊆ M.observed := fun k _ hv => hS (mem_of_mem_inter_left hv) let a : ℕ → ENNReal := fun k => M.qLocalMass s (S ∩ H.prefixIn D k) (hPrefObs k) x let T : Finset ℕ := (range D.card).filter fun k => if hk : k < D.card then (H.nodesAt D ⟨k, hk⟩).val ∈ S else False have hreindex : (∏ i ∈ Finset.univ.filter (fun i : Fin D.card => (H.nodesAt D i).val ∈ S), a (i.val + 1) / a i.val) = ∏ k ∈ T, a (k + 1) / a k := by refine Finset.prod_bij (fun i _hi => i.val) ?_ ?_ ?_ ?_ · intro i hi simp [T, i.isLt, Finset.mem_filter.mp hi] · intro i _hi j _hj hij exact Fin.ext hij · intro k hk simp [T] at hk have hklt : k < D.card := hk.1 refine ⟨⟨k, hklt⟩, ?_, rfl⟩ rw [mem_filter] exact ⟨Finset.mem_univ _, by simpa [hklt] using hk.2⟩ · intro i _hi rfl have hTsubset : T ⊆ range D.card := by intro k hk exact (Finset.mem_filter.mp hk).1 have hne' : ∀ k ≤ D.card, a k ≠ 0 := by intro k hk exact hne k hk have hfin : ∀ k ≤ D.card, a k ≠ ∞ := by intro k hk exact qLocalMass_ne_top M s (S ∩ H.prefixIn D k) (hPrefObs k) x have hconst : ∀ k < D.card, k ∉ T → a (k + 1) = a k := by intro k hk hnot have hnode_not : (H.nodesAt D ⟨k, hk⟩).val ∉ S := by intro hnode exact hnot (by simp [T, hk, hnode]) dsimp [a] have hset : S ∩ H.prefixIn D (k + 1) = S ∩ H.prefixIn D k := cComponent_inter_prefixIn_succ_eq_of_node_not_mem H D hnode_not unfold qLocalMass congr 1 ext ℓ constructor · intro hℓ v hv have hv' : v ∈ S ∩ H.prefixIn D (k + 1) := by simpa [hset] using hv simpa using hℓ v hv' · intro hℓ v hv have hv' : v ∈ S ∩ H.prefixIn D k := by simpa [hset] using hv simpa using hℓ v hv' have htelescope : ∏ k ∈ T, a (k + 1) / a k = a D.card / a 0 := prod_filter_div_telescope a D.card T hTsubset hne' hfin hconst have htop : S ∩ H.prefixIn D D.card = S := by rw [prefixIn_card H D] exact Finset.inter_eq_left.mpr hSD have hzero : S ∩ H.prefixIn D 0 = ∅ := by rw [prefixIn_zero H D, Finset.inter_empty] calc (∏ i ∈ Finset.univ.filter (fun i : Fin D.card => (H.nodesAt D i).val ∈ S), M.qLocalMass s (S ∩ H.prefixIn D (i.val + 1)) (fun _ hv => hS (mem_of_mem_inter_left hv)) x / M.qLocalMass s (S ∩ H.prefixIn D i.val) (fun _ hv => hS (mem_of_mem_inter_left hv)) x) = ∏ i ∈ Finset.univ.filter (fun i : Fin D.card => (H.nodesAt D i).val ∈ S), a (i.val + 1) / a i.val := by rfl _ = ∏ k ∈ T, a (k + 1) / a k := hreindex _ = a D.card / a 0 := htelescope _ = M.qLocalMass s S hS x / 1 := by simp [a, htop, hzero] _ = M.qLocalMass s S hS x := by simp

Causalean.SCM.ID.component_qLocalMass_ratio_product_prefixIn_of_ne_zero · Causalean/SCM/ID/Density/QFactor/RatioProduct.lean:344
extractDistrict_qLocalMass lemma — Given a finite structural causal model, fixed assignment, ancestral set, and induced district, if the ancestral set is observed, the set is a district of the induced graph, and the observational kernel has positive mass, then for an observed assignment, extracting the district from the ancestral local mass recovers that district's local mass.

hypotheses

N :

Type u_1
N → Type u_2
shared

∀ n, Fintype (Ω n)

∀ n, MeasurableSingletonClass (Ω n)

M :

SCM N Ω

s :

M.FixedValues

A C' :

Finset (SWIGNode N)

hA :

A ⊆ M.observed

hC' :

C' ∈ (M.toSWIGGraph.induce A).cComponentSet

hpos :

DiscreteID.PositiveMass (M.obsKernel s)

x :

ValuesOn M.observed (swigΩ Ω)

conclusion

extractDistrict M.observed (M.toSWIGGraph.induce A) A C' hA (M.qLocalMass s A hA) x
= M.qLocalMass s C' (fun _ hv => hA (by have hHobs : (M.toSWIGGraph.induce A).observed = A := by simp [SWIGGraph.induce, Finset.inter_eq_left.mpr hA] exact hHobs ▸ (M.toSWIGGraph.induce A).cComponentSet_subset_observed C' hC' hv)) x

Proof (Lean source)

lemma extractDistrict_qLocalMass [∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)] (M : SCM N Ω) (s : M.FixedValues) (A C' : Finset (SWIGNode N)) (hA : A ⊆ M.observed) (hC' : C' ∈ (M.toSWIGGraph.induce A).cComponentSet) (hpos : DiscreteID.PositiveMass (M.obsKernel s)) (x : ValuesOn M.observed (swigΩ Ω)) : extractDistrict M.observed (M.toSWIGGraph.induce A) A C' hA (M.qLocalMass s A hA) x = M.qLocalMass s C' (fun _ hv => hA (by have hHobs : (M.toSWIGGraph.induce A).observed = A := by simp [SWIGGraph.induce, Finset.inter_eq_left.mpr hA] exact hHobs ▸ (M.toSWIGGraph.induce A).cComponentSet_subset_observed C' hC' hv)) x := by classical let H := M.toSWIGGraph.induce A have hHobs : H.observed = A := by simp [H, SWIGGraph.induce, Finset.inter_eq_left.mpr hA] have hCobs : C' ⊆ M.observed := by intro v hv exact hA (hHobs ▸ H.cComponentSet_subset_observed C' hC' hv) have hCA : C' ⊆ A := by intro v hv exact hHobs ▸ H.cComponentSet_subset_observed C' hC' hv have hdisj : (↑H.cComponentSet : Set (Finset (SWIGNode N))).Pairwise (fun U U' => Disjoint U U') := by intro U hU V hV hne exact H.cComponentSet_pairwise_disjoint hU hV hne have hmarg : ∀ k, marginalizeOn M.observed (A \ H.prefixIn A k) (fun _ hv => hA ((Finset.mem_sdiff.mp hv).1)) (M.qLocalMass s A hA) x = M.qLocalMass s (H.prefixIn A k) (fun _ hv => hA (H.prefixIn_subset A k hv)) x := by intro k simpa [H] using M.qLocalMass_marginalize_ancestralClosed s A (H.prefixIn A k) hA (H.prefixIn_subset A k) (prefixIn_parent_closed_induce_observed M A hA k) x have hprod : ∀ k, M.qLocalMass s (H.prefixIn A k) (fun _ hv => hA (H.prefixIn_subset A k hv)) x = ∏ C ∈ H.cComponentSet, M.qLocalMass s (C ∩ H.prefixIn A k) (fun _ hv => hA (H.prefixIn_subset A k (mem_of_mem_inter_right hv))) x := by intro k simpa [H] using qLocalMass_prefixIn_eq_prod_induce_components M s A hA k x unfold SCM.extractDistrict calc (∏ i ∈ Finset.univ.filter (fun i : Fin A.card => (H.nodesAt A i).val ∈ C'), marginalizeOn M.observed (A \ H.prefixIn A (i.val + 1)) (fun _ hv => hA ((Finset.mem_sdiff.mp hv).1)) (M.qLocalMass s A hA) x / marginalizeOn M.observed (A \ H.prefixIn A i.val) (fun _ hv => hA ((Finset.mem_sdiff.mp hv).1)) (M.qLocalMass s A hA) x) = ∏ i ∈ Finset.univ.filter (fun i : Fin A.card => (H.nodesAt A i).val ∈ C'), (∏ C ∈ H.cComponentSet, M.qLocalMass s (C ∩ H.prefixIn A (i.val + 1)) (fun _ hv => hA (H.prefixIn_subset A (i.val + 1) (mem_of_mem_inter_right hv))) x) / (∏ C ∈ H.cComponentSet, M.qLocalMass s (C ∩ H.prefixIn A i.val) (fun _ hv => hA (H.prefixIn_subset A i.val (mem_of_mem_inter_right hv))) x) := by refine Finset.prod_congr rfl ?_ intro i _hi rw [hmarg (i.val + 1), hmarg i.val, hprod (i.val + 1), hprod i.val] _ = ∏ i ∈ Finset.univ.filter (fun i : Fin A.card => (H.nodesAt A i).val ∈ C'), M.qLocalMass s (C' ∩ H.prefixIn A (i.val + 1)) (fun _ hv => hA (H.prefixIn_subset A (i.val + 1) (mem_of_mem_inter_right hv))) x / M.qLocalMass s (C' ∩ H.prefixIn A i.val) (fun _ hv => hA (H.prefixIn_subset A i.val (mem_of_mem_inter_right hv))) x := by refine Finset.prod_congr rfl ?_ intro i hi have hiC : (H.nodesAt A i).val ∈ C' := (Finset.mem_filter.mp hi).2 exact prefixIn_qProduct_ratio_eq_component_ratio_of_family M H A s H.cComponentSet C' hC' (fun C hC hne => hdisj hC hC' hne) i hA hiC hpos x _ = M.qLocalMass s C' hCobs x := by simpa using component_qLocalMass_ratio_product_prefixIn M H A s C' hCobs hCA hpos x _ = M.qLocalMass s C' (fun _ hv => hA (by have hHobs' : (M.toSWIGGraph.induce A).observed = A := by simp [SWIGGraph.induce, Finset.inter_eq_left.mpr hA] exact hHobs' ▸ (M.toSWIGGraph.induce A).cComponentSet_subset_observed C' hC' hv)) x := by rfl

Causalean.SCM.ID.extractDistrict_qLocalMass · Causalean/SCM/ID/Density/QFactor/RatioProduct.lean:441
target_subset theorem — The target set of a recursive c-factor reachability certificate is contained in the source set.

hypotheses

N :

Type u_1
SWIGGraph N
Finset (SWIGNode N)
shared

h :

CFactorReachableRec G T C

conclusion

C ⊆ T

Proof (Lean source)

theorem CFactorReachableRec.target_subset {G : SWIGGraph N} {T C : Finset (SWIGNode N)} (h : CFactorReachableRec G T C) : C ⊆ T := by cases h with | base _ hCT _ => exact hCT | step _ hCT _ _ _ => exact hCT

Causalean.SCM.ID.CFactorReachableRec.target_subset · Causalean/SCM/ID/Density/QFactor/RatioProduct.lean:553
qLocalMass_obsProof_irrel lemma — The local q-mass of an observed variable set does not depend on which proof establishes that the set is observed.

hypotheses

N :

Type u_1
N → Type u_2
shared

M :

SCM N Ω

s :

M.FixedValues

T :

Finset (SWIGNode N)

hT hT' :

T ⊆ M.observed

x :

ValuesOn M.observed (swigΩ Ω)

conclusion

M.qLocalMass s T hT x = M.qLocalMass s T hT' x

Proof (Lean source)

lemma qLocalMass_obsProof_irrel (M : SCM N Ω) (s : M.FixedValues) (T : Finset (SWIGNode N)) (hT hT' : T ⊆ M.observed) (x : ValuesOn M.observed (swigΩ Ω)) : M.qLocalMass s T hT x = M.qLocalMass s T hT' x := by unfold SCM.qLocalMass congr 1

Causalean.SCM.ID.qLocalMass_obsProof_irrel · Causalean/SCM/ID/Density/QFactor/RatioProduct.lean:562

TianRecovery 3 core · 0 supporting This file identifies a district density of the post-intervention ancestral law with a mechanism c-factor and, for a full c-component, with the corresponding observational c-component density. ★ tianDistrictDensity_eq_mechCFactor_doModel★ tianDistrictDensity_eq_qLocalMass_div_jointRef_district★ tian_full_cComponent_density_recovery

Tian district-density recovery

This file identifies a district density of the post-intervention ancestral law with a mechanism c-factor and, for a full c-component, with the corresponding observational c-component density. It contains the terminal recovery results assembled from the prefix-mass lemmas and mechanism invariance.

theorem tianDistrictDensity_eq_mechCFactor_doModel reviewed

Causalean.SCM.ID

(B) Tian Lemma 1 for the do-model ancestral marginal. Consider a structural causal model M with an intervention set X whose random copies are observed and whose fixed copies are not already frozen, an outcome set Y disjoint from the random copies of X, under a faithful reference-measure family, a positive observational kernel at every fixed-value assignment, and the standing assumption that M is a standard model. For a set S that is simultaneously a district of the post-intervention ancestral graph and a full c-component of M, and an extension map that inverts the projection onto the ancestral observed coordinates, the Tian district density read off the do(X)-law ancestral marginal at S agrees with the mechanism c-factor of the post-intervention model at the extended point.

Formal statement

hypotheses

N :

Type u_1

N → Type u_2

shared

∀ n, Nonempty (Ω n)

∀ n, Fintype (Ω n)

∀ n, MeasurableSingletonClass (Ω n)

M :

SCM N Ω

X :

hObs :

∀ D ∈ X, SWIGNode.random D ∈ M.observed

hFix :

∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed

Y :

ref :

href :

ReferenceFaithful ref

sDo :

(M.fixSet X hObs hFix).FixedValues

hpos :

∀ s' : M.FixedValues, DiscreteID.PositiveMass (M.obsKernel s')

hYX :

∀ d ∈ X, SWIGNode.random d ∉ Y

hStd :

M.isStandard

S :

hS :

S ∈ fixTruncCComponentSet M X hObs hFix Y

hSfull :

S ∈ M.toSWIGGraph.cComponentSet

IsFiniteMeasure (doObsKernelAncestralMarginal M X hObs hFix Y sDo)

∀ (k : ℕ) (hk : k < (fixObservedAncestralSet M X hObs hFix Y).card),

StandardBorelSpace (ValuesOn ({(((M.fixSet X hObs hFix).toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y)).nodesAt (fixObservedAncestralSet M X hObs hFix Y) ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))

∀ (k : ℕ) (hk : k < (fixObservedAncestralSet M X hObs hFix Y).card),

Nonempty (ValuesOn ({(((M.fixSet X hObs hFix).toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y)).nodesAt (fixObservedAncestralSet M X hObs hFix Y) ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))

extend :

ValuesOn (fixObservedAncestralSet M X hObs hFix Y) (swigΩ Ω) → ValuesOn M.observed (swigΩ Ω)

hExtend :

∀ xD,

valuesProjection (show fixObservedAncestralSet M X hObs hFix Y ⊆ M.observed from inter_subset_right) (extend xD)

= xD

xD :

ValuesOn (fixObservedAncestralSet M X hObs hFix Y) (swigΩ Ω)

conclusion

tianDistrictDensity ((M.fixSet X hObs hFix).toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y)) (fixObservedAncestralSet M X hObs hFix Y) (doObsKernelAncestralMarginal M X hObs hFix Y sDo) ref S xD

= (M.fixSet X hObs hFix).mechCFactor ref S (by have hSobs : S ⊆ M.observed := M.toSWIGGraph.cComponentSet_subset_observed S hSfull simpa [SCM.fixSet_observed] using hSobs) sDo (extend xD)

Proof (Lean source)

theorem tianDistrictDensity_eq_mechCFactor_doModel [∀ n, Nonempty (Ω n)] [∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)] (M : SCM N Ω) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (Y : Finset (SWIGNode N)) (ref : ReferenceMeasures Ω) (href : ReferenceFaithful ref) (sDo : (M.fixSet X hObs hFix).FixedValues) (hpos : ∀ s' : M.FixedValues, DiscreteID.PositiveMass (M.obsKernel s')) (hYX : ∀ d ∈ X, SWIGNode.random d ∉ Y) (hStd : M.isStandard) (S : Finset (SWIGNode N)) (hS : S ∈ fixTruncCComponentSet M X hObs hFix Y) (hSfull : S ∈ M.toSWIGGraph.cComponentSet) [IsFiniteMeasure (doObsKernelAncestralMarginal M X hObs hFix Y sDo)] [∀ (k : ℕ) (hk : k < (fixObservedAncestralSet M X hObs hFix Y).card), StandardBorelSpace (ValuesOn ({(((M.fixSet X hObs hFix).toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y)).nodesAt (fixObservedAncestralSet M X hObs hFix Y) ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ (k : ℕ) (hk : k < (fixObservedAncestralSet M X hObs hFix Y).card), Nonempty (ValuesOn ({(((M.fixSet X hObs hFix).toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y)).nodesAt (fixObservedAncestralSet M X hObs hFix Y) ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] (extend : ValuesOn (fixObservedAncestralSet M X hObs hFix Y) (swigΩ Ω) → ValuesOn M.observed (swigΩ Ω)) (hExtend : ∀ xD, valuesProjection (show fixObservedAncestralSet M X hObs hFix Y ⊆ M.observed from Finset.inter_subset_right) (extend xD) = xD) (xD : ValuesOn (fixObservedAncestralSet M X hObs hFix Y) (swigΩ Ω)) : tianDistrictDensity ((M.fixSet X hObs hFix).toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y)) (fixObservedAncestralSet M X hObs hFix Y) (doObsKernelAncestralMarginal M X hObs hFix Y sDo) ref S xD = (M.fixSet X hObs hFix).mechCFactor ref S (by have hSobs : S ⊆ M.observed := M.toSWIGGraph.cComponentSet_subset_observed S hSfull simpa [SCM.fixSet_observed] using hSobs) sDo (extend xD) := by classical let MX := M.fixSet X hObs hFix let D := fixObservedAncestralSet M X hObs hFix Y let H := MX.toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y) let μ : Measure (ValuesOn D (swigΩ Ω)) := doObsKernelAncestralMarginal M X hObs hFix Y sDo have hDobs : D ⊆ MX.observed := Finset.inter_subset_right have hSdoComp : S ∈ MX.toSWIGGraph.cComponentSet := by exact (fixSet_cComponentSet_mem M X hObs hFix S).mpr hSfull have hSobsMX : S ⊆ MX.observed := MX.toSWIGGraph.cComponentSet_subset_observed S hSdoComp have hSobsM : S ⊆ M.observed := M.toSWIGGraph.cComponentSet_subset_observed S hSfull have hSD : S ⊆ D := by have hSHobs : S ⊆ H.observed := by exact H.cComponentSet_subset_observed S (by simpa [H, MX, fixTruncCComponentSet] using hS) exact hSHobs have hμpos : DiscreteID.PositiveMass μ := by simpa [μ] using doObsKernelAncestralMarginal_positiveMass M X hObs hFix Y hpos hYX sDo have hprefixMass_ne0 : ∀ k, (μ.map (valuesProjection (H.prefixIn_subset D k))) ({valuesProjection (H.prefixIn_subset D k) xD} : Set (ValuesOn (H.prefixIn D k) (swigΩ Ω))) ≠ 0 := by intro k have hmapPos := DiscreteID.PositiveMass.map_valuesProjection (Ω' := swigΩ Ω) hμpos (H.prefixIn_subset D k) simpa [DiscreteID.singletonMass_apply] using hmapPos (valuesProjection (H.prefixIn_subset D k) xD) have hprefixProd_eq : ∀ k, (μ.map (valuesProjection (H.prefixIn_subset D k))) ({valuesProjection (H.prefixIn_subset D k) xD} : Set (ValuesOn (H.prefixIn D k) (swigΩ Ω))) = ∏ C ∈ MX.toSWIGGraph.cComponentSet, MX.qLocalMass sDo (C ∩ H.prefixIn D k) (fun _ hv => hDobs (H.prefixIn_subset D k (mem_of_mem_inter_right hv))) (extend xD) := by intro k simpa [MX, D, H, μ, hDobs] using doObsKernelAncestralMarginal_prefix_singleton_eq_prod_qLocalMass M X hObs hFix Y sDo extend hExtend k xD have hprefixProd_ne0 : ∀ k, (∏ C ∈ MX.toSWIGGraph.cComponentSet, MX.qLocalMass sDo (C ∩ H.prefixIn D k) (fun _ hv => hDobs (H.prefixIn_subset D k (mem_of_mem_inter_right hv))) (extend xD)) ≠ 0 := by intro k hzero exact hprefixMass_ne0 k (by rw [hprefixProd_eq k, hzero]) have hfactor_ne0 : ∀ k C, C ∈ MX.toSWIGGraph.cComponentSet → MX.qLocalMass sDo (C ∩ H.prefixIn D k) (fun _ hv => hDobs (H.prefixIn_subset D k (mem_of_mem_inter_right hv))) (extend xD) ≠ 0 := by intro k C hC exact (Finset.prod_ne_zero_iff.mp (hprefixProd_ne0 k)) C hC have hS_q_ne0 : ∀ k ≤ D.card, MX.qLocalMass sDo (S ∩ H.prefixIn D k) (fun _ hv => hSobsMX (mem_of_mem_inter_left hv)) (extend xD) ≠ 0 := by intro k _hk simpa [hDobs, hSobsMX] using hfactor_ne0 k S hSdoComp have hpointS : valuesProjection hSobsMX (extend xD) = valuesProjection hSD xD := by have h := valuesProjection_extend_eq_of_subset M (show D ⊆ M.observed from Finset.inter_subset_right) hSD hSobsM extend hExtend xD simpa [MX, SCM.fixSet_observed, hSobsMX, hSobsM] using h have hstep : ∀ i ∈ Finset.univ.filter (fun i : Fin D.card => (H.nodesAt D i).val ∈ S), tianPrefixStepDensity H D μ ref i xD = (MX.qLocalMass sDo (S ∩ H.prefixIn D (i.val + 1)) (fun _ hv => hSobsMX (mem_of_mem_inter_left hv)) (extend xD) / MX.qLocalMass sDo (S ∩ H.prefixIn D i.val) (fun _ hv => hSobsMX (mem_of_mem_inter_left hv)) (extend xD)) / jointRef ref ({(H.nodesAt D i).val} : Finset (SWIGNode N)) ({valuesProjection (show ({(H.nodesAt D i).val} : Finset (SWIGNode N)) ⊆ D from by intro v hv rw [Finset.mem_singleton] at hv exact hv ▸ (H.nodesAt D i).property) xD} : Set (ValuesOn ({(H.nodesAt D i).val} : Finset (SWIGNode N)) (swigΩ Ω))) := by intro i hi have hiS : (H.nodesAt D i).val ∈ S := (Finset.mem_filter.mp hi).2 have hmass := tianPrefixStepDensity_eq_prefix_mass_ratio H D μ ref href i xD (hprefixMass_ne0 i.val) have hrest0 : (∏ C ∈ MX.toSWIGGraph.cComponentSet \ {S}, MX.qLocalMass sDo (C ∩ H.prefixIn D i.val) (fun _ hv => hDobs (H.prefixIn_subset D i.val (mem_of_mem_inter_right hv))) (extend xD)) ≠ 0 := by exact Finset.prod_ne_zero_iff.mpr (by intro C hC exact hfactor_ne0 i.val C (Finset.mem_sdiff.mp hC).1) have hcancel := prefixIn_qProduct_ratio_eq_component_ratio_of_ne_zero MX H D sDo S hSdoComp i hDobs hiS (extend xD) hrest0 calc tianPrefixStepDensity H D μ ref i xD = (((∏ C ∈ MX.toSWIGGraph.cComponentSet, MX.qLocalMass sDo (C ∩ H.prefixIn D (i.val + 1)) (fun _ hv => hDobs (H.prefixIn_subset D (i.val + 1) (mem_of_mem_inter_right hv))) (extend xD)) / (∏ C ∈ MX.toSWIGGraph.cComponentSet, MX.qLocalMass sDo (C ∩ H.prefixIn D i.val) (fun _ hv => hDobs (H.prefixIn_subset D i.val (mem_of_mem_inter_right hv))) (extend xD))) / jointRef ref ({(H.nodesAt D i).val} : Finset (SWIGNode N)) ({valuesProjection (show ({(H.nodesAt D i).val} : Finset (SWIGNode N)) ⊆ D from by intro v hv rw [Finset.mem_singleton] at hv exact hv ▸ (H.nodesAt D i).property) xD} : Set (ValuesOn ({(H.nodesAt D i).val} : Finset (SWIGNode N)) (swigΩ Ω)))) := by rw [hmass, hprefixProd_eq (i.val + 1), hprefixProd_eq i.val] _ = (MX.qLocalMass sDo (S ∩ H.prefixIn D (i.val + 1)) (fun _ hv => hSobsMX (mem_of_mem_inter_left hv)) (extend xD) / MX.qLocalMass sDo (S ∩ H.prefixIn D i.val) (fun _ hv => hSobsMX (mem_of_mem_inter_left hv)) (extend xD)) / jointRef ref ({(H.nodesAt D i).val} : Finset (SWIGNode N)) ({valuesProjection (show ({(H.nodesAt D i).val} : Finset (SWIGNode N)) ⊆ D from by intro v hv rw [Finset.mem_singleton] at hv exact hv ▸ (H.nodesAt D i).property) xD} : Set (ValuesOn ({(H.nodesAt D i).val} : Finset (SWIGNode N)) (swigΩ Ω))) := by rw [hcancel] let idxS := Finset.univ.filter (fun i : Fin D.card => (H.nodesAt D i).val ∈ S) let qratio : Fin D.card → ENNReal := fun i => MX.qLocalMass sDo (S ∩ H.prefixIn D (i.val + 1)) (fun _ hv => hSobsMX (mem_of_mem_inter_left hv)) (extend xD) / MX.qLocalMass sDo (S ∩ H.prefixIn D i.val) (fun _ hv => hSobsMX (mem_of_mem_inter_left hv)) (extend xD) let den : Fin D.card → ENNReal := fun i => jointRef ref ({(H.nodesAt D i).val} : Finset (SWIGNode N)) ({valuesProjection (show ({(H.nodesAt D i).val} : Finset (SWIGNode N)) ⊆ D from by intro v hv rw [Finset.mem_singleton] at hv exact hv ▸ (H.nodesAt D i).property) xD} : Set (ValuesOn ({(H.nodesAt D i).val} : Finset (SWIGNode N)) (swigΩ Ω))) have hden0 : ∀ i ∈ idxS, den i ≠ 0 := by intro i _hi exact jointRef_singleton_ne_zero ref href _ _ have hdentop : ∀ i ∈ idxS, den i ≠ ∞ := by intro i _hi exact ne_of_lt (MeasureTheory.measure_lt_top (jointRef ref ({(H.nodesAt D i).val} : Finset (SWIGNode N))) _) have hqprod : (∏ i ∈ idxS, qratio i) = MX.qLocalMass sDo S hSobsMX (extend xD) := by simpa [idxS, qratio] using component_qLocalMass_ratio_product_prefixIn_of_ne_zero MX H D sDo S hSobsMX hSD (extend xD) hS_q_ne0 have hdenprod : (∏ i ∈ idxS, den i) = jointRef ref S ({valuesProjection hSD xD} : Set (ValuesOn S (swigΩ Ω))) := by have hden_atom : (∏ i ∈ idxS, den i) = ∏ i ∈ idxS, ref.μ (H.nodesAt D i).val ({xD (H.nodesAt D i)} : Set (swigΩ Ω (H.nodesAt D i).val)) := by refine Finset.prod_congr rfl ?_ intro i hi dsimp [den] rw [jointRef_singleton_eq_prod] simp [valuesProjection] rw [hden_atom] simpa [idxS] using component_ref_atom_product_eq_jointRef_prefixIn H D ref S hSD xD have htian : tianDistrictDensity H D μ ref S xD = MX.qLocalMass sDo S hSobsMX (extend xD) / jointRef ref S ({valuesProjection hSD xD} : Set (ValuesOn S (swigΩ Ω))) := by unfold tianDistrictDensity calc (∏ i ∈ Finset.univ.filter (fun i : Fin D.card => (H.nodesAt D i).val ∈ S), tianPrefixStepDensity H D μ ref i xD) = ∏ i ∈ idxS, qratio i / den i := by refine Finset.prod_congr ?_ ?_ · simp [idxS] · intro i hi simpa [idxS, qratio, den] using hstep i (by simpa [idxS] using hi) _ = (∏ i ∈ idxS, qratio i) / (∏ i ∈ idxS, den i) := by exact ENNReal.prod_div_prod idxS qratio den hden0 hdentop -- … truncated; follow the source link for the rest …

Causalean.SCM.ID.tianDistrictDensity_eq_mechCFactor_doModel · Causalean/SCM/ID/Density/QFactor/TianRecovery.lean:40 · uses cComponentSet , induce , nodesAt , SWIGNode , instDecidableEqSWIGNode , instMeasurableSpaceSwigΩ , swigΩ , ValuesOn , valuesProjection , SCM , FixedValues , PositiveMass , doObsKernelAncestralMarginal , fixAncestralSet , fixObservedAncestralSet , fixTruncCComponentSet , tianDistrictDensity , ObservedValues , ReferenceFaithful , ReferenceMeasures , fixSet , isStandard , mechCFactor , obsKernel

theorem tianDistrictDensity_eq_qLocalMass_div_jointRef_district reviewed

Causalean.SCM.ID

Consider an intervention set X whose random copies are observed and whose fixed copies are not already frozen together with an outcome set Y disjoint from the random copies of X, under a faithful reference-measure family and a positive observational kernel at every fixed-value assignment. For any district S of the post-intervention ancestral graph and an extension map inverting the projection onto the ancestral observed coordinates, the Tian district density read off the do(X)-law ancestral marginal at S equals the do-model local q-mass on S divided by the reference atom mass of S.

Formal statement

hypotheses

N :

Type u_1

N → Type u_2

shared

∀ n, Nonempty (Ω n)

∀ n, Fintype (Ω n)

∀ n, MeasurableSingletonClass (Ω n)

M :

SCM N Ω

X :

hObs :

∀ D ∈ X, SWIGNode.random D ∈ M.observed

hFix :

∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed

Y :

ref :

href :

ReferenceFaithful ref

sDo :

(M.fixSet X hObs hFix).FixedValues

hpos :

∀ s' : M.FixedValues, DiscreteID.PositiveMass (M.obsKernel s')

hYX :

∀ d ∈ X, SWIGNode.random d ∉ Y

S :

hS :

S ∈ fixTruncCComponentSet M X hObs hFix Y

IsFiniteMeasure (doObsKernelAncestralMarginal M X hObs hFix Y sDo)

∀ (k : ℕ) (hk : k < (fixObservedAncestralSet M X hObs hFix Y).card),

StandardBorelSpace (ValuesOn ({(((M.fixSet X hObs hFix).toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y)).nodesAt (fixObservedAncestralSet M X hObs hFix Y) ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))

∀ (k : ℕ) (hk : k < (fixObservedAncestralSet M X hObs hFix Y).card),

Nonempty (ValuesOn ({(((M.fixSet X hObs hFix).toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y)).nodesAt (fixObservedAncestralSet M X hObs hFix Y) ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))

extend :

ValuesOn (fixObservedAncestralSet M X hObs hFix Y) (swigΩ Ω) → ValuesOn M.observed (swigΩ Ω)

hExtend :

∀ xD,

valuesProjection (show fixObservedAncestralSet M X hObs hFix Y ⊆ M.observed from inter_subset_right) (extend xD)

= xD

xD :

ValuesOn (fixObservedAncestralSet M X hObs hFix Y) (swigΩ Ω)

conclusion

MX :

M.fixSet X hObs hFix

D :

fixObservedAncestralSet M X hObs hFix Y

H :

MX.toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y)

tianDistrictDensity H D (doObsKernelAncestralMarginal M X hObs hFix Y sDo) ref S xD

= MX.qLocalMass sDo S (show S ⊆ MX.observed from by intro v hv have hSHobs : S ⊆ H.observed := H.cComponentSet_subset_observed S (by simpa [H, MX, fixTruncCComponentSet] using hS) have hvD : v ∈ D := by dsimp [H, D, SWIGGraph.induce, fixObservedAncestralSet] at hSHobs ⊢ exact hSHobs hv exact (Finset.mem_inter.mp hvD).2) (extend xD) / jointRef ref S ({valuesProjection (show S ⊆ D from by intro v hv have hSHobs : S ⊆ H.observed := H.cComponentSet_subset_observed S (by simpa [H, MX, fixTruncCComponentSet] using hS) dsimp [H, D, SWIGGraph.induce, fixObservedAncestralSet] at hSHobs ⊢ exact hSHobs hv) xD} : Set (ValuesOn S (swigΩ Ω)))

Proof (Lean source)

theorem tianDistrictDensity_eq_qLocalMass_div_jointRef_district [∀ n, Nonempty (Ω n)] [∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)] (M : SCM N Ω) (X : Finset N) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (Y : Finset (SWIGNode N)) (ref : ReferenceMeasures Ω) (href : ReferenceFaithful ref) (sDo : (M.fixSet X hObs hFix).FixedValues) (hpos : ∀ s' : M.FixedValues, DiscreteID.PositiveMass (M.obsKernel s')) (hYX : ∀ d ∈ X, SWIGNode.random d ∉ Y) (S : Finset (SWIGNode N)) (hS : S ∈ fixTruncCComponentSet M X hObs hFix Y) [IsFiniteMeasure (doObsKernelAncestralMarginal M X hObs hFix Y sDo)] [∀ (k : ℕ) (hk : k < (fixObservedAncestralSet M X hObs hFix Y).card), StandardBorelSpace (ValuesOn ({(((M.fixSet X hObs hFix).toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y)).nodesAt (fixObservedAncestralSet M X hObs hFix Y) ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ (k : ℕ) (hk : k < (fixObservedAncestralSet M X hObs hFix Y).card), Nonempty (ValuesOn ({(((M.fixSet X hObs hFix).toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y)).nodesAt (fixObservedAncestralSet M X hObs hFix Y) ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] (extend : ValuesOn (fixObservedAncestralSet M X hObs hFix Y) (swigΩ Ω) → ValuesOn M.observed (swigΩ Ω)) (hExtend : ∀ xD, valuesProjection (show fixObservedAncestralSet M X hObs hFix Y ⊆ M.observed from Finset.inter_subset_right) (extend xD) = xD) (xD : ValuesOn (fixObservedAncestralSet M X hObs hFix Y) (swigΩ Ω)) : let MX := M.fixSet X hObs hFix let D := fixObservedAncestralSet M X hObs hFix Y let H := MX.toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y) tianDistrictDensity H D (doObsKernelAncestralMarginal M X hObs hFix Y sDo) ref S xD = MX.qLocalMass sDo S (show S ⊆ MX.observed from by intro v hv have hSHobs : S ⊆ H.observed := H.cComponentSet_subset_observed S (by simpa [H, MX, fixTruncCComponentSet] using hS) have hvD : v ∈ D := by dsimp [H, D, SWIGGraph.induce, fixObservedAncestralSet] at hSHobs ⊢ exact hSHobs hv exact (Finset.mem_inter.mp hvD).2) (extend xD) / jointRef ref S ({valuesProjection (show S ⊆ D from by intro v hv have hSHobs : S ⊆ H.observed := H.cComponentSet_subset_observed S (by simpa [H, MX, fixTruncCComponentSet] using hS) dsimp [H, D, SWIGGraph.induce, fixObservedAncestralSet] at hSHobs ⊢ exact hSHobs hv) xD} : Set (ValuesOn S (swigΩ Ω))) := by classical let MX := M.fixSet X hObs hFix let D := fixObservedAncestralSet M X hObs hFix Y let H := MX.toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y) let μ : Measure (ValuesOn D (swigΩ Ω)) := doObsKernelAncestralMarginal M X hObs hFix Y sDo have hDobs : D ⊆ MX.observed := Finset.inter_subset_right have hScomp : S ∈ H.cComponentSet := by simpa [H, MX, fixTruncCComponentSet] using hS have hSobsMX : S ⊆ MX.observed := by intro v hv have hSHobs : S ⊆ H.observed := H.cComponentSet_subset_observed S hScomp have hvD : v ∈ D := by dsimp [H, D, SWIGGraph.induce, fixObservedAncestralSet] at hSHobs ⊢ exact hSHobs hv exact (Finset.mem_inter.mp hvD).2 have hSD : S ⊆ D := by intro v hv have hSHobs : S ⊆ H.observed := H.cComponentSet_subset_observed S hScomp dsimp [H, D, SWIGGraph.induce, fixObservedAncestralSet] at hSHobs ⊢ exact hSHobs hv have hdisj : (↑H.cComponentSet : Set (Finset (SWIGNode N))).Pairwise (fun U U' => Disjoint U U') := by intro U hU V hV hne exact H.cComponentSet_pairwise_disjoint hU hV hne have hμpos : DiscreteID.PositiveMass μ := by simpa [μ] using doObsKernelAncestralMarginal_positiveMass M X hObs hFix Y hpos hYX sDo have hprefixMass_ne0 : ∀ k, (μ.map (valuesProjection (H.prefixIn_subset D k))) ({valuesProjection (H.prefixIn_subset D k) xD} : Set (ValuesOn (H.prefixIn D k) (swigΩ Ω))) ≠ 0 := by intro k have hmapPos := DiscreteID.PositiveMass.map_valuesProjection (Ω' := swigΩ Ω) hμpos (H.prefixIn_subset D k) simpa [DiscreteID.singletonMass_apply] using hmapPos (valuesProjection (H.prefixIn_subset D k) xD) have hprefixProd_eq : ∀ k, (μ.map (valuesProjection (H.prefixIn_subset D k))) ({valuesProjection (H.prefixIn_subset D k) xD} : Set (ValuesOn (H.prefixIn D k) (swigΩ Ω))) = ∏ C ∈ H.cComponentSet, MX.qLocalMass sDo (C ∩ H.prefixIn D k) (fun _ hv => hDobs (H.prefixIn_subset D k (mem_of_mem_inter_right hv))) (extend xD) := by intro k simpa [MX, D, H, μ, hDobs] using doObsKernelAncestralMarginal_prefix_singleton_eq_prod_H_qLocalMass M X hObs hFix Y sDo extend hExtend k xD have hprefixProd_ne0 : ∀ k, (∏ C ∈ H.cComponentSet, MX.qLocalMass sDo (C ∩ H.prefixIn D k) (fun _ hv => hDobs (H.prefixIn_subset D k (mem_of_mem_inter_right hv))) (extend xD)) ≠ 0 := by intro k hzero exact hprefixMass_ne0 k (by rw [hprefixProd_eq k, hzero]) have hfactor_ne0 : ∀ k C, C ∈ H.cComponentSet → MX.qLocalMass sDo (C ∩ H.prefixIn D k) (fun _ hv => hDobs (H.prefixIn_subset D k (mem_of_mem_inter_right hv))) (extend xD) ≠ 0 := by intro k C hC exact (Finset.prod_ne_zero_iff.mp (hprefixProd_ne0 k)) C hC have hS_q_ne0 : ∀ k ≤ D.card, MX.qLocalMass sDo (S ∩ H.prefixIn D k) (fun _ hv => hSobsMX (mem_of_mem_inter_left hv)) (extend xD) ≠ 0 := by intro k _hk simpa [hDobs, hSobsMX] using hfactor_ne0 k S hScomp have hstep : ∀ i ∈ Finset.univ.filter (fun i : Fin D.card => (H.nodesAt D i).val ∈ S), tianPrefixStepDensity H D μ ref i xD = (MX.qLocalMass sDo (S ∩ H.prefixIn D (i.val + 1)) (fun _ hv => hSobsMX (mem_of_mem_inter_left hv)) (extend xD) / MX.qLocalMass sDo (S ∩ H.prefixIn D i.val) (fun _ hv => hSobsMX (mem_of_mem_inter_left hv)) (extend xD)) / jointRef ref ({(H.nodesAt D i).val} : Finset (SWIGNode N)) ({valuesProjection (show ({(H.nodesAt D i).val} : Finset (SWIGNode N)) ⊆ D from by intro v hv rw [Finset.mem_singleton] at hv exact hv ▸ (H.nodesAt D i).property) xD} : Set (ValuesOn ({(H.nodesAt D i).val} : Finset (SWIGNode N)) (swigΩ Ω))) := by intro i hi have hiS : (H.nodesAt D i).val ∈ S := (Finset.mem_filter.mp hi).2 have hmass := tianPrefixStepDensity_eq_prefix_mass_ratio H D μ ref href i xD (hprefixMass_ne0 i.val) have hrest0 : (∏ C ∈ H.cComponentSet \ {S}, MX.qLocalMass sDo (C ∩ H.prefixIn D i.val) (fun _ hv => hDobs (H.prefixIn_subset D i.val (mem_of_mem_inter_right hv))) (extend xD)) ≠ 0 := by exact Finset.prod_ne_zero_iff.mpr (by intro C hC exact hfactor_ne0 i.val C (Finset.mem_sdiff.mp hC).1) have hcancel := prefixIn_qProduct_ratio_eq_component_ratio_of_family_of_ne_zero MX H D sDo H.cComponentSet S hScomp (fun C hC hne => hdisj hC hScomp hne) i hDobs hiS (extend xD) hrest0 calc tianPrefixStepDensity H D μ ref i xD = (((∏ C ∈ H.cComponentSet, MX.qLocalMass sDo (C ∩ H.prefixIn D (i.val + 1)) (fun _ hv => hDobs (H.prefixIn_subset D (i.val + 1) (mem_of_mem_inter_right hv))) (extend xD)) / (∏ C ∈ H.cComponentSet, MX.qLocalMass sDo (C ∩ H.prefixIn D i.val) (fun _ hv => hDobs (H.prefixIn_subset D i.val (mem_of_mem_inter_right hv))) (extend xD))) / jointRef ref ({(H.nodesAt D i).val} : Finset (SWIGNode N)) ({valuesProjection (show ({(H.nodesAt D i).val} : Finset (SWIGNode N)) ⊆ D from by intro v hv rw [Finset.mem_singleton] at hv exact hv ▸ (H.nodesAt D i).property) xD} : Set (ValuesOn ({(H.nodesAt D i).val} : Finset (SWIGNode N)) (swigΩ Ω)))) := by rw [hmass, hprefixProd_eq (i.val + 1), hprefixProd_eq i.val] _ = (MX.qLocalMass sDo (S ∩ H.prefixIn D (i.val + 1)) (fun _ hv => hSobsMX (mem_of_mem_inter_left hv)) (extend xD) / MX.qLocalMass sDo (S ∩ H.prefixIn D i.val) (fun _ hv => hSobsMX (mem_of_mem_inter_left hv)) (extend xD)) / jointRef ref ({(H.nodesAt D i).val} : Finset (SWIGNode N)) ({valuesProjection (show ({(H.nodesAt D i).val} : Finset (SWIGNode N)) ⊆ D from by intro v hv rw [Finset.mem_singleton] at hv exact hv ▸ (H.nodesAt D i).property) xD} : Set (ValuesOn ({(H.nodesAt D i).val} : Finset (SWIGNode N)) (swigΩ Ω))) := by rw [hcancel] let idxS := Finset.univ.filter (fun i : Fin D.card => (H.nodesAt D i).val ∈ S) let qratio : Fin D.card → ENNReal := fun i => MX.qLocalMass sDo (S ∩ H.prefixIn D (i.val + 1)) (fun _ hv => hSobsMX (mem_of_mem_inter_left hv)) (extend xD) / MX.qLocalMass sDo (S ∩ H.prefixIn D i.val) (fun _ hv => hSobsMX (mem_of_mem_inter_left hv)) (extend xD) let den : Fin D.card → ENNReal := fun i => jointRef ref ({(H.nodesAt D i).val} : Finset (SWIGNode N)) ({valuesProjection (show ({(H.nodesAt D i).val} : Finset (SWIGNode N)) ⊆ D from by intro v hv rw [Finset.mem_singleton] at hv exact hv ▸ (H.nodesAt D i).property) xD} : Set (ValuesOn ({(H.nodesAt D i).val} : Finset (SWIGNode N)) (swigΩ Ω))) have hden0 : ∀ i ∈ idxS, den i ≠ 0 := by intro i _hi exact jointRef_singleton_ne_zero ref href _ _ have hdentop : ∀ i ∈ idxS, den i ≠ ∞ := by intro i _hi exact ne_of_lt (MeasureTheory.measure_lt_top (jointRef ref ({(H.nodesAt D i).val} : Finset (SWIGNode N))) _) have hqprod : (∏ i ∈ idxS, qratio i) = MX.qLocalMass sDo S hSobsMX (extend xD) := by simpa [idxS, qratio] using component_qLocalMass_ratio_product_prefixIn_of_ne_zero MX H D sDo S hSobsMX hSD (extend xD) hS_q_ne0 have hdenprod : (∏ i ∈ idxS, den i) = jointRef ref S ({valuesProjection hSD xD} : Set (ValuesOn S (swigΩ Ω))) := by have hden_atom : (∏ i ∈ idxS, den i) = ∏ i ∈ idxS, ref.μ (H.nodesAt D i).val ({xD (H.nodesAt D i)} : Set (swigΩ Ω (H.nodesAt D i).val)) := by refine Finset.prod_congr rfl ?_ intro i hi dsimp [den] rw [jointRef_singleton_eq_prod] simp [valuesProjection] rw [hden_atom] -- … truncated; follow the source link for the rest …

Causalean.SCM.ID.tianDistrictDensity_eq_qLocalMass_div_jointRef_district · Causalean/SCM/ID/Density/QFactor/TianRecovery.lean:311 · uses SWIGGraph , induce , nodesAt , SWIGNode , instDecidableEqSWIGNode , instMeasurableSpaceSwigΩ , swigΩ , ValuesOn , valuesProjection , SCM , FixedValues , PositiveMass , doObsKernelAncestralMarginal , fixAncestralSet , fixObservedAncestralSet , fixTruncCComponentSet , tianDistrictDensity , ObservedValues , ReferenceFaithful , ReferenceMeasures , fixSet , jointRef , obsKernel , qLocalMass

lemma tian_full_cComponent_density_recovery reviewed

Causalean.SCM.ID

District recovery by c-factor projection consistency. Consider a standard structural causal model M with an intervention set X whose random copies are observed and whose fixed copies are not already frozen, under a faithful reference-measure family and a positive observational kernel at every fixed-value assignment, for an outcome set Y disjoint from the random copies of X. For a set S that is simultaneously a district of the post-intervention ancestral graph and a full c-component of M, and an extension map that inverts the projection onto the ancestral observed coordinates and reproduces the intervention values sDo on the intervened coordinates, the Tian district density read off the do(X)-law ancestral marginal at S agrees, almost everywhere with respect to the product reference measure on the ancestral observed coordinates, with the observational c-component density factor at S pulled back through the extension.

Formal statement

hypotheses

N :

Type u_1

N → Type u_2

shared

∀ n, Nonempty (Ω n)

∀ n, Fintype (Ω n)

∀ n, MeasurableSingletonClass (Ω n)

M :

SCM N Ω

X :

hStd :

M.isStandard

hObs :

∀ D ∈ X, SWIGNode.random D ∈ M.observed

hFix :

∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed

Y :

ref :

href :

ReferenceFaithful ref

sDo :

(M.fixSet X hObs hFix).FixedValues

S :

hS :

S ∈ fixTruncCComponentSet M X hObs hFix Y

hSfull :

S ∈ M.toSWIGGraph.cComponentSet

IsFiniteMeasure (doObsKernelAncestralMarginal M X hObs hFix Y sDo)

∀ s' : M.FixedValues, IsFiniteMeasure (M.obsKernel s')

∀ (k : ℕ) (hk : k < (fixObservedAncestralSet M X hObs hFix Y).card),

StandardBorelSpace (ValuesOn ({(((M.fixSet X hObs hFix).toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y)).nodesAt (fixObservedAncestralSet M X hObs hFix Y) ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))

∀ (k : ℕ) (hk : k < (fixObservedAncestralSet M X hObs hFix Y).card),

Nonempty (ValuesOn ({(((M.fixSet X hObs hFix).toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y)).nodesAt (fixObservedAncestralSet M X hObs hFix Y) ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))

∀ (k : ℕ) (hk : k < M.observed.card),

StandardBorelSpace (ValuesOn ({(M.observedAt ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))

∀ (k : ℕ) (hk : k < M.observed.card),

Nonempty (ValuesOn ({(M.observedAt ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))

∀ k : ℕ,

CountableOrCountablyGenerated M.FixedValues (ValuesOn (M.prefixNodes k) (swigΩ Ω))

hpos :

∀ s' : M.FixedValues, DiscreteID.PositiveMass (M.obsKernel s')

hYX :

∀ D ∈ X, SWIGNode.random D ∉ Y

extend :

ValuesOn (fixObservedAncestralSet M X hObs hFix Y) (swigΩ Ω) → ValuesOn M.observed (swigΩ Ω)

hExtend :

∀ xD,

valuesProjection (show fixObservedAncestralSet M X hObs hFix Y ⊆ M.observed from inter_subset_right) (extend xD)

= xD

hExtendX :

∀ xD (D : N) (hD : D ∈ X),

extend xD ⟨SWIGNode.random D, hObs D hD⟩

= sDo ⟨SWIGNode.fixed D, mem_union_right _ (Finset.mem_image.mpr ⟨D, hD, rfl⟩)⟩

conclusion

D :

fixObservedAncestralSet M X hObs hFix Y

H :

(M.fixSet X hObs hFix).toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y)

tianDistrictDensity H D (doObsKernelAncestralMarginal M X hObs hFix Y sDo) ref S

=ᵐ[jointRef ref D] fun xD => M.cComponentDensityFactor ref (M.fixSetProj X hObs hFix sDo) S (extend xD)

Proof (Lean source)

lemma tian_full_cComponent_density_recovery [∀ n, Nonempty (Ω n)] [∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)] (M : SCM N Ω) (X : Finset N) (hStd : M.isStandard) (hObs : ∀ D ∈ X, SWIGNode.random D ∈ M.observed) (hFix : ∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed) (Y : Finset (SWIGNode N)) (ref : ReferenceMeasures Ω) (href : ReferenceFaithful ref) (sDo : (M.fixSet X hObs hFix).FixedValues) (S : Finset (SWIGNode N)) (hS : S ∈ fixTruncCComponentSet M X hObs hFix Y) (hSfull : S ∈ M.toSWIGGraph.cComponentSet) [IsFiniteMeasure (doObsKernelAncestralMarginal M X hObs hFix Y sDo)] [∀ s' : M.FixedValues, IsFiniteMeasure (M.obsKernel s')] [∀ (k : ℕ) (hk : k < (fixObservedAncestralSet M X hObs hFix Y).card), StandardBorelSpace (ValuesOn ({(((M.fixSet X hObs hFix).toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y)).nodesAt (fixObservedAncestralSet M X hObs hFix Y) ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ (k : ℕ) (hk : k < (fixObservedAncestralSet M X hObs hFix Y).card), Nonempty (ValuesOn ({(((M.fixSet X hObs hFix).toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y)).nodesAt (fixObservedAncestralSet M X hObs hFix Y) ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ (k : ℕ) (hk : k < M.observed.card), StandardBorelSpace (ValuesOn ({(M.observedAt ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ (k : ℕ) (hk : k < M.observed.card), Nonempty (ValuesOn ({(M.observedAt ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ k : ℕ, CountableOrCountablyGenerated M.FixedValues (ValuesOn (M.prefixNodes k) (swigΩ Ω))] (hpos : ∀ s' : M.FixedValues, DiscreteID.PositiveMass (M.obsKernel s')) (hYX : ∀ D ∈ X, SWIGNode.random D ∉ Y) (extend : ValuesOn (fixObservedAncestralSet M X hObs hFix Y) (swigΩ Ω) → ValuesOn M.observed (swigΩ Ω)) (hExtend : ∀ xD, valuesProjection (show fixObservedAncestralSet M X hObs hFix Y ⊆ M.observed from inter_subset_right) (extend xD) = xD) (hExtendX : ∀ xD (D : N) (hD : D ∈ X), extend xD ⟨SWIGNode.random D, hObs D hD⟩ = sDo ⟨SWIGNode.fixed D, mem_union_right _ (Finset.mem_image.mpr ⟨D, hD, rfl⟩)⟩) : let D := fixObservedAncestralSet M X hObs hFix Y let H := (M.fixSet X hObs hFix).toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y) tianDistrictDensity H D (doObsKernelAncestralMarginal M X hObs hFix Y sDo) ref S =ᵐ[jointRef ref D] fun xD => M.cComponentDensityFactor ref (M.fixSetProj X hObs hFix sDo) S (extend xD) := by classical let D := fixObservedAncestralSet M X hObs hFix Y let H := (M.fixSet X hObs hFix).toSWIGGraph.induce (fixAncestralSet M X hObs hFix Y) have hSobs : S ⊆ M.observed := M.toSWIGGraph.cComponentSet_subset_observed S hSfull have hSD : S ⊆ D := by have hSHobs : S ⊆ H.observed := by exact H.cComponentSet_subset_observed S (by simpa [H, fixTruncCComponentSet] using hS) exact hSHobs have hSX : ∀ n ∈ X, SWIGNode.random n ∉ S := by intro n hn hnS have hnD : SWIGNode.random n ∈ D := hSD hnS have hnA : SWIGNode.random n ∈ fixAncestralSet M X hObs hFix Y := by simpa [D, fixObservedAncestralSet] using (Finset.mem_inter.mp hnD).1 exact hYX n hn ((random_intervened_mem_fixAncestralSet_iff_mem_Y M X hObs hFix Y hn).mp hnA) filter_upwards with xD have hB : tianDistrictDensity H D (doObsKernelAncestralMarginal M X hObs hFix Y sDo) ref S xD = (M.fixSet X hObs hFix).mechCFactor ref S (by simpa [SCM.fixSet_observed] using hSobs) sDo (extend xD) := by simpa [H, D] using tianDistrictDensity_eq_mechCFactor_doModel M X hObs hFix Y ref href sDo hpos hYX hStd S hS hSfull extend hExtend xD have hC : (M.fixSet X hObs hFix).mechCFactor ref S (by simpa [SCM.fixSet_observed] using hSobs) sDo (extend xD) = M.mechCFactor ref S hSobs (M.fixSetProj X hObs hFix sDo) (extend xD) := by simpa using mechCFactor_fixSet_invariant M ref X href hStd hObs hFix S hSobs hSX sDo (extend xD) (fun D hD => hExtendX xD D hD) have hA : M.mechCFactor ref S hSobs (M.fixSetProj X hObs hFix sDo) (extend xD) = M.cComponentDensityFactor ref (M.fixSetProj X hObs hFix sDo) S (extend xD) := by exact (cComponentDensityFactor_eq_mechCFactor M ref (M.fixSetProj X hObs hFix sDo) hStd S hSobs hSfull href (hpos (M.fixSetProj X hObs hFix sDo)) (extend xD)).symm exact hB.trans (hC.trans hA)

Causalean.SCM.ID.tian_full_cComponent_density_recovery · Causalean/SCM/ID/Density/QFactor/TianRecovery.lean:584 · uses SWIGGraph , cComponentSet , induce , nodesAt , SWIGNode , instDecidableEqSWIGNode , instMeasurableSpaceSwigΩ , swigΩ , ValuesOn , valuesProjection , SCM , FixedValues , PositiveMass , doObsKernelAncestralMarginal , fixAncestralSet , fixObservedAncestralSet , fixTruncCComponentSet , tianDistrictDensity , ObservedValues , ReferenceFaithful , ReferenceMeasures , cComponentDensityFactor , fixSet , fixSetProj , isStandard , jointRef , obsKernel , observedAt , prefixNodes

TianRecoveryLemmas 1 core · 6 supporting This file relates prefix singleton masses, reference atoms, local q-masses, and Tian prefix-step densities. ★ doObsKernelAncestralMarginal_prefix_singleton_eq_prod_H_qLocalMass

Point-mass lemmas for Tian density recovery

This file relates prefix singleton masses, reference atoms, local q-masses, and Tian prefix-step densities. These lemmas supply the pointwise calculations used by the district-recovery theorems in TianRecovery.

lemma doObsKernelAncestralMarginal_prefix_singleton_eq_prod_H_qLocalMass reviewed

Causalean.SCM.ID

For a finite structural causal model with finite measurable node-value spaces, an intervention set, evidence that its random copies are observed, evidence that its fixed copies are not already fixed, an outcome set, a fixed-node assignment after intervention, an extension from the ancestral observed margin to the original observed space, proof that extension preserves that margin, a prefix length, and a realization on the ancestral margin, the intervened observational law's singleton mass on that prefix equals the product of the induced graph's local q-masses over its c-components.

Formal statement

hypotheses

N :

Type u_1

N → Type u_2

shared

∀ n, Fintype (Ω n)

∀ n, MeasurableSingletonClass (Ω n)

M :

SCM N Ω

X :

hObs :

∀ D ∈ X, SWIGNode.random D ∈ M.observed

hFix :

∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed

Y :