Discovery.InvariantPrediction
Entry point for the formalization of Peters, Bühlmann & Meinshausen, *Causal inference using invariant prediction: identification and confidence intervals* (JRSS-B 2016, arXiv:1501.01332).
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. Invariant Causal Prediction asks which predictor sets S
make this conditional law the same across all 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 SWIGNode.random Y.
Definition (Lean source)
The observed parents of the target in environment i — the conditioning candidates ICP ranges over. Index-independent by hParents and hObs (see paObs_eq).
The fixed parents of the target in environment i — the parents of Y that are intervened on (fixed) in that environment. These are the coordinates of Y's mechanism whose values live in s i and may legitimately differ across environments; the redesigned Invariant predicate conditions on them.
For any two environments i and j, the fixed parents of the target coincide between environment i and environment j.
Formal statement
Proof (Lean source)
The fixed-parent values assigned by environment i's intervention, projected from s i.
Definition (Lean source)
3 supporting declarations (lemmas, instances)
-
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).hypothesesconclusiond ∈ (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.hypothesesi :ιconclusionF.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 collection of invariant predictor sets, viewed as sets of nodes.
The identified set S(E): the intersection of all invariant predictor sets across the environment family.
For an invariant-prediction environment family and an index i₀ selecting the target's observed-parent set, the target's observed parents form an invariant predictor set — the membership form of mechanism_invariant.
Formal statement
Proof (Lean source)
1 supporting declaration (lemmas, instances)
-
idSet_subset_of_memtheorem — The identified set is contained in every invariant set.Proof (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 law of the target Y given X_S — read off from obsCondKernel {Y} S evaluated at each environment's intervention values s i — is the *same* i ★ 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 law of the target Y given X_S — read off from
obsCondKernel {Y} S evaluated at each environment's intervention values s i
— is the same in every environment.
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 singleton node set {Y} used as the conditioned target.
S is invariant across the environment family F.
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.Proof (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.
The proof is the formal version of the standard Theorem 1 argument. 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.
Theorem 1 (soundness). 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.