SCM.ID.Density.QMass

For a structural causal model with finitely many values per variable, the local q-mass of a set S of observed nodes at an observed assignment is the probability, under the product law of the latent noises, that every str

Basic 3 core · 5 supporting This file develops the basic finite-mass calculus for qLocalMass: point-value updates, one-coordinate summation, and marginalization over ancestrally closed sets. ★ qLocalMass_marginalize_ancestralClosed

Elimination and marginalization for local q-masses

This file develops the basic finite-mass calculus for qLocalMass: point-value updates, one-coordinate summation, and marginalization over ancestrally closed sets. These operations are the mass-level substrate for later component factorization and recursive district extraction.

def qLocalMass reviewed
Causalean.SCM

For a structural causal model, a fixed-value assignment, a finite set of observed SWIG vertices, contained in the model's observed-node set, and an assignment of values to all observed SWIG vertices, the local q-mass is the latent-product mass of latent-variable assignments for which every vertex in the specified set satisfies its local structural consistency condition at those fixed and observed values.

Definition (Lean source)
parameters
N :
Type u_1
N → Type u_2
shared
M :
SCM N Ω
s :
M.FixedValues
T :
Finset (SWIGNode N)
hT :
T ⊆ M.observed
x :
ValuesOn M.observed (swigΩ Ω)
def
qLocalMass M s T hT x :
ENNReal
given by
M.latentProduct {ℓ | ∀ v (hv : v ∈ T), M.localConsistent s x v (hT hv) ℓ}
Causalean.SCM.qLocalMass · Causalean/SCM/ID/Density/QMass/Basic.lean:41 · uses SWIGNode , swigΩ , ValuesOn , SCM , FixedValues
def singletonValuePt reviewed
Causalean.SCM

A value at one SWIG node is packaged as an assignment on the singleton set containing that node. This helper is used when conditioning or overriding a model with one node's specified value.

Definition (Lean source)
parameters
N :
Type u_1
N → Type u_2
shared
v :
SWIGNode N
ω :
swigΩ Ω v
def
singletonValuePt v ω :
ValuesOn ({v} : Finset (SWIGNode N)) (swigΩ Ω)
given by
fun i => cast (congrArg (swigΩ Ω) (Finset.mem_singleton.mp i.property).symm) ω
Causalean.SCM.singletonValuePt · Causalean/SCM/ID/Density/QMass/Basic.lean:85 · uses SWIGNode , swigΩ , ValuesOn
lemma qLocalMass_marginalize_ancestralClosed reviewed
Causalean.SCM

For a set of observed nodes T and a subset W of T such that every parent, within T, of a node in W also lies in W, marginalizing the local q-mass on T over the coordinates in T \ W yields the local q-mass on W.

Formal statement
hypotheses
N :
Type u_1
N → Type u_2
shared
∀ n, Fintype (Ω n)
∀ n, MeasurableSingletonClass (Ω n)
M :
SCM N Ω
s :
M.FixedValues
T W :
Finset (SWIGNode N)
hT :
T ⊆ M.observed
hWT :
W ⊆ T
hclosed :
∀ v ∈ T, ∀ w ∈ W, M.dag.edge v w → v ∈ W
x :
ValuesOn M.observed (swigΩ Ω)
conclusion
marginalizeOn M.observed (T \ W) (fun _ hv => hT ((Finset.mem_sdiff.mp hv).1)) (M.qLocalMass s T hT) x
= M.qLocalMass s W (fun _ hv => hT (hWT hv)) x
Proof (Lean source)
lemma qLocalMass_marginalize_ancestralClosed [∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)] (M : SCM N Ω) (s : M.FixedValues) (T W : Finset (SWIGNode N)) (hT : T ⊆ M.observed) (hWT : W ⊆ T) (hclosed : ∀ v ∈ T, ∀ w ∈ W, M.dag.edge v w → v ∈ W) (x : ValuesOn M.observed (swigΩ Ω)) : marginalizeOn M.observed (T \ W) (fun _ hv => hT ((Finset.mem_sdiff.mp hv).1)) (M.qLocalMass s T hT) x = M.qLocalMass s W (fun _ hv => hT (hWT hv)) x := by classical let P : Nat → Prop := fun n => ∀ (T : Finset (SWIGNode N)) (hT : T ⊆ M.observed) (hWT : W ⊆ T), (∀ v ∈ T, ∀ w ∈ W, M.dag.edge v w → v ∈ W) → ∀ x : ValuesOn M.observed (swigΩ Ω), (T \ W).card = n → marginalizeOn M.observed (T \ W) (fun _ hv => hT ((Finset.mem_sdiff.mp hv).1)) (M.qLocalMass s T hT) x = M.qLocalMass s W (fun _ hv => hT (hWT hv)) x have hP : ∀ n, P n := by intro n induction n using Nat.strong_induction_on with | h n ih => intro T hT hWT hclosed x hcard by_cases hempty : T \ W = ∅ · have hTW : T ⊆ W := by intro v hvT by_contra hvW have hvS : v ∈ T \ W := Finset.mem_sdiff.mpr ⟨hvT, hvW⟩ simp [hempty] at hvS have hEq : T = W := Finset.Subset.antisymm hTW hWT subst T simpa [Finset.sdiff_self] using (marginalizeOn_empty M (M.qLocalMass s W hT) x) · have hne : (T \ W).Nonempty := Finset.nonempty_iff_ne_empty.mpr hempty obtain ⟨v, hvS, hNoChild⟩ := exists_sdiff_topoMax_noChild M hne hclosed let U : Finset (SWIGNode N) := (T \ W).erase v have hvT : v ∈ T := (Finset.mem_sdiff.mp hvS).1 have hvNotW : v ∉ W := (Finset.mem_sdiff.mp hvS).2 have hvNotU : v ∉ U := by dsimp [U] simp have hS_eq : T \ W = insert v U := by dsimp [U] exact (Finset.insert_erase hvS).symm have hUobs : U ⊆ M.observed := by intro u hu exact hT ((Finset.mem_sdiff.mp (mem_of_mem_erase hu)).1) have hInsobs : insert v U ⊆ M.observed := by intro u hu have huS : u ∈ T \ W := by simpa [hS_eq] using hu exact hT ((Finset.mem_sdiff.mp huS).1) let hTerase : T.erase v ⊆ M.observed := fun _ hv => hT (mem_of_mem_erase hv) have hfun : (fun x' : ValuesOn M.observed (swigΩ Ω) => ∑ ω : swigΩ Ω v, M.qLocalMass s T hT (overrideOn x' (singletonValuePt v ω))) = (fun x' : ValuesOn M.observed (swigΩ Ω) => M.qLocalMass s (T.erase v) hTerase x') := by funext x' simpa using (qLocalMass_sum_point_eliminate M s T hT hvT hNoChild x') have hEraseSdiff : (T.erase v) \ W = U := by dsimp [U] exact erase_sdiff_eq_sdiff_erase have hcard_lt : ((T.erase v) \ W).card < n := by rw [hEraseSdiff] dsimp [U] rw [← hcard] exact Finset.card_erase_lt_of_mem hvS have hWTerase : W ⊆ T.erase v := by intro w hw refine Finset.mem_erase.mpr ⟨?_, hWT hw⟩ intro hwv exact hvNotW (by simpa [hwv] using hw) have hclosedErase : ∀ a ∈ T.erase v, ∀ w ∈ W, M.dag.edge a w → a ∈ W := by intro a ha w hw haw exact hclosed a (mem_of_mem_erase ha) w hw haw calc marginalizeOn M.observed (T \ W) (fun _ hv => hT ((Finset.mem_sdiff.mp hv).1)) (M.qLocalMass s T hT) x = marginalizeOn M.observed (insert v U) hInsobs (M.qLocalMass s T hT) x := by exact marginalizeOn_congr_finset M hS_eq (fun _ hv => hT ((Finset.mem_sdiff.mp hv).1)) hInsobs (M.qLocalMass s T hT) x _ = marginalizeOn M.observed U hUobs (fun x' => ∑ ω : swigΩ Ω v, M.qLocalMass s T hT (overrideOn x' (singletonValuePt v ω))) x := by exact marginalizeOn_insert M hvNotU hInsobs hUobs (M.qLocalMass s T hT) x _ = marginalizeOn M.observed U hUobs (M.qLocalMass s (T.erase v) hTerase) x := by rw [hfun] _ = marginalizeOn M.observed ((T.erase v) \ W) (fun _ hv => hTerase ((Finset.mem_sdiff.mp hv).1)) (M.qLocalMass s (T.erase v) hTerase) x := by exact marginalizeOn_congr_finset M hEraseSdiff.symm hUobs (fun _ hv => hTerase ((Finset.mem_sdiff.mp hv).1)) (M.qLocalMass s (T.erase v) hTerase) x _ = M.qLocalMass s W (fun _ hv => hT (hWT hv)) x := by have hIH := ih ((T.erase v) \ W).card hcard_lt (T.erase v) hTerase hWTerase hclosedErase x rfl simpa [hTerase] using hIH exact hP (T \ W).card T hT hWT hclosed x rfl
Causalean.SCM.qLocalMass_marginalize_ancestralClosed · Causalean/SCM/ID/Density/QMass/Basic.lean:535 · uses SWIGNode , instFintype , instDecidableEqSWIGNode , swigΩ , ValuesOn , SCM , FixedValues , marginalizeOn , qLocalMass
5 supporting declarations (lemmas, instances)
  • qLocalMass_eq lemma — The local q-mass of an observed subset is the latent-product mass of the set of latent draws that make every node of that subset locally consistent with the given fixed values and observed values.
    hypotheses
    N :
    Type u_1
    N → Type u_2
    shared
    M :
    SCM N Ω
    s :
    M.FixedValues
    T :
    Finset (SWIGNode N)
    hT :
    T ⊆ M.observed
    x :
    ValuesOn M.observed (swigΩ Ω)
    conclusion
    M.qLocalMass s T hT x
    = M.latentProduct {ℓ | ∀ v (hv : v ∈ T), M.localConsistent s x v (hT hv) ℓ}
    Proof (Lean source)
    @[causal_defs_simps] lemma qLocalMass_eq (M : SCM N Ω) (s : M.FixedValues) (T : Finset (SWIGNode N)) (hT : T ⊆ M.observed) (x : ValuesOn M.observed (swigΩ Ω)) : M.qLocalMass s T hT x = M.latentProduct {ℓ | ∀ v (hv : v ∈ T), M.localConsistent s x v (hT hv) ℓ} := rfl
    Causalean.SCM.qLocalMass_eq · Causalean/SCM/ID/Density/QMass/Basic.lean:54
  • qLocalMass_empty lemma — The empty local q-mass is one.
    hypotheses
    N :
    Type u_1
    N → Type u_2
    shared
    M :
    SCM N Ω
    s :
    M.FixedValues
    x :
    ValuesOn M.observed (swigΩ Ω)
    conclusion
    M.qLocalMass s ∅ (by simp) x = 1
    Proof (Lean source)
    @[simp] lemma qLocalMass_empty (M : SCM N Ω) (s : M.FixedValues) (x : ValuesOn M.observed (swigΩ Ω)) : M.qLocalMass s ∅ (by simp) x = 1 := by simp [causal_defs_simps]
    Causalean.SCM.qLocalMass_empty · Causalean/SCM/ID/Density/QMass/Basic.lean:67
  • qLocalMass_anti lemma — Local q-mass is antitone in the constrained observed set.
    hypotheses
    N :
    Type u_1
    N → Type u_2
    shared
    M :
    SCM N Ω
    s :
    M.FixedValues
    T T' :
    Finset (SWIGNode N)
    hTT' :
    T ⊆ T'
    hT :
    T ⊆ M.observed
    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_anti (M : SCM N Ω) (s : M.FixedValues) {T T' : Finset (SWIGNode N)} (hTT' : T ⊆ T') (hT : T ⊆ M.observed) (hT' : T' ⊆ M.observed) (x : ValuesOn M.observed (swigΩ Ω)) : M.qLocalMass s T' hT' x ≤ M.qLocalMass s T hT x := by apply MeasureTheory.measure_mono intro ℓ hℓ v hv exact hℓ v (hTT' hv)
    Causalean.SCM.qLocalMass_anti · Causalean/SCM/ID/Density/QMass/Basic.lean:74
  • marginalizeOn_empty lemma — Marginalizing a mass function over an empty set of observed coordinates leaves its value at every observed assignment unchanged.
    hypotheses
    N :
    Type u_1
    N → Type u_2
    shared
    ∀ n, Fintype (Ω n)
    M :
    SCM N Ω
    q :
    ValuesOn M.observed (swigΩ Ω) → ENNReal
    x :
    ValuesOn M.observed (swigΩ Ω)
    conclusion
    marginalizeOn M.observed ∅ (by simp) q x = q x
    Proof (Lean source)
    lemma marginalizeOn_empty [∀ n, Fintype (Ω n)] (M : SCM N Ω) (q : ValuesOn M.observed (swigΩ Ω) → ENNReal) (x : ValuesOn M.observed (swigΩ Ω)) : marginalizeOn M.observed ∅ (by simp) q x = q x := by classical unfold marginalizeOn let y0 : ValuesOn (∅ : Finset (SWIGNode N)) (swigΩ Ω) := fun i => False.elim (notMem_empty i.val i.property) rw [Finset.sum_eq_single y0] · congr funext i simp · intro y _hy hy exact (hy (Subsingleton.elim y y0)).elim · intro hy exact (hy (Finset.mem_univ y0)).elim
    Causalean.SCM.marginalizeOn_empty · Causalean/SCM/ID/Density/QMass/Basic.lean:180
  • qLocalMass_sum_point_eliminate lemma — Summing a local q-mass over one childless observed coordinate removes that coordinate from the constrained set.
    hypotheses
    N :
    Type u_1
    N → Type u_2
    shared
    ∀ n, Fintype (Ω n)
    ∀ n, MeasurableSingletonClass (Ω n)
    M :
    SCM N Ω
    s :
    M.FixedValues
    T :
    Finset (SWIGNode N)
    hT :
    T ⊆ M.observed
    v :
    SWIGNode N
    hvT :
    v ∈ T
    hNoChild :
    ∀ w ∈ T, ¬ M.dag.edge v w
    x :
    ValuesOn M.observed (swigΩ Ω)
    conclusion
    (∑ ω : swigΩ Ω v, M.qLocalMass s T hT (overrideOn x (singletonValuePt v ω)))
    = M.qLocalMass s (T.erase v) (fun _ hv => hT (mem_of_mem_erase hv)) x
    Proof (Lean source)
    lemma qLocalMass_sum_point_eliminate [∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)] (M : SCM N Ω) (s : M.FixedValues) (T : Finset (SWIGNode N)) (hT : T ⊆ M.observed) {v : SWIGNode N} (hvT : v ∈ T) (hNoChild : ∀ w ∈ T, ¬ M.dag.edge v w) (x : ValuesOn M.observed (swigΩ Ω)) : (∑ ω : swigΩ Ω v, M.qLocalMass s T hT (overrideOn x (singletonValuePt v ω))) = M.qLocalMass s (T.erase v) (fun _ hv => hT (mem_of_mem_erase hv)) x := by classical let Erest : Set M.LatentValues := {ℓ | ∀ w (hw : w ∈ T.erase v), M.localConsistent s x w (hT (mem_of_mem_erase hw)) ℓ} let Fset : swigΩ Ω v → Set M.LatentValues := fun ω => {ℓ | localStructValue M s x v (hT hvT) ℓ = ω} have hevent : ∀ ω : swigΩ Ω v, {ℓ : M.LatentValues | ∀ w (hw : w ∈ T), M.localConsistent s (overrideOn x (singletonValuePt v ω)) w (hT hw) ℓ} = Erest ∩ Fset ω := by intro ω simpa [Erest, Fset] using qLocalEvent_override_singleton_eq_inter M s hT hvT hNoChild x ω have hdisj : PairwiseDisjoint (↑(Finset.univ : Finset (swigΩ Ω v))) (fun ω => Erest ∩ Fset ω) := by intro ω₁ _ ω₂ _ hne change Disjoint (Erest ∩ Fset ω₁) (Erest ∩ Fset ω₂) rw [Set.disjoint_left] intro ℓ hℓ₁ hℓ₂ exact hne (hℓ₁.2.symm.trans hℓ₂.2) have hmeas : ∀ ω ∈ (Finset.univ : Finset (swigΩ Ω v)), MeasurableSet (Erest ∩ Fset ω) := by intro ω _hω exact Set.Finite.measurableSet (Set.toFinite _) have hunion : (⋃ ω ∈ (Finset.univ : Finset (swigΩ Ω v)), Erest ∩ Fset ω) = Erest := by ext ℓ simp [Fset] simp only [causal_defs_simps] calc (∑ ω : swigΩ Ω v, M.latentProduct {ℓ : M.LatentValues | ∀ w (hw : w ∈ T), M.localConsistent s (overrideOn x (singletonValuePt v ω)) w (hT hw) ℓ}) = ∑ ω : swigΩ Ω v, M.latentProduct (Erest ∩ Fset ω) := by refine Finset.sum_congr rfl ?_ intro ω _hω rw [hevent ω] _ = M.latentProduct (⋃ ω ∈ (Finset.univ : Finset (swigΩ Ω v)), Erest ∩ Fset ω) := by symm simpa using (MeasureTheory.measure_biUnion_finset (μ := M.latentProduct) (s := (Finset.univ : Finset (swigΩ Ω v))) (f := fun ω => Erest ∩ Fset ω) hdisj hmeas) _ = M.latentProduct Erest := by rw [hunion]
    Causalean.SCM.qLocalMass_sum_point_eliminate · Causalean/SCM/ID/Density/QMass/Basic.lean:440
