Discovery.InvariantPrediction.LinearGaussian.Helpers
Linear-Gaussian invariant-prediction helpers: intervention invariance, centered-noise moments, and residual algebra for soundness and completeness proofs.
Invariance 1 core · 0 supporting The structural backbone of the mean-shift argument (propos:sem): under a single do-intervention do(X_{k₀} = a), every coordinate that is not a descendant of k₀ and is not k₀ itself keeps its observational value a.e. ★ nonDescendant_invariance
Invariant Causal Prediction — non-descendant invariance
The structural backbone of the mean-shift argument (propos:sem): under a single
do-intervention do(X_{k₀} = a), every coordinate that is not a descendant of
k₀ and is not k₀ itself keeps its observational value a.e.
nonDescendant_invariance proves, for the single-intervention environment
e with A = {k₀}, that e.X ω k = M.X ω k a.e. for every k ≠ k₀ with
¬ dag.isAncestor k₀ k (i.e. k is not a strict descendant of k₀). This
includes nodes incomparable with k₀ and ancestors of k₀, exactly the
"upstream + sideways" part of the graph the intervention cannot reach; the
intervened node k₀ is excluded because it is pinned to the assigned constant.
The proof is a strong induction along the topological order: each such k
satisfies the same structural equation in both worlds (hDoStruct k vs
hε k, since k ≠ k₀ so k ∉ A), and all its parents are also non-descendants
of k₀ with strictly smaller topological order, so they agree by induction.
Non-descendant invariance. Let e be an environment of the observational SEM M in which the single intervened coordinate is k₀. Then every coordinate k that is neither k₀ nor a descendant of k₀ in the observational DAG keeps its observational value almost surely: Xₖᵉ = Xₖ¹. (The node k₀ itself is pinned to the assigned constant, hence excluded.)
Formal statement
Proof (Lean source)
Moments 1 core · 2 supporting The structural noises εⱼ of the observational SEM are centered Gaussian (hGauss), hence integrable with mean 0. ★ eps_integral_zero
Invariant Causal Prediction — Gaussian-noise moments
The structural noises εⱼ of the observational SEM are centered Gaussian
(hGauss), hence integrable with mean 0. These two facts feed the mean-shift
integral computation in the completeness proof.
eps_integrable— eachεⱼisM.P-integrable.eps_integral_zero—E[εⱼ] = 0.
For a linear-Gaussian observational SEM and coordinate index j, the structural noise εⱼ is centered: its expectation under M's probability measure is zero.
Formal statement
Proof (Lean source)
2 supporting declarations (lemmas, instances)
-
eps_aemeasurabletheorem — εⱼ is a.e.-measurable: by the structural-residual identity hε it agrees a.e. with the measurable map Xⱼ − Σ_{k≠j} βⱼₖ Xₖ.Proof (Lean source)
@[fun_prop] theorem eps_aemeasurable (M : ObsSEM p) (j : Fin (p + 1)) : AEMeasurable (fun ω => M.ε ω j) M.P := by have hmeasRHS : Measurable (fun ω => M.X ω j - ∑ k ∈ Finset.univ.erase j, M.β j k * M.X ω k) := by fun_prop refine hmeasRHS.aemeasurable.congr ?_ filter_upwards [M.hε] with ω hω using (hω j).symm -
eps_integrabletheorem — The noise εⱼ is M.P-integrable (Gaussian marginal has a first moment).Proof (Lean source)
@[fun_prop] theorem eps_integrable (M : ObsSEM p) (j : Fin (p + 1)) : Integrable (fun ω => M.ε ω j) M.P := by have hmeas : AEMeasurable (fun ω => M.ε ω j) M.P := eps_aemeasurable M j -- The identity map is integrable against the Gaussian law (`MemLp id 1`), -- and integrability transfers back through `integrable_map_measure`. have hid : Integrable (id : ℝ → ℝ) (M.P.map (fun ω => M.ε ω j)) := by rw [M.hGauss j] exact (memLp_id_gaussianReal 1).integrable (by norm_num) rw [M.hGauss j] at hid -- transfer have := (integrable_map_measure (μ := M.P) (f := fun ω => M.ε ω j) (g := (id : ℝ → ℝ)) ?_ hmeas).mp (by rwa [M.hGauss j]) · simpa using this · rw [M.hGauss j]; exact (memLp_id_gaussianReal 1).aestronglyMeasurable
Residual 3 core · 1 supporting Algebraic helper lemmas for the completeness proof: with the *causal* coefficient γ* = β₀,·, the regression residual Y − Σ_k γ*_k X_k equals the target noise ε₀ a.e. ★ obsResidual_eq_eps★ envResidual_eq_eps
Invariant Causal Prediction — residual equals the target noise
Algebraic helper lemmas for the completeness proof: with the causal coefficient
γ* = β₀,·, the regression residual Y − Σ_k γ*_k X_k equals the target noise
ε₀ a.e. in every environment.
* obsResidual_eq_eps — observational block: from hε at the target row.
* envResidual_eq_eps — interventional block: from hDoStruct at the target
(the target is never intervened on, so it keeps its structural equation).
Both use that the target's own coefficient is 0 (hNoSelf) to turn the
Σ_{k≠0} of the structural equation into the full Σ_k of the residual.
For an observational linear-Gaussian structural equation model, the causal coefficient vector assigns to each variable its coefficient in the structural equation for the target outcome.
Observational residual is the target noise. For an observational SEM, evaluated at the causal coefficient γ* = β₀,·, the observational residual Y − Σ_k β₀ₖ X_k equals the target's structural noise ε₀ almost everywhere.
Formal statement
Proof (Lean source)
Interventional residual is the target noise. For an observational SEM and a do-intervention environment built on it — where the target is never itself intervened on, so it keeps its structural equation — the environment residual Yᵉ − Σ_k β₀ₖ Xₖᵉ, evaluated at the causal coefficient, equals the target's structural noise ε₀ almost everywhere.
Formal statement
Proof (Lean source)
1 supporting declaration (lemmas, instances)
-
sum_causalCoeff_eqtheorem — With the causal coefficient, the full-sum Σ_k β₀ₖ X_k equals the structural-equation sum Σ_{k≠0} β₀ₖ X_k, since β₀₀ = 0.hypotheses