Discovery.InvariantPrediction
Population identification of the direct causes of a target variable from the invariance of its conditional law across interventional environments, after Peters, Bühlmann & Meinshausen, *Causal inference using invariant p
Model 6 core · 3 supporting Formalization of the setup of Peters, Bühlmann & Meinshausen, *Causal inference using invariant prediction* (JRSS-B 2016, arXiv:1501.01332). ★ EnvFamily★ paFix_eq
Invariant Causal Prediction: environment-family model layer
Formalization of the setup of Peters, Bühlmann & Meinshausen, Causal inference
using invariant prediction (JRSS-B 2016, arXiv:1501.01332).
An environment family is a finite collection of structural causal models
{M i} over a common set of observed and latent variables, indexed by an
environment label i. Each M i arises from interventions that may differ
between environments, but never act on the target node Y: every
environment shares the target's structural mechanism (hStruct), the target's
parent set (hParents), and the latent-noise law (hLatent). Each environment
also carries the values s i assigned to its intervened (fixed) coordinates,
because an intervention do(X = x) fixes those coordinates to x.
The only observable content per environment is the conditional law of the target
Y given a set of predictors X_S, read off from (M i).obsCondKernel {Y} S
evaluated at s i. Here invariance asks which predictor sets S make these
laws instances of one conditional rule with the target's fixed-parent values as
explicit inputs. Evaluating that rule at different fixed-parent values may
produce different laws across environments.
An environment family for Invariant Causal Prediction (Peters, Bühlmann & Meinshausen 2016) bundles a finite, Fintype-indexed collection of structural causal models sharing a common target variable that every environment observes, a common observed-variable set, and a common latent-variable set. The environments never intervene on the target: they share the target's parent set, the target's structural mechanism, and the latent-noise law, while each environment carries the values assigned to its own intervened coordinates. It further packages the regularity needed to disintegrate the joint law into the target's conditional law given any predictor set — a standard Borel and nonempty target value space, and countable generation of the relevant kernels, and states the exogeneity assumption that in every environment the target's exogenous (latent) parents are independent of its observed parents under the joint law.
Definition (Lean source)
The target node is the random-form outcome whose conditional law is compared across family F, over finite nodes, finite environments, and measurable coordinate outcomes.
The target's observed-parent set is the causally sufficient conditioning candidate available in environment i of family F, over finite nodes, finite environments, and measurable coordinate outcomes.
The target's fixed-parent set records which direct causes are assigned rather than random in environment i of family F; their values must remain arguments of the invariant mechanism. The setup uses finite nodes, finite environments, and measurable coordinate outcomes.
The target has the same fixed-parent set in any two environments, namely environments i and j of family F over finite nodes, finite environments, and measurable coordinate outcomes.
Formal statement
Proof (Lean source)
The fixed-parent values expose the intervention assignments that the target mechanism must condition on in environment i of family F, over finite nodes, finite environments, and measurable coordinate outcomes.
Definition (Lean source)
3 supporting declarations (lemmas, instances)
-
paObs_eqtheorem — paObs does not depend on the chosen environment.hypothesesconclusionF.paObs i = F.paObs j -
fixed_parent_mem_fixed_of_memtheorem — A target parent that is fixed in one environment is fixed in every environment. The point is not that EnvFamily shares the whole fixed set, but that it shares the target parent set (E4), and a fixed-form SWIG node cannot be an observed or unobserved random-form node in the other environment, while a parent of Y is always classified as fixed/observed/unobserved (dag_edges_classified).hypothesesN :sharedType u_1N → Type u_2ι :sharedType u_3i j :ιd :SWIGNode Nhd :d ∈ (F.M i).dag.parents F.yNode ∩ (F.M i).fixedconclusiond ∈ (F.M j).fixedProof (Lean source)
theorem fixed_parent_mem_fixed_of_mem {i j : ι} {d : SWIGNode N} (hd : d ∈ (F.M i).dag.parents F.yNode ∩ (F.M i).fixed) : d ∈ (F.M j).fixed := by classical have hd_parent_i : d ∈ (F.M i).dag.parents F.yNode := (Finset.mem_inter.mp hd).1 have hd_fixed_i : d ∈ (F.M i).fixed := (Finset.mem_inter.mp hd).2 have hd_parent_j : d ∈ (F.M j).dag.parents F.yNode := by rw [← F.hParents i j] exact hd_parent_i have hedge_j : (F.M j).dag.edge d F.yNode := (F.M j).dag.mem_parents.mp hd_parent_j have hclass_j : d ∈ (F.M j).fixed ∪ (F.M j).observed ∪ (F.M j).unobserved := ((F.M j).dag_edges_classified d F.yNode hedge_j).1 rcases (F.M i).fixed_is_fixed d hd_fixed_i with ⟨n, rfl⟩ rcases Finset.mem_union.mp hclass_j with hfo | hunobs · rcases Finset.mem_union.mp hfo with hfixed | hobs · exact hfixed · rcases (F.M j).observed_is_random (SWIGNode.fixed n) hobs with ⟨m, hm⟩ cases hm · rcases (F.M j).unobserved_is_random (SWIGNode.fixed n) hunobs with ⟨m, hm⟩ cases hm -
paFix_subset_fixedtheorem — The fixed parents are a subset of the fixed coordinates, so they can be read off the environment's intervention assignment s i.hypothesesconclusionF.paFix i ⊆ (F.M i).fixedProof (Lean source)
theorem paFix_subset_fixed (i : ι) : F.paFix i ⊆ (F.M i).fixed := inter_subset_right
IdentifiedSet 3 core · 1 supporting The identified set S(E) is the intersection of all invariant predictor sets. ★ idSet★ paObs_mem_invariantSets
Invariant Causal Prediction: the identified set S(E)
The identified set S(E) is the intersection of all invariant predictor
sets. By mechanism_invariant the target's observed parents are invariant, so
the collection is nonempty and S(E) is contained in the parents — the
soundness direction (proved in Soundness.lean).
The invariant predictor collection retains exactly the finite node sets observed throughout an environment family and make the target's conditional law stable across its finite environments, for finite nodes with measurable coordinate outcomes.
The ICP identified set contains precisely the nodes that survive every invariant predictor specification admitted by the environment family, over finite nodes, finite environments, and measurable coordinate outcomes.
The target's observed parents belong to the invariant predictor collection, so the ICP intersection ranges over a causally sufficient candidate selected in environment i₀ of family F, over finite nodes, finite environments, and measurable coordinate outcomes.
Formal statement
Proof (Lean source)
1 supporting declaration (lemmas, instances)
-
idSet_subset_of_memtheorem — The identified set is contained in every invariant set.hypothesesN :sharedType u_1N → Type u_2ι :sharedType u_3F :EnvFamily N Ω ιhT :T ∈ F.invariantSetsconclusionF.idSet ⊆ TProof (Lean source)
theorem idSet_subset_of_mem (F : EnvFamily N Ω ι) {T : Set (SWIGNode N)} (hT : T ∈ F.invariantSets) : F.idSet ⊆ T := Set.sInter_subset_of_mem hT
Invariance 3 core · 1 supporting A predictor set S is invariant across an environment family when the conditional laws of the target Y given X_S share one rule after the target's fixed-parent values are treated as explicit inputs. ★ Invariant★ mechanism_invariant
Invariant Causal Prediction: the invariance predicate and mechanism invariance
A predictor set S is invariant across an environment family when the
conditional laws of the target Y given X_S share one rule after the target's
fixed-parent values are treated as explicit inputs. In each environment,
obsCondKernel {Y} S evaluated at its intervention values s i agrees with the
common rule at that environment's fixed-parent values; the resulting evaluated
laws may differ when those values differ.
The central structural fact is mechanism_invariant: the target's own observed
parents paObs always form an invariant set, because conditioning on the parents
exposes the target's structural mechanism, which every environment shares
(hStruct/hLatent/hParents). This is the engine behind soundness
(S(E) ⊆ PA(Y)).
Throughout we assume the per-coordinate value spaces are standard Borel and
nonempty; the finite-measure and countably-generated obligations of
obsCondKernel are threaded as instance hypotheses.
The target set singles out the random-form outcome whose conditional distribution ICP compares across an environment family, over finite nodes, finite environments, and measurable coordinate outcomes.
A predictor set observed in every environment is invariant for a family of intervention environments when the target's conditional law depends only on the predictors and fixed parent values: the common conditional rule agrees across environments after fixed-parent values are aligned, and each environment's observed conditional law agrees with that rule at its own fixed-parent values. This applies to finite nodes, finitely many environments, and measurable coordinate outcomes.
Definition (Lean source)
Mechanism invariance (the heart of soundness). For an environment family and a target index i₀, the target's observed parents paObs form an invariant set: in every environment the conditional law of the target given its observed parents equals one fixed structural factor, so ICP never rejects the parents.
Formal statement
Proof (Lean source)
1 supporting declaration (lemmas, instances)
-
paObs_subset_observedtheorem — The observed parents form a valid conditioning set in every environment.hypothesesN :sharedType u_1N → Type u_2ι :sharedType u_3F :EnvFamily N Ω ιi j :ιconclusionF.paObs i ⊆ (F.M j).observedProof (Lean source)
theorem paObs_subset_observed (F : EnvFamily N Ω ι) (i j : ι) : F.paObs i ⊆ (F.M j).observed := by rw [F.paObs_eq i j] unfold paObs exact inter_subset_right
Soundness 1 core · 0 supporting This file proves the soundness theorem for invariant causal prediction: icp_sound states that the identified set S(E) is contained in the target's observed parents PA(Y). ★ icp_sound
Invariant Causal Prediction: soundness
This file proves the soundness theorem for invariant causal prediction:
icp_sound states that the identified set S(E) is contained in the target's
observed parents PA(Y). Thus every variable selected by ICP is a genuine
direct cause in the observed parent set.
This is a population set-inclusion consequence of the mechanism validity
represented by Proposition 1 in Peters–Bühlmann–Meinshausen. The parent set is
itself invariant (paObs_mem_invariantSets), and the ICP identified set is the
intersection of all invariant sets (idSet_subset_of_mem), so it must be
contained in the parents. The paper's Theorem 1 is a finite-sample coverage
result and is not asserted here.
Population ICP soundness from parent-set invariance. For an environment family and an index i₀ selecting the target's observed-parent set, the identified set is contained in the target's observed parents: every node selected by ICP is a genuine direct cause.