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)
For a finite node-label set, measurable coordinate outcome spaces, a finite environment index set, and an invariant-prediction environment family, the target node is the random-form node associated with the family's target variable.
For a finite node-label set, measurable coordinate outcome spaces, a finite environment index set, an invariant-prediction environment family, and an environment, the observed-parent set of the target is the set of target parents that are observed in that environment.
For a finite node-label set, measurable coordinate outcome spaces, a finite environment index set, an invariant-prediction environment family, and an environment, the fixed-parent set of the target is the set of target parents that are fixed by intervention in that environment.
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)
For a finite node-label set, measurable coordinate outcome spaces, a finite environment index set, an invariant-prediction environment family, and an environment, the fixed-parent values are the values assigned by that environment's intervention, restricted to the target's fixed parents.
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).
For a finite node-label set, measurable coordinate outcome spaces, a finite environment index set, and an invariant-prediction environment family, the collection of invariant predictor sets consists exactly of node sets that can be represented by a finite predictor set observed in every environment and that satisfy invariance for that environment family.
For a finite node-label set, measurable coordinate outcome spaces, a finite environment index set, and an invariant-prediction environment family, the identified set is the intersection of all invariant predictor sets for that 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.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 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.
For a finite node-label set, measurable coordinate outcome spaces, a finite environment index set, and an invariant-prediction environment family, the target set is the singleton containing that family's random-form target node.
For a finite node-label set, measurable coordinate outcome spaces, a finite environment index set, an invariant-prediction environment family, and a finite predictor-node set that is observed in every environment, the assertion that this predictor set is invariant means that there exists a measure-valued rule for the target as a function of the predictor values and the values of fixed parents such that (1) after transporting fixed-parent values between environments, this law is the same in every pair of environments, and (2) in each environment, the observed conditional law of the target given the predictors agrees almost everywhere with that common law evaluated at that environment's fixed-parent values.
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.
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.