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.
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)
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) := (M.hXmeas j).sub (measurable_sum _ (fun k _ => (M.hXmeas k).const_mul _)) 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)
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.
The causal coefficient γ* = β₀,· (row 0 of β).
Definition (Lean source)
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