Factorization 2 core · 4 supporting This file splits local-consistency events and their latent-product masses over disjoint latent blocks. ★ qLocalMass_prod_of_latentBlock_disjoint★ obsKernel_marginal_singleton_eq_prod_qLocalMass

C-component factorization of local q-masses

This file splits local-consistency events and their latent-product masses over disjoint latent blocks. Its main result expresses an observational marginal atom as the product of the local q-masses of the graph's c-components.

lemma qLocalMass_prod_of_latentBlock_disjoint reviewed
Causalean.SCM

For a finite family 𝒞 of observed node sets whose latent parent blocks are pairwise disjoint, the local q-mass on the union of the family equals the product, over the members U of 𝒞, of the local q-mass on U.

Formal statement
hypotheses
N :
Type u_1
N → Type u_2
shared
∀ n, Fintype (Ω n)
∀ n, MeasurableSingletonClass (Ω n)
M :
SCM N Ω
s :
M.FixedValues
𝒞 :
Finset (Finset (SWIGNode N))
h𝒞obs :
∀ U ∈ 𝒞, U ⊆ M.observed
hblock :
(↑𝒞 : Set (Finset (SWIGNode N))).Pairwise (fun U U' => Disjoint (M.latentBlock U) (M.latentBlock U'))
x :
ValuesOn M.observed (swigΩ Ω)
conclusion
M.qLocalMass s (𝒞.sup id) (fun v hv => by rw [Finset.mem_sup] at hv rcases hv with ⟨U, hU, hvU⟩ exact h𝒞obs U hU hvU) x
= ∏ U ∈ 𝒞, if hU : U ∈ 𝒞 then M.qLocalMass s U (h𝒞obs U hU) x else 1
Proof (Lean source)
lemma qLocalMass_prod_of_latentBlock_disjoint [∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)] (M : SCM N Ω) (s : M.FixedValues) (𝒞 : Finset (Finset (SWIGNode N))) (h𝒞obs : ∀ U ∈ 𝒞, U ⊆ M.observed) (hblock : (↑𝒞 : Set (Finset (SWIGNode N))).Pairwise (fun U U' => Disjoint (M.latentBlock U) (M.latentBlock U'))) (x : ValuesOn M.observed (swigΩ Ω)) : M.qLocalMass s (𝒞.sup id) (fun v hv => by rw [Finset.mem_sup] at hv rcases hv with ⟨U, hU, hvU⟩ exact h𝒞obs U hU hvU) x = ∏ U ∈ 𝒞, if hU : U ∈ 𝒞 then M.qLocalMass s U (h𝒞obs U hU) x else 1 := by classical let hSup : 𝒞.sup id ⊆ M.observed := fun v hv => by rw [Finset.mem_sup] at hv rcases hv with ⟨U, hU, hvU⟩ exact h𝒞obs U hU hvU let E : Finset (SWIGNode N) → Set M.LatentValues := fun U => if hU : U ∈ 𝒞 then {ℓ : M.LatentValues | ∀ v (hv : v ∈ U), M.localConsistent s x v (h𝒞obs U hU hv) ℓ} else Set.univ have hevent : {ℓ : M.LatentValues | ∀ v (hv : v ∈ 𝒞.sup id), M.localConsistent s x v (hSup hv) ℓ} = ⋂ U ∈ 𝒞, E U := by simpa [E, hSup] using localConsistent_event_eq_family_biInter M s 𝒞 h𝒞obs hSup x have hcoord : iIndepFun (fun u : {u // u ∈ M.unobserved} => fun ℓ : M.LatentValues => ℓ u) M.latentProduct := by haveI : ∀ u : {u // u ∈ M.unobserved}, IsProbabilityMeasure (M.latentDist u) := M.isProbability_latent unfold SCM.latentProduct exact ProbabilityTheory.iIndepFun_pi (X := fun _ : {u // u ∈ M.unobserved} => id) (fun _ => aemeasurable_id) have hfactor : ∀ S : Finset (Finset (SWIGNode N)), S ⊆ 𝒞 → M.latentProduct (⋂ U ∈ S, E U) = ∏ U ∈ S, M.latentProduct (E U) := by intro S refine Finset.induction_on S ?base ?step · intro _hS simp [E] · intro U S hUnot ih hSinsert have hS : S ⊆ 𝒞 := by intro V hV exact hSinsert (Finset.mem_insert_of_mem hV) have hU : U ∈ 𝒞 := hSinsert (Finset.mem_insert_self U S) have hdisj : Disjoint (S.biUnion (latentBlockIndex M)) (latentBlockIndex M U) := latentBlockIndex_biUnion_disjoint_of_pairwise M hS hU hUnot hblock have hindep : IndepFun (fun ℓ : M.LatentValues => fun u : S.biUnion (latentBlockIndex M) => ℓ u) (fun ℓ : M.LatentValues => fun u : latentBlockIndex M U => ℓ u) M.latentProduct := hcoord.indepFun_finset (S.biUnion (latentBlockIndex M)) (latentBlockIndex M U) hdisj (fun u => measurable_pi_apply u) have hmeasS : MeasurableSet[ comap (fun ℓ : M.LatentValues => fun u : S.biUnion (latentBlockIndex M) => ℓ u) inferInstance] (⋂ V ∈ S, E V) := by have hbase := localConsistent_biInter_event_measurable_comap_latentBlockIndex_of_family M s 𝒞 S hS h𝒞obs x convert hbase using 1 ext ℓ simp only [Set.mem_iInter, Set.mem_setOf_eq] constructor · intro h V hVS have hEV := h V hVS simpa [E, hS hVS] using hEV · intro h V hVS have hEV := h V hVS simpa [E, hS hVS] using hEV have hmeasU : MeasurableSet[ comap (fun ℓ : M.LatentValues => fun u : latentBlockIndex M U => ℓ u) inferInstance] (E U) := by simpa [E, hU] using localConsistent_event_measurable_comap_latentBlockIndex_of_family M s U (h𝒞obs U hU) x have hinter := hindep.meas_inter (μ := M.latentProduct) hmeasS hmeasU calc M.latentProduct (⋂ V ∈ insert U S, E V) = M.latentProduct ((⋂ V ∈ S, E V) ∩ E U) := by congr 1 ext ℓ simp [E, and_comm] _ = M.latentProduct (⋂ V ∈ S, E V) * M.latentProduct (E U) := by exact hinter _ = (∏ V ∈ S, M.latentProduct (E V)) * M.latentProduct (E U) := by rw [ih hS] _ = ∏ V ∈ insert U S, M.latentProduct (E V) := by rw [Finset.prod_insert hUnot] rw [mul_comm] have hfull := hfactor 𝒞 (fun _ h => h) simp only [causal_defs_simps] rw [hevent] rw [hfull] refine Finset.prod_congr rfl ?_ intro U hU simp [E, hU]
Causalean.SCM.qLocalMass_prod_of_latentBlock_disjoint · Causalean/SCM/ID/Density/QMass/Factorization.lean:207 · uses SWIGNode , instDecidableEqSWIGNode , swigΩ , ValuesOn , SCM , FixedValues , latentBlock , qLocalMass
theorem obsKernel_marginal_singleton_eq_prod_qLocalMass reviewed
Causalean.SCM

For a set of observed nodes P that is closed under observed parents, the singleton mass of the projection of the observational law onto P equals the product, over the full c-components C of the graph, of the local q-mass on C ∩ P.

Formal statement
hypotheses
N :
Type u_1
N → Type u_2
shared
∀ n, Fintype (Ω n)
∀ n, MeasurableSingletonClass (Ω n)
M :
SCM N Ω
s :
M.FixedValues
P :
Finset (SWIGNode N)
hP :
M.ObsParentClosed P
x :
ValuesOn M.observed (swigΩ Ω)
conclusion
((M.obsKernel s).map (valuesProjection hP.1)) {valuesProjection hP.1 x}
= ∏ C ∈ M.toSWIGGraph.cComponentSet, M.qLocalMass s (C ∩ P) (fun _ hv => hP.1 (mem_of_mem_inter_right hv)) x
Proof (Lean source)
theorem obsKernel_marginal_singleton_eq_prod_qLocalMass [∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)] (M : SCM N Ω) (s : M.FixedValues) (P : Finset (SWIGNode N)) (hP : M.ObsParentClosed P) (x : ValuesOn M.observed (swigΩ Ω)) : ((M.obsKernel s).map (valuesProjection hP.1)) {valuesProjection hP.1 x} = ∏ C ∈ M.toSWIGGraph.cComponentSet, M.qLocalMass s (C ∩ P) (fun _ hv => hP.1 (mem_of_mem_inter_right hv)) x := by classical rw [obsKernel_marginal_singleton_eq_latentProduct_agree M s hP.1 x] have hset : {ℓ | ∀ v : {v // v ∈ P}, M.evalMap s ℓ ⟨v.val, mem_union_left M.unobserved (hP.1 v.property)⟩ = x ⟨v.val, hP.1 v.property⟩} = {ℓ | ∀ v (hv : v ∈ P), M.localConsistent s x v (hP.1 hv) ℓ} := by ext ℓ constructor · intro hEval exact (M.evalMap_agree_iff_localConsistent s P hP x ℓ).mp (fun v hv => hEval ⟨v, hv⟩) · intro hLocal v exact (M.evalMap_agree_iff_localConsistent s P hP x ℓ).mpr hLocal v.val v.property rw [hset] exact latentProduct_localConsistent_factorization M s P hP x
Causalean.SCM.obsKernel_marginal_singleton_eq_prod_qLocalMass · Causalean/SCM/ID/Density/QMass/Factorization.lean:569 · uses cComponentSet , SWIGNode , instFintype , instDecidableEqSWIGNode , instMeasurableSpaceSwigΩ , swigΩ , ValuesOn , valuesProjection , SCM , FixedValues , ObsParentClosed , ObservedValues , obsKernel , qLocalMass
4 supporting declarations (lemmas, instances)
  • localConsistent_event_eq_component_biInter lemma — For an observed-parent-closed node set, local consistency at all of its nodes is equivalent to local consistency within each of its confounded components.
    hypotheses
    N :
    Type u_1
    N → Type u_2
    shared
    M :
    SCM N Ω
    s :
    M.FixedValues
    P :
    Finset (SWIGNode N)
    hP :
    M.ObsParentClosed P
    x :
    ValuesOn M.observed (swigΩ Ω)
    conclusion
    {ℓ : M.LatentValues | ∀ v (hv : v ∈ P), M.localConsistent s x v (hP.1 hv) ℓ}
    = ⋂ C ∈ M.toSWIGGraph.cComponentSet, {ℓ : M.LatentValues | ∀ v (hv : v ∈ C ∩ P), M.localConsistent s x v (hP.1 (mem_of_mem_inter_right hv)) ℓ}
    Proof (Lean source)
    lemma localConsistent_event_eq_component_biInter (M : SCM N Ω) (s : M.FixedValues) (P : Finset (SWIGNode N)) (hP : M.ObsParentClosed P) (x : ValuesOn M.observed (swigΩ Ω)) : {ℓ : M.LatentValues | ∀ v (hv : v ∈ P), M.localConsistent s x v (hP.1 hv) ℓ} = ⋂ C ∈ M.toSWIGGraph.cComponentSet, {ℓ : M.LatentValues | ∀ v (hv : v ∈ C ∩ P), M.localConsistent s x v (hP.1 (mem_of_mem_inter_right hv)) ℓ} := by classical ext ℓ constructor · intro hℓ rw [Set.mem_iInter] intro C rw [Set.mem_iInter] intro _hC v hv exact hℓ v (mem_of_mem_inter_right hv) · intro hℓ v hvP rw [Set.mem_iInter] at hℓ have hC : M.toSWIGGraph.cComponentOf v ∈ M.toSWIGGraph.cComponentSet := by rw [SWIGGraph.cComponentSet, mem_image] exact ⟨v, hP.1 hvP, rfl⟩ have hvC : v ∈ M.toSWIGGraph.cComponentOf v := M.toSWIGGraph.mem_cComponentOf_self (hP.1 hvP) have hℓC := hℓ (M.toSWIGGraph.cComponentOf v) rw [Set.mem_iInter] at hℓC exact hℓC hC v (Finset.mem_inter.mpr ⟨hvC, hvP⟩)
    Causalean.SCM.localConsistent_event_eq_component_biInter · Causalean/SCM/ID/Density/QMass/Factorization.lean:41
  • localConsistent_event_eq_family_biInter lemma — For a finite family of observed node sets, local consistency over their union is equivalent to local consistency over every member of the family.
    hypotheses
    N :
    Type u_1
    N → Type u_2
    shared
    M :
    SCM N Ω
    s :
    M.FixedValues
    𝒞 :
    Finset (Finset (SWIGNode N))
    h𝒞obs :
    ∀ U ∈ 𝒞, U ⊆ M.observed
    hSup :
    𝒞.sup id ⊆ M.observed
    x :
    ValuesOn M.observed (swigΩ Ω)
    conclusion
    {ℓ : M.LatentValues | ∀ v (hv : v ∈ 𝒞.sup id), M.localConsistent s x v (hSup hv) ℓ}
    = ⋂ U ∈ 𝒞, if hU : U ∈ 𝒞 then {ℓ : M.LatentValues | ∀ v (hv : v ∈ U), M.localConsistent s x v (h𝒞obs U hU hv) ℓ} else univ
    Proof (Lean source)
    lemma localConsistent_event_eq_family_biInter (M : SCM N Ω) (s : M.FixedValues) (𝒞 : Finset (Finset (SWIGNode N))) (h𝒞obs : ∀ U ∈ 𝒞, U ⊆ M.observed) (hSup : 𝒞.sup id ⊆ M.observed) (x : ValuesOn M.observed (swigΩ Ω)) : {ℓ : M.LatentValues | ∀ v (hv : v ∈ 𝒞.sup id), M.localConsistent s x v (hSup hv) ℓ} = ⋂ U ∈ 𝒞, if hU : U ∈ 𝒞 then {ℓ : M.LatentValues | ∀ v (hv : v ∈ U), M.localConsistent s x v (h𝒞obs U hU hv) ℓ} else univ := by classical ext ℓ constructor · intro hℓ rw [Set.mem_iInter] intro U rw [Set.mem_iInter] intro hU simp [hU] intro v hv have hvSup : v ∈ 𝒞.sup id := by rw [Finset.mem_sup] exact ⟨U, hU, hv⟩ convert hℓ v hvSup using 1 · intro hℓ v hvSup rw [Set.mem_iInter] at hℓ rw [Finset.mem_sup] at hvSup rcases hvSup with ⟨U, hU, hvU⟩ have hℓU := hℓ U rw [Set.mem_iInter] at hℓU have hUevent : ℓ ∈ {ℓ : M.LatentValues | ∀ v (hv : v ∈ U), M.localConsistent s x v (h𝒞obs U hU hv) ℓ} := by simpa [hU] using hℓU hU convert hUevent v hvU using 1
    Causalean.SCM.localConsistent_event_eq_family_biInter · Causalean/SCM/ID/Density/QMass/Factorization.lean:74
  • qLocalMass_prod_inter_of_latentBlock_disjoint lemma — Local q-mass on a covered set factors over an abstract family after intersecting each family member with the covered set.
    hypotheses
    N :
    Type u_1
    N → Type u_2
    shared
    ∀ n, Fintype (Ω n)
    ∀ n, MeasurableSingletonClass (Ω n)
    M :
    SCM N Ω
    s :
    M.FixedValues
    P :
    Finset (SWIGNode N)
    hPobs :
    P ⊆ M.observed
    𝒞 :
    Finset (Finset (SWIGNode N))
    h𝒞obs :
    ∀ U ∈ 𝒞, U ⊆ M.observed
    hcover :
    P ⊆ 𝒞.sup id
    hblock :
    (↑𝒞 : Set (Finset (SWIGNode N))).Pairwise (fun U U' => Disjoint (M.latentBlock U) (M.latentBlock U'))
    x :
    ValuesOn M.observed (swigΩ Ω)
    conclusion
    M.qLocalMass s P hPobs x
    = ∏ U ∈ 𝒞, if hU : U ∈ 𝒞 then M.qLocalMass s (U ∩ P) (fun _ hv => h𝒞obs U hU (mem_of_mem_inter_left hv)) x else 1
    Proof (Lean source)
    lemma qLocalMass_prod_inter_of_latentBlock_disjoint [∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)] (M : SCM N Ω) (s : M.FixedValues) (P : Finset (SWIGNode N)) (hPobs : P ⊆ M.observed) (𝒞 : Finset (Finset (SWIGNode N))) (h𝒞obs : ∀ U ∈ 𝒞, U ⊆ M.observed) (hcover : P ⊆ 𝒞.sup id) (hblock : (↑𝒞 : Set (Finset (SWIGNode N))).Pairwise (fun U U' => Disjoint (M.latentBlock U) (M.latentBlock U'))) (x : ValuesOn M.observed (swigΩ Ω)) : M.qLocalMass s P hPobs x = ∏ U ∈ 𝒞, if hU : U ∈ 𝒞 then M.qLocalMass s (U ∩ P) (fun _ hv => h𝒞obs U hU (mem_of_mem_inter_left hv)) x else 1 := by classical let E : Finset (SWIGNode N) → Set M.LatentValues := fun U => if hU : U ∈ 𝒞 then {ℓ : M.LatentValues | ∀ v (hv : v ∈ U ∩ P), M.localConsistent s x v (h𝒞obs U hU (mem_of_mem_inter_left hv)) ℓ} else Set.univ have hevent : {ℓ : M.LatentValues | ∀ v (hv : v ∈ P), M.localConsistent s x v (hPobs hv) ℓ} = ⋂ U ∈ 𝒞, E U := by ext ℓ constructor · intro hℓ rw [Set.mem_iInter] intro U rw [Set.mem_iInter] intro hU simp [E, hU] intro v _hvU hvP exact hℓ v hvP · intro hℓ v hvP rw [Set.mem_iInter] at hℓ have hvSup : v ∈ 𝒞.sup id := hcover hvP rw [Finset.mem_sup] at hvSup rcases hvSup with ⟨U, hU, hvU⟩ have hℓU := hℓ U rw [Set.mem_iInter] at hℓU have hUevent : ℓ ∈ {ℓ : M.LatentValues | ∀ v (hv : v ∈ U ∩ P), M.localConsistent s x v (h𝒞obs U hU (mem_of_mem_inter_left hv)) ℓ} := by simpa [E, hU] using hℓU hU have hvUP : v ∈ U ∩ P := Finset.mem_inter.mpr ⟨hvU, hvP⟩ convert hUevent v hvUP using 1 have hcoord : iIndepFun (fun u : {u // u ∈ M.unobserved} => fun ℓ : M.LatentValues => ℓ u) M.latentProduct := by haveI : ∀ u : {u // u ∈ M.unobserved}, IsProbabilityMeasure (M.latentDist u) := M.isProbability_latent unfold SCM.latentProduct exact ProbabilityTheory.iIndepFun_pi (X := fun _ : {u // u ∈ M.unobserved} => id) (fun _ => aemeasurable_id) have hfactor : ∀ S : Finset (Finset (SWIGNode N)), S ⊆ 𝒞 → M.latentProduct (⋂ U ∈ S, E U) = ∏ U ∈ S, M.latentProduct (E U) := by intro S refine Finset.induction_on S ?base ?step · intro _hS simp [E] · intro U S hUnot ih hSinsert have hS : S ⊆ 𝒞 := by intro V hV exact hSinsert (Finset.mem_insert_of_mem hV) have hU : U ∈ 𝒞 := hSinsert (Finset.mem_insert_self U S) have hdisj : Disjoint (S.biUnion (latentBlockIndex M)) (latentBlockIndex M U) := latentBlockIndex_biUnion_disjoint_of_pairwise M hS hU hUnot hblock have hindep : IndepFun (fun ℓ : M.LatentValues => fun u : S.biUnion (latentBlockIndex M) => ℓ u) (fun ℓ : M.LatentValues => fun u : latentBlockIndex M U => ℓ u) M.latentProduct := hcoord.indepFun_finset (S.biUnion (latentBlockIndex M)) (latentBlockIndex M U) hdisj (fun u => measurable_pi_apply u) have hmeasS : MeasurableSet[ comap (fun ℓ : M.LatentValues => fun u : S.biUnion (latentBlockIndex M) => ℓ u) inferInstance] (⋂ V ∈ S, E V) := by refine measurableSet_comap_piFinset_of_depends (S := S.biUnion (latentBlockIndex M)) _ ?_ intro ℓ ℓ' hagree constructor · intro hℓ rw [Set.mem_iInter] at hℓ rw [Set.mem_iInter] intro V have hℓV := hℓ V rw [Set.mem_iInter] at hℓV rw [Set.mem_iInter] intro hVS have hV𝒞 : V ∈ 𝒞 := hS hVS simp [E, hV𝒞] intro v hvV hvP have hlocal : M.localConsistent s x v (h𝒞obs V hV𝒞 hvV) ℓ := by have hEV : ℓ ∈ E V := hℓV hVS have hEV' : ∀ v (hv : v ∈ V ∩ P), M.localConsistent s x v (h𝒞obs V hV𝒞 (mem_of_mem_inter_left hv)) ℓ := by simpa [E, hV𝒞] using hEV exact hEV' v (Finset.mem_inter.mpr ⟨hvV, hvP⟩) exact (localConsistent_depends_only_on_latentBlock_of_mem M s x hvV (h𝒞obs V hV𝒞 hvV) ℓ ℓ' (by intro u hu have hmemBlock : (⟨u, (Finset.mem_filter.mp hu).1⟩ : {u // u ∈ M.unobserved}) ∈ latentBlockIndex M V := (mem_latentBlockIndex_iff M V _).mpr hu have hmem : (⟨u, (Finset.mem_filter.mp hu).1⟩ : {u // u ∈ M.unobserved}) ∈ S.biUnion (latentBlockIndex M) := by rw [Finset.mem_biUnion] exact ⟨V, hVS, hmemBlock⟩ have hcoord := hagree ⟨u, (Finset.mem_filter.mp hu).1⟩ hmem simpa using hcoord)).mp hlocal · intro hℓ' rw [Set.mem_iInter] at hℓ' rw [Set.mem_iInter] intro V have hℓ'V := hℓ' V rw [Set.mem_iInter] at hℓ'V rw [Set.mem_iInter] intro hVS have hV𝒞 : V ∈ 𝒞 := hS hVS simp [E, hV𝒞] intro v hvV hvP have hlocal : M.localConsistent s x v (h𝒞obs V hV𝒞 hvV) ℓ' := by have hEV : ℓ' ∈ E V := hℓ'V hVS have hEV' : ∀ v (hv : v ∈ V ∩ P), M.localConsistent s x v (h𝒞obs V hV𝒞 (mem_of_mem_inter_left hv)) ℓ' := by simpa [E, hV𝒞] using hEV exact hEV' v (Finset.mem_inter.mpr ⟨hvV, hvP⟩) exact (localConsistent_depends_only_on_latentBlock_of_mem M s x hvV (h𝒞obs V hV𝒞 hvV) ℓ' ℓ (by intro u hu have hmemBlock : (⟨u, (Finset.mem_filter.mp hu).1⟩ : {u // u ∈ M.unobserved}) ∈ latentBlockIndex M V := (mem_latentBlockIndex_iff M V _).mpr hu have hmem : (⟨u, (Finset.mem_filter.mp hu).1⟩ : {u // u ∈ M.unobserved}) ∈ S.biUnion (latentBlockIndex M) := by rw [Finset.mem_biUnion] exact ⟨V, hVS, hmemBlock⟩ have hcoord := hagree ⟨u, (Finset.mem_filter.mp hu).1⟩ hmem simpa using hcoord.symm)).mp hlocal have hmeasU : MeasurableSet[ comap (fun ℓ : M.LatentValues => fun u : latentBlockIndex M U => ℓ u) inferInstance] (E U) := by refine measurableSet_comap_piFinset_of_depends (S := latentBlockIndex M U) _ ?_ intro ℓ ℓ' hagree constructor · intro hℓ simp [E, hU] at hℓ ⊢ intro v hvU hvP have hlocal : M.localConsistent s x v (h𝒞obs U hU hvU) ℓ := hℓ v hvU hvP exact (localConsistent_depends_only_on_latentBlock_of_mem M s x hvU (h𝒞obs U hU hvU) ℓ ℓ' (by intro u hu have hmem : (⟨u, (Finset.mem_filter.mp hu).1⟩ : {u // u ∈ M.unobserved}) ∈ latentBlockIndex M U := (mem_latentBlockIndex_iff M U _).mpr hu have hcoord := hagree ⟨u, (Finset.mem_filter.mp hu).1⟩ hmem simpa using hcoord)).mp hlocal · intro hℓ' simp [E, hU] at hℓ' ⊢ intro v hvU hvP have hlocal : M.localConsistent s x v (h𝒞obs U hU hvU) ℓ' := hℓ' v hvU hvP exact (localConsistent_depends_only_on_latentBlock_of_mem M s x hvU (h𝒞obs U hU hvU) ℓ' ℓ (by intro u hu have hmem : (⟨u, (Finset.mem_filter.mp hu).1⟩ : {u // u ∈ M.unobserved}) ∈ latentBlockIndex M U := (mem_latentBlockIndex_iff M U _).mpr hu have hcoord := hagree ⟨u, (Finset.mem_filter.mp hu).1⟩ hmem simpa using hcoord.symm)).mp hlocal have hinter := hindep.meas_inter (μ := M.latentProduct) hmeasS hmeasU calc M.latentProduct (⋂ V ∈ insert U S, E V) = M.latentProduct ((⋂ V ∈ S, E V) ∩ E U) := by congr 1 ext ℓ simp [E, and_comm] _ = M.latentProduct (⋂ V ∈ S, E V) * M.latentProduct (E U) := by exact hinter _ = (∏ V ∈ S, M.latentProduct (E V)) * M.latentProduct (E U) := by rw [ih hS] _ = ∏ V ∈ insert U S, M.latentProduct (E V) := by rw [Finset.prod_insert hUnot] rw [mul_comm] have hfull := hfactor 𝒞 (fun _ h => h) simp only [causal_defs_simps] rw [hevent] rw [hfull] refine Finset.prod_congr rfl ?_ intro U hU simp [E, hU]
    Causalean.SCM.qLocalMass_prod_inter_of_latentBlock_disjoint · Causalean/SCM/ID/Density/QMass/Factorization.lean:334
  • qLocalMass_pos_of_positiveObs lemma — Positive observational mass implies nonzero local q-mass.
    hypotheses
    N :
    Type u_1
    N → Type u_2
    shared
    M :
    SCM N Ω
    s :
    M.FixedValues
    MeasurableSingletonClass (ValuesOn M.observed (swigΩ Ω))
    hpos :
    ID.DiscreteID.PositiveMass (M.obsKernel s)
    T hT x :
    conclusion
    M.qLocalMass s T hT x ≠ 0
    Proof (Lean source)
    lemma qLocalMass_pos_of_positiveObs (M : SCM N Ω) (s : M.FixedValues) [MeasurableSingletonClass (ValuesOn M.observed (swigΩ Ω))] (hpos : ID.DiscreteID.PositiveMass (M.obsKernel s)) : ∀ T hT x, M.qLocalMass s T hT x ≠ 0 := by classical intro T hT x have hobs : M.observed ⊆ M.observed := fun ⦃_⦄ hv => hv have hclosed : M.ObsParentClosed M.observed := by refine ⟨hobs, ?_⟩ intro _v _hv _w hw _hedge exact hw have hmass := obsKernel_marginal_singleton_eq_latentProduct_agree M s (P := M.observed) hobs x have hset : {ℓ : M.LatentValues | ∀ v : {v // v ∈ M.observed}, M.evalMap s ℓ ⟨v.val, mem_union_left M.unobserved v.property⟩ = x ⟨v.val, v.property⟩} = {ℓ : M.LatentValues | ∀ v (hv : v ∈ M.observed), M.localConsistent s x v hv ℓ} := by ext ℓ constructor · intro hEval exact (M.evalMap_agree_iff_localConsistent s M.observed hclosed x ℓ).mp (fun v hv => hEval ⟨v, hv⟩) · intro hLocal v exact (M.evalMap_agree_iff_localConsistent s M.observed hclosed x ℓ).mpr hLocal v.val v.property rw [hset] at hmass have hproj_id : (valuesProjection (Ω := swigΩ Ω) hobs : ValuesOn M.observed (swigΩ Ω) → ValuesOn M.observed (swigΩ Ω)) = id := by funext ξ rfl rw [hproj_id, Measure.map_id] at hmass have hfull : M.qLocalMass s M.observed hobs x ≠ 0 := by have hx : (M.obsKernel s) ({x} : Set (ValuesOn M.observed (swigΩ Ω))) ≠ 0 := by simpa [ID.DiscreteID.singletonMass_apply] using hpos x simpa [qLocalMass] using (hmass ▸ hx) have hle : M.qLocalMass s M.observed hobs x ≤ M.qLocalMass s T hT x := M.qLocalMass_anti s (T := T) (T' := M.observed) hT hT hobs x intro hzero exact hfull (le_antisymm (by simpa [hzero] using hle) zero_le)
    Causalean.SCM.qLocalMass_pos_of_positiveObs · Causalean/SCM/ID/Density/QMass/Factorization.lean:601
Latent­Blocks 2 core · 9 supporting This file identifies the latent coordinates on which local-consistency events depend and proves the corresponding product-measurability statements. ★ localConsistent_biInter_event_measurable_comap_latentBlockIndex_of_family

Measurability of latent-block consistency events

This file identifies the latent coordinates on which local-consistency events depend and proves the corresponding product-measurability statements. The results prepare those events for independence and factorization across c-components.

def latentBlockIndex reviewed
Causalean.SCM

For a structural causal model and a set of graph nodes, the latent-block index is the finite collection of the model's unobserved variables that belong to that set's latent block. It is used to group the independent latent coordinates in density factorization arguments.

Definition (Lean source)
parameters
N :
Type u_1
N → Type u_2
shared
M :
SCM N Ω
C :
Finset (SWIGNode N)
def
latentBlockIndex M C :
Finset {u // u ∈ M.unobserved}
given by
Finset.univ.filter (fun u : {u // u ∈ M.unobserved} => u.val ∈ M.latentBlock C)
Causalean.SCM.latentBlockIndex · Causalean/SCM/ID/Density/QMass/LatentBlocks.lean:88 · uses SWIGNode , SCM
lemma localConsistent_biInter_event_measurable_comap_latentBlockIndex_of_family reviewed
Causalean.SCM

For a finite structural causal model with finite measurable node-value spaces, a fixed-node assignment, a finite family of observed node blocks and a selected subfamily, containment of the subfamily, observability of every block in the family, and an observed realization, the event that all local consistency equations hold throughout the selected blocks is measurable using only the latent coordinates in those blocks.

Formal statement
hypotheses
N :
Type u_1
N → Type u_2
shared
∀ n, Fintype (Ω n)
∀ n, MeasurableSingletonClass (Ω n)
M :
SCM N Ω
s :
M.FixedValues
𝒞 S :
Finset (Finset (SWIGNode N))
hS :
S ⊆ 𝒞
h𝒞obs :
∀ U ∈ 𝒞, U ⊆ M.observed
x :
ValuesOn M.observed (swigΩ Ω)
conclusion
MeasurableSet[ comap (fun ℓ : M.LatentValues => fun u : S.biUnion (latentBlockIndex M) => ℓ u) inferInstance] (⋂ U ∈ S, {ℓ : M.LatentValues | ∀ v (hv : v ∈ U), M.localConsistent s x v (h𝒞obs U (hS ‹U ∈ S›) hv) ℓ})
Proof (Lean source)
lemma localConsistent_biInter_event_measurable_comap_latentBlockIndex_of_family [∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)] (M : SCM N Ω) (s : M.FixedValues) (𝒞 S : Finset (Finset (SWIGNode N))) (hS : S ⊆ 𝒞) (h𝒞obs : ∀ U ∈ 𝒞, U ⊆ M.observed) (x : ValuesOn M.observed (swigΩ Ω)) : MeasurableSet[ comap (fun ℓ : M.LatentValues => fun u : S.biUnion (latentBlockIndex M) => ℓ u) inferInstance] (⋂ U ∈ S, {ℓ : M.LatentValues | ∀ v (hv : v ∈ U), M.localConsistent s x v (h𝒞obs U (hS ‹U ∈ S›) hv) ℓ}) := by classical refine measurableSet_comap_piFinset_of_depends (S := S.biUnion (latentBlockIndex M)) _ ?_ intro ℓ ℓ' hagree constructor · intro hℓ rw [Set.mem_iInter] at hℓ rw [Set.mem_iInter] intro U have hℓU := hℓ U rw [Set.mem_iInter] at hℓU rw [Set.mem_iInter] intro hUS v hv have hlocal : M.localConsistent s x v (h𝒞obs U (hS hUS) hv) ℓ := by simpa [hS hUS] using hℓU hUS v hv exact (localConsistent_depends_only_on_latentBlock_of_mem M s x hv (h𝒞obs U (hS hUS) hv) ℓ ℓ' (by intro u hu have hmemBlock : (⟨u, (Finset.mem_filter.mp hu).1⟩ : {u // u ∈ M.unobserved}) ∈ latentBlockIndex M U := (mem_latentBlockIndex_iff M U _).mpr hu have hmem : (⟨u, (Finset.mem_filter.mp hu).1⟩ : {u // u ∈ M.unobserved}) ∈ S.biUnion (latentBlockIndex M) := by rw [Finset.mem_biUnion] exact ⟨U, hUS, hmemBlock⟩ have hcoord := hagree ⟨u, (Finset.mem_filter.mp hu).1⟩ hmem simpa using hcoord)).mp hlocal · intro hℓ' rw [Set.mem_iInter] at hℓ' rw [Set.mem_iInter] intro U have hℓ'U := hℓ' U rw [Set.mem_iInter] at hℓ'U rw [Set.mem_iInter] intro hUS v hv have hlocal : M.localConsistent s x v (h𝒞obs U (hS hUS) hv) ℓ' := by simpa [hS hUS] using hℓ'U hUS v hv exact (localConsistent_depends_only_on_latentBlock_of_mem M s x hv (h𝒞obs U (hS hUS) hv) ℓ' ℓ (by intro u hu have hmemBlock : (⟨u, (Finset.mem_filter.mp hu).1⟩ : {u // u ∈ M.unobserved}) ∈ latentBlockIndex M U := (mem_latentBlockIndex_iff M U _).mpr hu have hmem : (⟨u, (Finset.mem_filter.mp hu).1⟩ : {u // u ∈ M.unobserved}) ∈ S.biUnion (latentBlockIndex M) := by rw [Finset.mem_biUnion] exact ⟨U, hUS, hmemBlock⟩ have hcoord := hagree ⟨u, (Finset.mem_filter.mp hu).1⟩ hmem simpa using hcoord.symm)).mp hlocal
Causalean.SCM.localConsistent_biInter_event_measurable_comap_latentBlockIndex_of_family · Causalean/SCM/ID/Density/QMass/LatentBlocks.lean:407 · uses SWIGNode , instDecidableEqSWIGNode , instMeasurableSpaceSwigΩ , swigΩ , ValuesOn , SCM , FixedValues , LatentValues , latentBlockIndex , localConsistent
9 supporting declarations (lemmas, instances)
  • latentProduct_singleton_eq_prod lemma — The latent-product mass of a singleton latent assignment equals the product of the singleton masses assigned by the latent distributions at every unobserved node.
    hypotheses
    N :
    Type u_1
    N → Type u_2
    shared
    ∀ n, Fintype (Ω n)
    ∀ n, MeasurableSingletonClass (Ω n)
    M :
    SCM N Ω
    ℓ₀ :
    M.LatentValues
    conclusion
    M.latentProduct ({ℓ₀} : Set M.LatentValues)
    = ∏ u : {u // u ∈ M.unobserved}, M.latentDist u ({ℓ₀ u} : Set (swigΩ Ω u.val))
    Proof (Lean source)
    lemma latentProduct_singleton_eq_prod [∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)] (M : SCM N Ω) (ℓ₀ : M.LatentValues) : M.latentProduct ({ℓ₀} : Set M.LatentValues) = ∏ u : {u // u ∈ M.unobserved}, M.latentDist u ({ℓ₀ u} : Set (swigΩ Ω u.val)) := by classical haveI : ∀ u : {u // u ∈ M.unobserved}, IsProbabilityMeasure (M.latentDist u) := M.isProbability_latent haveI : ∀ u : {u // u ∈ M.unobserved}, SigmaFinite (M.latentDist u) := fun _ => inferInstance unfold SCM.latentProduct have hsingleton : ({ℓ₀} : Set M.LatentValues) = Set.univ.pi (fun u => ({ℓ₀ u} : Set (swigΩ Ω u.val))) := by ext ℓ simp [Set.mem_pi, funext_iff] rw [hsingleton, MeasureTheory.Measure.pi_pi]
    Causalean.SCM.latentProduct_singleton_eq_prod · Causalean/SCM/ID/Density/QMass/LatentBlocks.lean:42
  • measurableSet_comap_piFinset_of_depends lemma — A set of finite product outcomes whose membership depends only on a specified finite set of coordinates is measurable with respect to the σ-algebra on those coordinates.
    hypotheses
    ι :
    Type*
    Fintype ι
    ι → Type*
    ∀ i, MeasurableSpace (α i)
    ∀ i, Fintype (α i)
    ∀ i, MeasurableSingletonClass (α i)
    S :
    Finset ι
    A :
    Set (∀ i, α i)
    hdep :
    ∀ ξ ξ'
    if
    (∀ i (_hi : i ∈ S), ξ i = ξ' i)
    then
    (ξ ∈ A ↔ ξ' ∈ A)
    conclusion
    MeasurableSet[ comap (fun ξ : (∀ i, α i) => fun i : S => ξ i) inferInstance] A
    Proof (Lean source)
    lemma measurableSet_comap_piFinset_of_depends {ι : Type*} [Fintype ι] {α : ι → Type*} [∀ i, MeasurableSpace (α i)] [∀ i, Fintype (α i)] [∀ i, MeasurableSingletonClass (α i)] (S : Finset ι) (A : Set (∀ i, α i)) (hdep : ∀ ξ ξ', (∀ i (_hi : i ∈ S), ξ i = ξ' i) → (ξ ∈ A ↔ ξ' ∈ A)) : MeasurableSet[ comap (fun ξ : (∀ i, α i) => fun i : S => ξ i) inferInstance] A := by let B : Set (∀ i : S, α i.val) := {η | ∃ ξ ∈ A, (fun i : S => ξ i) = η} refine ⟨B, Set.Finite.measurableSet B.toFinite, ?_⟩ ext ξ change ξ ∈ ((fun ξ : (∀ i, α i) => fun i : S => ξ i) ⁻¹' B) ↔ ξ ∈ A constructor · rintro ⟨ξ', hξ'A, hξ'⟩ exact (hdep ξ' ξ (by intro i hi exact congrFun hξ' ⟨i, hi⟩)).mp hξ'A · intro hξA exact ⟨ξ, hξA, rfl⟩
    Causalean.SCM.measurableSet_comap_piFinset_of_depends · Causalean/SCM/ID/Density/QMass/LatentBlocks.lean:64
  • mem_latentBlockIndex_iff lemma — Given a finite structural causal model, node set, and unobserved node, the unobserved-node index belongs to the set's latent-block index exactly when the underlying node belongs to its latent block.
    hypotheses
    N :
    Type u_1
    N → Type u_2
    shared
    M :
    SCM N Ω
    C :
    Finset (SWIGNode N)
    u :
    {u // u ∈ M.unobserved}
    conclusion
    u ∈ latentBlockIndex M C ↔ u.val ∈ M.latentBlock C
    Proof (Lean source)
    lemma mem_latentBlockIndex_iff (M : SCM N Ω) (C : Finset (SWIGNode N)) (u : {u // u ∈ M.unobserved}) : u ∈ latentBlockIndex M C ↔ u.val ∈ M.latentBlock C := by simp [latentBlockIndex]
    Causalean.SCM.mem_latentBlockIndex_iff · Causalean/SCM/ID/Density/QMass/LatentBlocks.lean:97
  • latentBlockIndex_biUnion_disjoint_of_pairwise lemma — Given a finite structural causal model, a family of node sets, a subfamily, and one member, if the subfamily lies in the family, the selected set belongs to the family, it is outside the subfamily, and distinct family members have disjoint latent blocks, then the union of latent-block indices over the subfamily is disjoint from the selected set's index.
    hypotheses
    N :
    Type u_1
    N → Type u_2
    shared
    M :
    SCM N Ω
    𝒞 S :
    Finset (Finset (SWIGNode N))
    C :
    Finset (SWIGNode N)
    hS :
    S ⊆ 𝒞
    hC :
    C ∈ 𝒞
    hCnot :
    C ∉ S
    hblock :
    (↑𝒞 : Set (Finset (SWIGNode N))).Pairwise (fun U U' => Disjoint (M.latentBlock U) (M.latentBlock U'))
    conclusion
    Disjoint (S.biUnion (latentBlockIndex M)) (latentBlockIndex M C)
    Proof (Lean source)
    lemma latentBlockIndex_biUnion_disjoint_of_pairwise (M : SCM N Ω) {𝒞 S : Finset (Finset (SWIGNode N))} {C : Finset (SWIGNode N)} (hS : S ⊆ 𝒞) (hC : C ∈ 𝒞) (hCnot : C ∉ S) (hblock : (↑𝒞 : Set (Finset (SWIGNode N))).Pairwise (fun U U' => Disjoint (M.latentBlock U) (M.latentBlock U'))) : Disjoint (S.biUnion (latentBlockIndex M)) (latentBlockIndex M C) := by classical rw [Finset.disjoint_left] intro u huS huC rw [Finset.mem_biUnion] at huS rcases huS with ⟨D, hDS, huD⟩ have hD : D ∈ 𝒞 := hS hDS have hne : D ≠ C := by intro hDC exact hCnot (hDC ▸ hDS) exact Finset.disjoint_left.mp (latentBlockIndex_pairwise_disjoint_of_latentBlock M (hblock hD hC hne)) huD huC
    Causalean.SCM.latentBlockIndex_biUnion_disjoint_of_pairwise · Causalean/SCM/ID/Density/QMass/LatentBlocks.lean:131
  • latentBlockIndex_biUnion_disjoint lemma — Given a finite structural causal model, a collection of districts, and another district, if the collection consists of districts, the selected set is a district, and it is outside the collection, then the collection's latent-block indices are disjoint from the selected district's latent-block index.
    hypotheses
    N :
    Type u_1
    N → Type u_2
    shared
    M :
    SCM N Ω
    S :
    Finset (Finset (SWIGNode N))
    C :
    Finset (SWIGNode N)
    hS :
    S ⊆ M.toSWIGGraph.cComponentSet
    hC :
    C ∈ M.toSWIGGraph.cComponentSet
    hCnot :
    C ∉ S
    conclusion
    Disjoint (S.biUnion (latentBlockIndex M)) (latentBlockIndex M C)
    Proof (Lean source)
    lemma latentBlockIndex_biUnion_disjoint (M : SCM N Ω) {S : Finset (Finset (SWIGNode N))} {C : Finset (SWIGNode N)} (hS : S ⊆ M.toSWIGGraph.cComponentSet) (hC : C ∈ M.toSWIGGraph.cComponentSet) (hCnot : C ∉ S) : Disjoint (S.biUnion (latentBlockIndex M)) (latentBlockIndex M C) := by classical rw [Finset.disjoint_left] intro u huS huC rw [Finset.mem_biUnion] at huS rcases huS with ⟨D, hDS, huD⟩ have hne : D ≠ C := by intro hDC exact hCnot (hDC ▸ hDS) exact Finset.disjoint_left.mp (latentBlockIndex_pairwise_disjoint M (hS hDS) hC hne) huD huC
    Causalean.SCM.latentBlockIndex_biUnion_disjoint · Causalean/SCM/ID/Density/QMass/LatentBlocks.lean:156
  • localConsistent_event_measurable_comap_latentBlockIndex lemma — Given a finite structural causal model, fixed assignment, observed-parent-closed set, observed assignment, and district, if the set is a district, then the latent assignments locally consistent with the observed values on its intersection with the parent-closed set form a measurable event.
    hypotheses
    N :
    Type u_1
    N → Type u_2
    shared
    ∀ n, Fintype (Ω n)
    ∀ n, MeasurableSingletonClass (Ω n)
    M :
    SCM N Ω
    s :
    M.FixedValues
    P :
    Finset (SWIGNode N)
    hP :
    M.ObsParentClosed P
    x :
    ValuesOn M.observed (swigΩ Ω)
    C :
    Finset (SWIGNode N)
    hC :
    C ∈ M.toSWIGGraph.cComponentSet
    conclusion
    MeasurableSet[ comap (fun ℓ : M.LatentValues => fun u : latentBlockIndex M C => ℓ u) inferInstance] {ℓ : M.LatentValues | ∀ v (hv : v ∈ C ∩ P), M.localConsistent s x v (hP.1 (mem_of_mem_inter_right hv)) ℓ}
    Proof (Lean source)
    lemma localConsistent_event_measurable_comap_latentBlockIndex [∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)] (M : SCM N Ω) (s : M.FixedValues) (P : Finset (SWIGNode N)) (hP : M.ObsParentClosed P) (x : ValuesOn M.observed (swigΩ Ω)) {C : Finset (SWIGNode N)} (hC : C ∈ M.toSWIGGraph.cComponentSet) : MeasurableSet[ comap (fun ℓ : M.LatentValues => fun u : latentBlockIndex M C => ℓ u) inferInstance] {ℓ : M.LatentValues | ∀ v (hv : v ∈ C ∩ P), M.localConsistent s x v (hP.1 (mem_of_mem_inter_right hv)) ℓ} := by classical refine measurableSet_comap_piFinset_of_depends (S := latentBlockIndex M C) _ ?_ intro ℓ ℓ' hagree constructor · intro hℓ v hv have hvC : v ∈ C := Finset.mem_of_mem_inter_left hv have hcomp : M.toSWIGGraph.cComponentOf v = C := M.toSWIGGraph.cComponentOf_eq_of_mem_cComponentSet hC hvC exact (M.localConsistent_depends_only_on_block s x v (hP.1 (mem_of_mem_inter_right hv)) ℓ ℓ' (by intro u hu have huC : u ∈ M.latentBlock C := by simpa [hcomp] using hu have hmem : (⟨u, (Finset.mem_filter.mp huC).1⟩ : {u // u ∈ M.unobserved}) ∈ latentBlockIndex M C := (mem_latentBlockIndex_iff M C _).mpr huC have hcoord := hagree ⟨u, (Finset.mem_filter.mp huC).1⟩ hmem simpa using hcoord)).mp (hℓ v hv) · intro hℓ' v hv have hvC : v ∈ C := Finset.mem_of_mem_inter_left hv have hcomp : M.toSWIGGraph.cComponentOf v = C := M.toSWIGGraph.cComponentOf_eq_of_mem_cComponentSet hC hvC exact (M.localConsistent_depends_only_on_block s x v (hP.1 (mem_of_mem_inter_right hv)) ℓ' ℓ (by intro u hu have huC : u ∈ M.latentBlock C := by simpa [hcomp] using hu have hmem : (⟨u, (Finset.mem_filter.mp huC).1⟩ : {u // u ∈ M.unobserved}) ∈ latentBlockIndex M C := (mem_latentBlockIndex_iff M C _).mpr huC have hcoord := hagree ⟨u, (Finset.mem_filter.mp huC).1⟩ hmem simpa using hcoord.symm)).mp (hℓ' v hv)
    Causalean.SCM.localConsistent_event_measurable_comap_latentBlockIndex · Causalean/SCM/ID/Density/QMass/LatentBlocks.lean:176
  • localConsistent_biInter_event_measurable_comap_latentBlockIndex lemma — Given a finite structural causal model, fixed assignment, observed-parent-closed set, observed assignment, and collection of districts, if every selected set is a district, then the event of simultaneous local consistency over their intersections with the parent-closed set is measurable.
    hypotheses
    N :
    Type u_1
    N → Type u_2
    shared
    ∀ n, Fintype (Ω n)
    ∀ n, MeasurableSingletonClass (Ω n)
    M :
    SCM N Ω
    s :
    M.FixedValues
    P :
    Finset (SWIGNode N)
    hP :
    M.ObsParentClosed P
    x :
    ValuesOn M.observed (swigΩ Ω)
    S :
    Finset (Finset (SWIGNode N))
    hS :
    S ⊆ M.toSWIGGraph.cComponentSet
    conclusion
    MeasurableSet[ comap (fun ℓ : M.LatentValues => fun u : S.biUnion (latentBlockIndex M) => ℓ u) inferInstance] (⋂ C ∈ S, {ℓ : M.LatentValues | ∀ v (hv : v ∈ C ∩ P), M.localConsistent s x v (hP.1 (mem_of_mem_inter_right hv)) ℓ})
    Proof (Lean source)
    lemma localConsistent_biInter_event_measurable_comap_latentBlockIndex [∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)] (M : SCM N Ω) (s : M.FixedValues) (P : Finset (SWIGNode N)) (hP : M.ObsParentClosed P) (x : ValuesOn M.observed (swigΩ Ω)) {S : Finset (Finset (SWIGNode N))} (hS : S ⊆ M.toSWIGGraph.cComponentSet) : MeasurableSet[ comap (fun ℓ : M.LatentValues => fun u : S.biUnion (latentBlockIndex M) => ℓ u) inferInstance] (⋂ C ∈ S, {ℓ : M.LatentValues | ∀ v (hv : v ∈ C ∩ P), M.localConsistent s x v (hP.1 (mem_of_mem_inter_right hv)) ℓ}) := by classical refine measurableSet_comap_piFinset_of_depends (S := S.biUnion (latentBlockIndex M)) _ ?_ intro ℓ ℓ' hagree constructor · intro hℓ rw [Set.mem_iInter] at hℓ rw [Set.mem_iInter] intro C have hℓC := hℓ C rw [Set.mem_iInter] at hℓC rw [Set.mem_iInter] intro hCS v hv have hvC : v ∈ C := Finset.mem_of_mem_inter_left hv have hcomp : M.toSWIGGraph.cComponentOf v = C := M.toSWIGGraph.cComponentOf_eq_of_mem_cComponentSet (hS hCS) hvC exact (M.localConsistent_depends_only_on_block s x v (hP.1 (mem_of_mem_inter_right hv)) ℓ ℓ' (by intro u hu have huC : u ∈ M.latentBlock C := by simpa [hcomp] using hu have hmemBlock : (⟨u, (Finset.mem_filter.mp huC).1⟩ : {u // u ∈ M.unobserved}) ∈ latentBlockIndex M C := (mem_latentBlockIndex_iff M C _).mpr huC have hmem : (⟨u, (Finset.mem_filter.mp huC).1⟩ : {u // u ∈ M.unobserved}) ∈ S.biUnion (latentBlockIndex M) := by rw [Finset.mem_biUnion] exact ⟨C, hCS, hmemBlock⟩ have hcoord := hagree ⟨u, (Finset.mem_filter.mp huC).1⟩ hmem simpa using hcoord)).mp (hℓC hCS v hv) · intro hℓ' rw [Set.mem_iInter] at hℓ' rw [Set.mem_iInter] intro C have hℓ'C := hℓ' C rw [Set.mem_iInter] at hℓ'C rw [Set.mem_iInter] intro hCS v hv have hvC : v ∈ C := Finset.mem_of_mem_inter_left hv have hcomp : M.toSWIGGraph.cComponentOf v = C := M.toSWIGGraph.cComponentOf_eq_of_mem_cComponentSet (hS hCS) hvC exact (M.localConsistent_depends_only_on_block s x v (hP.1 (mem_of_mem_inter_right hv)) ℓ' ℓ (by intro u hu have huC : u ∈ M.latentBlock C := by simpa [hcomp] using hu have hmemBlock : (⟨u, (Finset.mem_filter.mp huC).1⟩ : {u // u ∈ M.unobserved}) ∈ latentBlockIndex M C := (mem_latentBlockIndex_iff M C _).mpr huC have hmem : (⟨u, (Finset.mem_filter.mp huC).1⟩ : {u // u ∈ M.unobserved}) ∈ S.biUnion (latentBlockIndex M) := by rw [Finset.mem_biUnion] exact ⟨C, hCS, hmemBlock⟩ have hcoord := hagree ⟨u, (Finset.mem_filter.mp huC).1⟩ hmem simpa using hcoord.symm)).mp (hℓ'C hCS v hv)
    Causalean.SCM.localConsistent_biInter_event_measurable_comap_latentBlockIndex · Causalean/SCM/ID/Density/QMass/LatentBlocks.lean:227
  • localConsistent_depends_only_on_latentBlock_of_mem lemma — Local consistency at an observed node in a node set is unchanged when two latent assignments agree on every unobserved parent of a node in that set.
    hypotheses
    N :
    Type u_1
    N → Type u_2
    shared
    M :
    SCM N Ω
    s :
    M.FixedValues
    x :
    ValuesOn M.observed (swigΩ Ω)
    U :
    Finset (SWIGNode N)
    v :
    SWIGNode N
    hvU :
    v ∈ U
    hv :
    v ∈ M.observed
    ℓ ℓ' :
    M.LatentValues
    hℓ :
    ∀ u (hu : u ∈ M.latentBlock U),
    ℓ ⟨u, (Finset.mem_filter.mp hu).1⟩ = ℓ' ⟨u, (Finset.mem_filter.mp hu).1⟩
    conclusion
    M.localConsistent s x v hv ℓ ↔ M.localConsistent s x v hv ℓ'
    Proof (Lean source)
    lemma localConsistent_depends_only_on_latentBlock_of_mem (M : SCM N Ω) (s : M.FixedValues) (x : ValuesOn M.observed (swigΩ Ω)) {U : Finset (SWIGNode N)} {v : SWIGNode N} (hvU : v ∈ U) (hv : v ∈ M.observed) (ℓ ℓ' : M.LatentValues) (hℓ : ∀ u (hu : u ∈ M.latentBlock U), ℓ ⟨u, (Finset.mem_filter.mp hu).1⟩ = ℓ' ⟨u, (Finset.mem_filter.mp hu).1⟩) : M.localConsistent s x v hv ℓ ↔ M.localConsistent s x v hv ℓ' := by unfold localConsistent set j : Fin M.observed.card := M.observedIndex ⟨v, hv⟩ with hj have hat : (M.observedAt j).val = v := by rw [hj] exact M.observedAt_observedIndex ⟨v, hv⟩ have hfun : M.structFun (M.observedAt j) (fun w => M.parentMap s ℓ j.isLt (prevFromObservedValues M x) w) = M.structFun (M.observedAt j) (fun w => M.parentMap s ℓ' j.isLt (prevFromObservedValues M x) w) := by congr 1 funext w by_cases huo : w.val ∈ M.unobserved · rw [parentMap_unobserved M s ℓ j.isLt _ w huo, parentMap_unobserved M s ℓ' j.isLt _ w huo] have hedge_v : M.dag.edge w.val v := by have hedge_at : M.dag.edge w.val (M.observedAt j).val := M.dag.mem_parents.mp w.property simpa [hat] using hedge_at have huBlock : w.val ∈ M.latentBlock U := by rw [latentBlock, mem_filter] exact ⟨huo, ⟨v, hvU, hedge_v⟩⟩ exact hℓ w.val huBlock · by_cases hfix : w.val ∈ M.fixed · rw [parentMap_fixed M s ℓ j.isLt _ w hfix, parentMap_fixed M s ℓ' j.isLt _ w hfix] · have hedge : M.dag.edge w.val (M.observedAt j).val := M.dag.mem_parents.mp w.property have hobs : w.val ∈ M.observed := by rcases Finset.mem_union.mp (M.dag_edges_classified _ _ hedge).1 with h1 | h2 · rcases Finset.mem_union.mp h1 with hfx | hob · exact absurd hfx hfix · exact hob · exact absurd h2 huo rw [parentMap_observed M s ℓ j.isLt _ w hobs, parentMap_observed M s ℓ' j.isLt _ w hobs] subst j change ((M.observedAt_observedIndex ⟨v, hv⟩) ▸ M.structFun (M.observedAt (M.observedIndex ⟨v, hv⟩)) (fun w => M.parentMap s ℓ (M.observedIndex ⟨v, hv⟩).isLt (prevFromObservedValues M x) w) = x ⟨v, hv⟩) ↔ ((M.observedAt_observedIndex ⟨v, hv⟩) ▸ M.structFun (M.observedAt (M.observedIndex ⟨v, hv⟩)) (fun w => M.parentMap s ℓ' (M.observedIndex ⟨v, hv⟩).isLt (prevFromObservedValues M x) w) = x ⟨v, hv⟩) rw [hfun]
    Causalean.SCM.localConsistent_depends_only_on_latentBlock_of_mem · Causalean/SCM/ID/Density/QMass/LatentBlocks.lean:304
  • localConsistent_event_measurable_comap_latentBlockIndex_of_family lemma — Given a finite structural causal model, fixed assignment, observed node family, and observed assignment, if the family is observed, then the latent assignments locally consistent at every node in the family form a measurable event.
    hypotheses
    N :
    Type u_1
    N → Type u_2
    shared
    ∀ n, Fintype (Ω n)
    ∀ n, MeasurableSingletonClass (Ω n)
    M :
    SCM N Ω
    s :
    M.FixedValues
    U :
    Finset (SWIGNode N)
    hUobs :
    U ⊆ M.observed
    x :
    ValuesOn M.observed (swigΩ Ω)
    conclusion
    MeasurableSet[ comap (fun ℓ : M.LatentValues => fun u : latentBlockIndex M U => ℓ u) inferInstance] {ℓ : M.LatentValues | ∀ v (hv : v ∈ U), M.localConsistent s x v (hUobs hv) ℓ}
    Proof (Lean source)
    lemma localConsistent_event_measurable_comap_latentBlockIndex_of_family [∀ n, Fintype (Ω n)] [∀ n, MeasurableSingletonClass (Ω n)] (M : SCM N Ω) (s : M.FixedValues) (U : Finset (SWIGNode N)) (hUobs : U ⊆ M.observed) (x : ValuesOn M.observed (swigΩ Ω)) : MeasurableSet[ comap (fun ℓ : M.LatentValues => fun u : latentBlockIndex M U => ℓ u) inferInstance] {ℓ : M.LatentValues | ∀ v (hv : v ∈ U), M.localConsistent s x v (hUobs hv) ℓ} := by classical refine measurableSet_comap_piFinset_of_depends (S := latentBlockIndex M U) _ ?_ intro ℓ ℓ' hagree constructor · intro hℓ v hv exact (localConsistent_depends_only_on_latentBlock_of_mem M s x hv (hUobs hv) ℓ ℓ' (by intro u hu have hmem : (⟨u, (Finset.mem_filter.mp hu).1⟩ : {u // u ∈ M.unobserved}) ∈ latentBlockIndex M U := (mem_latentBlockIndex_iff M U _).mpr hu have hcoord := hagree ⟨u, (Finset.mem_filter.mp hu).1⟩ hmem simpa using hcoord)).mp (hℓ v hv) · intro hℓ' v hv exact (localConsistent_depends_only_on_latentBlock_of_mem M s x hv (hUobs hv) ℓ' ℓ (by intro u hu have hmem : (⟨u, (Finset.mem_filter.mp hu).1⟩ : {u // u ∈ M.unobserved}) ∈ latentBlockIndex M U := (mem_latentBlockIndex_iff M U _).mpr hu have hcoord := hagree ⟨u, (Finset.mem_filter.mp hu).1⟩ hmem simpa using hcoord.symm)).mp (hℓ' v hv)
    Causalean.SCM.localConsistent_event_measurable_comap_latentBlockIndex_of_family · Causalean/SCM/ID/Density/QMass/LatentBlocks.lean:367
Prefix 1 core · 1 supporting This file proves positivity of the do-model ancestral marginal under positive observational mass and the ENNReal telescoping identity used to turn successive prefix-mass ratios into a district factor. ★ doObsKernelAncestralMarginal_positiveMass

Positivity and telescoping for prefix q-masses

This file proves positivity of the do-model ancestral marginal under positive observational mass and the ENNReal telescoping identity used to turn successive prefix-mass ratios into a district factor.

lemma doObsKernelAncestralMarginal_positiveMass reviewed
Causalean.SCM.ID

For an intervention set X whose random copies are observed and whose fixed copies are not already frozen, a positive observational kernel at every fixed-value assignment, and an outcome set Y disjoint from the random copies of X, the do(X)-law ancestral marginal kernel used in the identification density assembly also has everywhere-positive point mass.

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 :
Finset N
hObs :
∀ D ∈ X, SWIGNode.random D ∈ M.observed
hFix :
∀ D ∈ X, SWIGNode.fixed D ∉ M.fixed
Y :
Finset (SWIGNode N)
hpos :
∀ s' : M.FixedValues, DiscreteID.PositiveMass (M.obsKernel s')
hYX :
∀ d ∈ X, SWIGNode.random d ∉ Y
sDo :
(M.fixSet X hObs hFix).FixedValues
conclusion
DiscreteID.PositiveMass (doObsKernelAncestralMarginal M X hObs hFix Y sDo)
Proof (Lean source)
lemma doObsKernelAncestralMarginal_positiveMass [∀ 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)) (hpos : ∀ s' : M.FixedValues, DiscreteID.PositiveMass (M.obsKernel s')) (hYX : ∀ d ∈ X, SWIGNode.random d ∉ Y) (sDo : (M.fixSet X hObs hFix).FixedValues) : DiscreteID.PositiveMass (doObsKernelAncestralMarginal M X hObs hFix Y sDo) := by classical let MX := M.fixSet X hObs hFix let D := fixObservedAncestralSet M X hObs hFix Y let A := fixAncestralSet M X hObs hFix Y have hDclosed : MX.ObsParentClosed D := by simpa [MX, D] using fixObservedAncestralSet_obsParent_closed M X hObs hFix Y intro xD let xFull : ValuesOn M.observed (swigΩ Ω) := fun v => if hvD : v.val ∈ D then xD ⟨v.val, hvD⟩ else match v.val with | SWIGNode.random d => if hd : d ∈ X then sDo ⟨SWIGNode.fixed d, mem_union_right _ (Finset.mem_image.mpr ⟨d, hd, rfl⟩)⟩ else choice (inferInstance : Nonempty (swigΩ Ω (SWIGNode.random d))) | SWIGNode.fixed d => choice (inferInstance : Nonempty (swigΩ Ω (SWIGNode.fixed d))) let xDo : ValuesOn MX.observed (swigΩ Ω) := fun v => xFull ⟨v.val, v.property⟩ have hprojD : valuesProjection hDclosed.1 xDo = xD := by ext v simp [valuesProjection, xDo, xFull, v.property] have hpin : ∀ d (hd : d ∈ X), xFull ⟨SWIGNode.random d, hObs d hd⟩ = sDo ⟨SWIGNode.fixed d, mem_union_right _ (Finset.mem_image.mpr ⟨d, hd, rfl⟩)⟩ := by intro d hd have hnotD : SWIGNode.random d ∉ D := by intro hdD have hdA : SWIGNode.random d ∈ A := (Finset.mem_inter.mp hdD).1 exact hYX d hd ((random_intervened_mem_fixAncestralSet_iff_mem_Y M X hObs hFix Y hd).mp hdA) simp [xFull, hnotD, hd] have hobsAgree : ∀ w (hw : w ∈ M.observed), xDo ⟨w, by simpa [MX, SCM.fixSet_observed] using hw⟩ = xFull ⟨w, hw⟩ := by intro w hw rfl have hq_ne : ∀ C ∈ MX.toSWIGGraph.cComponentSet, MX.qLocalMass sDo (C ∩ D) (fun _ hv => hDclosed.1 (Finset.mem_of_mem_inter_right hv)) xDo ≠ 0 := by intro C _hC have hsubsetM : C ∩ D ⊆ M.observed := by intro v hv have hvD : v ∈ D := Finset.mem_of_mem_inter_right hv exact Finset.inter_subset_right hvD have hqeq : MX.qLocalMass sDo (C ∩ D) (fun _ hv => hDclosed.1 (Finset.mem_of_mem_inter_right hv)) xDo = M.qLocalMass (M.fixSetProj X hObs hFix sDo) (C ∩ D) hsubsetM xFull := by simp only [causal_defs_simps] congr 1 ext ℓ constructor · intro hLocal v hv have hvD : v ∈ D := Finset.mem_of_mem_inter_right hv have hnot : v ∉ X.image SWIGNode.random := by intro hvX rcases Finset.mem_image.mp hvX with ⟨d, hd, rfl⟩ have hdA : SWIGNode.random d ∈ A := (Finset.mem_inter.mp hvD).1 exact hYX d hd ((random_intervened_mem_fixAncestralSet_iff_mem_Y M X hObs hFix Y hd).mp hdA) exact (localConsistent_fixSet_iff M X hObs hFix sDo (M.fixSetProj X hObs hFix sDo) xDo xFull v ((fun _ hv => hDclosed.1 (Finset.mem_of_mem_inter_right hv)) v hv) (hsubsetM hv) hnot hobsAgree hpin rfl ℓ).mp (hLocal v hv) · intro hLocal v hv have hvD : v ∈ D := Finset.mem_of_mem_inter_right hv have hnot : v ∉ X.image SWIGNode.random := by intro hvX rcases Finset.mem_image.mp hvX with ⟨d, hd, rfl⟩ have hdA : SWIGNode.random d ∈ A := (Finset.mem_inter.mp hvD).1 exact hYX d hd ((random_intervened_mem_fixAncestralSet_iff_mem_Y M X hObs hFix Y hd).mp hdA) exact (localConsistent_fixSet_iff M X hObs hFix sDo (M.fixSetProj X hObs hFix sDo) xDo xFull v ((fun _ hv => hDclosed.1 (Finset.mem_of_mem_inter_right hv)) v hv) (hsubsetM hv) hnot hobsAgree hpin rfl ℓ).mpr (hLocal v hv) rw [hqeq] exact M.qLocalMass_pos_of_positiveObs (M.fixSetProj X hObs hFix sDo) (hpos (M.fixSetProj X hObs hFix sDo)) (C ∩ D) hsubsetM xFull have hmass := MX.obsKernel_marginal_singleton_eq_prod_qLocalMass sDo D hDclosed xDo have hkey : doObsKernelAncestralMarginal M X hObs hFix Y = MX.obsKernel.map (valuesProjection hDclosed.1) := rfl unfold DiscreteID.singletonMass rw [hkey, ProbabilityTheory.Kernel.map_apply _ (measurable_valuesProjection hDclosed.1), ← hprojD, hmass] exact Finset.prod_ne_zero_iff.mpr hq_ne
Causalean.SCM.ID.doObsKernelAncestralMarginal_positiveMass · Causalean/SCM/ID/Density/QMass/Prefix.lean:40 · uses SWIGNode , instMeasurableSpaceSwigΩ , swigΩ , ValuesOn , SCM , FixedValues , PositiveMass , doObsKernelAncestralMarginal , fixObservedAncestralSet , ObservedValues , fixSet , obsKernel
1 supporting declaration (lemmas, instances)
  • prod_filter_div_telescope lemma — Pure ENNReal telescope for products of selected adjacent ratios.
    hypotheses
    a :
    ℕ → ENNReal
    m :
    ℕ
    T :
    Finset ℕ
    hT :
    T ⊆ range m
    hne :
    ∀ i ≤ m, a i ≠ 0
    hfin :
    ∀ i ≤ m, a i ≠ ⊤
    hconst :
    ∀ i < m
    if
    i ∉ T
    then
    a (i + 1) = a i
    conclusion
    ∏ i ∈ T, a (i + 1) / a i = a m / a 0
    Proof (Lean source)
    lemma prod_filter_div_telescope (a : ℕ → ENNReal) (m : ℕ) (T : Finset ℕ) (hT : T ⊆ range m) (hne : ∀ i ≤ m, a i ≠ 0) (hfin : ∀ i ≤ m, a i ≠ ⊤) (hconst : ∀ i < m, i ∉ T → a (i + 1) = a i) : ∏ i ∈ T, a (i + 1) / a i = a m / a 0 := by classical have hrange_all : ∀ n : ℕ, (∀ i ≤ n, a i ≠ 0) → (∀ i ≤ n, a i ≠ ⊤) → ∏ i ∈ range n, a (i + 1) / a i = a n / a 0 := by intro n hnne hnfin induction n with | zero => simp [ENNReal.div_self (hnne 0 le_rfl) (hnfin 0 le_rfl)] | succ m ih => rw [Finset.prod_range_succ] have hih : ∏ i ∈ range m, a (i + 1) / a i = a m / a 0 := ih (fun i hi => hnne i (le_trans hi (le_succ m))) (fun i hi => hnfin i (le_trans hi (le_succ m))) rw [hih] rw [div_eq_mul_inv, div_eq_mul_inv, div_eq_mul_inv] rw [show a m * (a 0)⁻¹ * (a (m + 1) * (a m)⁻¹) = a (m + 1) * (a m * (a m)⁻¹) * (a 0)⁻¹ by ac_rfl] rw [ENNReal.mul_inv_cancel (hnne m (le_succ m)) (hnfin m (le_succ m))] simp have hrange : ∏ i ∈ range m, a (i + 1) / a i = a m / a 0 := hrange_all m hne hfin have hsubset : ∏ i ∈ T, a (i + 1) / a i = ∏ i ∈ range m, a (i + 1) / a i := by exact Finset.prod_subset hT (by intro i hiRange hiT have hi_lt : i < m := Finset.mem_range.mp hiRange rw [hconst i hi_lt hiT] exact ENNReal.div_self (hne i (le_of_lt hi_lt)) (hfin i (le_of_lt hi_lt))) rw [hsubset, hrange]
    Causalean.SCM.ID.prod_filter_div_telescope · Causalean/SCM/ID/Density/QMass/Prefix.lean:152