PO.Assumptions

shared

r :

Regime P.V P.X

ω :

P.Ω

v (hv : v ∈ r.target) :

def

FactualAgrees P r ω :

Prop

given by

P.eval Regime.empty ω v = r.assign v hv

Causalean.PO.POSystem.FactualAgrees · Causalean/PO/Assumptions/Consistency.lean:29 · uses POSystem , Regime

def IntermediateAgrees reviewed

Causalean.PO.POSystem

For a potential-outcome system, a first intervention regime, a second intervention regime, and a unit in its sample space, intermediate agreement means that, after the first intervention, every variable targeted by the second has exactly the value assigned by the second.

Definition (Lean source)

parameters

P :

shared

r₁ r₂ :

Regime P.V P.X

ω :

P.Ω

v (hv : v ∈ r₂.target) :

def

IntermediateAgrees P r₁ r₂ ω :

Prop

given by

P.eval r₁ ω v = r₂.assign v hv

Causalean.PO.POSystem.IntermediateAgrees · Causalean/PO/Assumptions/Consistency.lean:40 · uses POSystem , Regime

structure Consistency reviewed

Causalean.PO.POSystem

For a potential-outcome system, consistency says that whenever a unit factually receives an intervention regime, every non-target potential outcome under that regime equals its observed factual outcome.

Definition (Lean source)

parameters

P :

assumes

factual :

∀ (r : Regime P.V P.X) (Y : Finset P.V),

_root_.Disjoint Y r.target → ∀ ω : P.Ω, P.FactualAgrees r ω → P.poVariable r Y ω

= P.poVariable Regime.empty Y ω

Factual consistency.

Causalean.PO.POSystem.Consistency · Causalean/PO/Assumptions/Consistency.lean:51 · uses POSystem

structure CompositionConsistency reviewed

Causalean.PO.POSystem

For a potential-outcome system, composition consistency for nested or sequential interventions says that an intervention which assigns variables their values after a first disjoint intervention can be removed from the composed regime.

Definition (Lean source)

parameters

P :

assumes

composition :

∀ (r₁ r₂ : Regime P.V P.X) (h : r₁.Disjoint r₂) (Y : Finset P.V),

_root_.Disjoint Y (r₁.target ∪ r₂.target) → ∀ ω : P.Ω, P.IntermediateAgrees r₁ r₂ ω → P.poVariable (r₁.sqcup r₂ h) Y ω

= P.poVariable r₁ Y ω

Composition / nested consistency.

Causalean.PO.POSystem.CompositionConsistency · Causalean/PO/Assumptions/Consistency.lean:69 · uses POSystem

ConsistencyLemmas 1 core · 8 supporting This file provides reusable pointwise consistency combinators for empty, singleton, and disjoint-union regimes, together with generic event-level rewrites for POVar counterfactual values. ★ cf_eq_factual_of_factualAgrees

Pointwise consistency lemmas for potential-outcome variables

This file provides reusable pointwise consistency combinators for empty, singleton, and disjoint-union regimes, together with generic event-level rewrites for POVar counterfactual values. These lemmas factor the consistency arguments used by LATE, frontdoor, dynamic regimes, and other multi-target PO identification files. Important results include POSystem.factualAgrees_empty, POSystem.factualAgrees_sqcup, POVar.factualAgrees_single, POVar.cf_eq_factual_on_event, and the integrated indicator rewrites POVar.factual_mul_indicator_eq_cfUnder_mul_indicator and POVar.factual_mul_indicator_eq_cf_mul_indicator.

theorem cf_eq_factual_of_factualAgrees reviewed

Causalean.PO.POVar

Multi-target consistency. Under the consistency (SUTVA) assumption on the potential-outcome system, for a regimed variable a whose index does not lie in the target of a regime r, if the outcome ω factually agrees with the regime r, then the counterfactual value of a under r at ω equals its factual value at ω.

Formal statement

hypotheses

P :

α :

Type*

hC :

P.Consistency

a :

POVar P α

r :

Regime P.V P.X

h_notmem :

a.v ∉ r.target

ω :

P.Ω

hAgrees :

P.FactualAgrees r ω

conclusion

a.cf r ω = a.factual ω

Proof (Lean source)

theorem POVar.cf_eq_factual_of_factualAgrees {P : POSystem} {α : Type*} [MeasurableSpace α] (hC : P.Consistency) (a : POVar P α) (r : Regime P.V P.X) (h_notmem : a.v ∉ r.target) (ω : P.Ω) (hAgrees : P.FactualAgrees r ω) : a.cf r ω = a.factual ω := by -- Disjointness: `{a.v}` is disjoint from `r.target`. have hdisj : _root_.Disjoint ({a.v} : Finset P.V) r.target := by simpa [Finset.disjoint_singleton_left] using h_notmem -- Apply `hC.factual`. have hPoEq := hC.factual r {a.v} hdisj ω hAgrees have haEq : P.eval r ω a.v = P.eval Regime.empty ω a.v := by simpa [POSystem.poVariable] using congrFun hPoEq ⟨a.v, mem_singleton_self a.v⟩ -- Push through `a.equiv`. change a.equiv (P.eval r ω a.v) = a.equiv (P.eval Regime.empty ω a.v) exact congrArg a.equiv haEq

Causalean.PO.POVar.cf_eq_factual_of_factualAgrees · Causalean/PO/Assumptions/ConsistencyLemmas.lean:204 · uses POSystem , Consistency , FactualAgrees , POVar , cf , factual , Regime

8 supporting declarations (lemmas, instances)

factualAgrees_empty theorem — FactualAgrees holds vacuously for the empty regime.

hypotheses

P :

POSystem
shared

ω :

P.Ω

conclusion

P.FactualAgrees Regime.empty ω

Proof (Lean source)

theorem factualAgrees_empty (ω : P.Ω) : P.FactualAgrees Regime.empty ω := by intro v hv exact (notMem_empty v hv).elim

Causalean.PO.POSystem.factualAgrees_empty · Causalean/PO/Assumptions/ConsistencyLemmas.lean:49
factualAgrees_sqcup theorem — Combinator: FactualAgrees for a disjoint union reduces to FactualAgrees for each component.

hypotheses

P :

POSystem
shared

r₁ r₂ :

Regime P.V P.X

h :

r₁.Disjoint r₂

ω :

P.Ω

h₁ :

P.FactualAgrees r₁ ω

h₂ :

P.FactualAgrees r₂ ω

conclusion

P.FactualAgrees (r₁.sqcup r₂ h) ω

Proof (Lean source)

theorem factualAgrees_sqcup {r₁ r₂ : Regime P.V P.X} (h : r₁.Disjoint r₂) {ω : P.Ω} (h₁ : P.FactualAgrees r₁ ω) (h₂ : P.FactualAgrees r₂ ω) : P.FactualAgrees (r₁.sqcup r₂ h) ω := by intro v hv -- `v ∈ r₁.target ∪ r₂.target`. have hv' : v ∈ r₁.target ∪ r₂.target := by simpa only [Regime.sqcup_target] using hv by_cases hv₁ : v ∈ r₁.target · -- `r₁.sqcup r₂` agrees with `r₁` on `r₁.target`. have hassign : (r₁.sqcup r₂ h).assign v hv = r₁.assign v hv₁ := by exact Regime.sqcup_assign_pos r₁ r₂ h v hv₁ rw [hassign] exact h₁ v hv₁ · -- Must be in `r₂.target`. have hv₂ : v ∈ r₂.target := by rcases Finset.mem_union.mp hv' with h₁ | h₂ · exact (hv₁ h₁).elim · exact h₂ have hassign : (r₁.sqcup r₂ h).assign v hv = r₂.assign v hv₂ := by exact Regime.sqcup_assign_neg r₁ r₂ h v hv₁ hv₂ rw [hassign] exact h₂ v hv₂

Causalean.PO.POSystem.factualAgrees_sqcup · Causalean/PO/Assumptions/ConsistencyLemmas.lean:54
factualAgrees_single theorem — Combinator: from a factual equality a.factual ω = x, build FactualAgrees for the singleton regime {a.v ← a.equiv.symm x}.

hypotheses

P :

POSystem
shared

α :

Type u_1
shared

a :

POVar P α

x :

α

ω :

P.Ω

h :

a.factual ω = x

conclusion

P.FactualAgrees (Regime.single a.v (a.equiv.symm x)) ω

Proof (Lean source)

theorem factualAgrees_single (a : POVar P α) (x : α) {ω : P.Ω} (h : a.factual ω = x) : P.FactualAgrees (Regime.single a.v (a.equiv.symm x)) ω := by intro v hv -- `v ∈ {a.v}`, so `v = a.v`. have hv_eq : v = a.v := Finset.mem_singleton.mp hv subst hv_eq -- `h : a.equiv (P.eval ∅ ω a.v) = x`; apply `a.equiv.symm`. have hω : a.equiv (P.eval Regime.empty ω a.v) = x := h have := congrArg a.equiv.symm hω simpa [Regime.single] using this

Causalean.PO.POVar.factualAgrees_single · Causalean/PO/Assumptions/ConsistencyLemmas.lean:86
cf_eq_factual_on_event theorem — Under consistency, changing a distinct variable to a value it already has does not change the counterfactual value of the target variable on that event.

hypotheses

P :

POSystem

α β :

Type*
MeasurableSpace α
MeasurableSpace β

hC :

P.Consistency

a :

POVar P α

w :

POVar P β

y :

β

hvw :

a.v ≠ w.v

ω :

P.Ω

hω :

ω ∈ w.event y

conclusion

a.cfUnder w y ω = a.factual ω

Proof (Lean source)

theorem POVar.cf_eq_factual_on_event {P : POSystem} {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] (hC : P.Consistency) (a : POVar P α) (w : POVar P β) (y : β) (hvw : a.v ≠ w.v) {ω : P.Ω} (hω : ω ∈ w.event y) : a.cfUnder w y ω = a.factual ω := by -- The regime: `{w.v ← w.equiv.symm y}`. set r : Regime P.V P.X := Regime.single w.v (w.equiv.symm y) with hr -- Factual agreement: `P.eval ∅ ω v = r.assign v hv` for all `v ∈ r.target`. have hAgrees : P.FactualAgrees r ω := by intro v hv have hvw_eq : v = w.v := Finset.mem_singleton.mp hv subst hvw_eq -- `hω : ω ∈ w.event y`, i.e. `w.factual ω = y`, i.e. -- `w.equiv (P.eval ∅ ω w.v) = y`. have hωeq : w.equiv (P.eval Regime.empty ω w.v) = y := hω -- Apply `w.equiv.symm` and use `symm_apply_apply`. have hsym := congrArg w.equiv.symm hωeq rw [MeasurableEquiv.symm_apply_apply] at hsym show P.eval Regime.empty ω w.v = w.equiv.symm y exact hsym -- Disjointness: `{a.v}` is disjoint from `r.target = {w.v}`. have hdisj : _root_.Disjoint ({a.v} : Finset P.V) r.target := by simp [hr, Regime.single, hvw] -- Apply `hC.factual`. have hPoEq := hC.factual r {a.v} hdisj ω hAgrees have haEq : P.eval r ω a.v = P.eval Regime.empty ω a.v := by simpa [POSystem.poVariable] using congrFun hPoEq ⟨a.v, mem_singleton_self a.v⟩ -- Push through `a.equiv`. change a.equiv (P.eval r ω a.v) = a.equiv (P.eval Regime.empty ω a.v) exact congrArg a.equiv haEq

Causalean.PO.POVar.cf_eq_factual_on_event · Causalean/PO/Assumptions/ConsistencyLemmas.lean:102
factual_eq_cfUnder_self_selected theorem — Under consistency, setting a distinct variable to its realized factual value leaves the target variable at its factual value.

hypotheses

P :

POSystem

α β :

Type*
MeasurableSpace α
MeasurableSpace β

hC :

P.Consistency

a :

POVar P α

w :

POVar P β

hvw :

a.v ≠ w.v

ω :

P.Ω

conclusion

a.factual ω = a.cfUnder w (w.factual ω) ω

Proof (Lean source)

theorem POVar.factual_eq_cfUnder_self_selected {P : POSystem} {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] (hC : P.Consistency) (a : POVar P α) (w : POVar P β) (hvw : a.v ≠ w.v) (ω : P.Ω) : a.factual ω = a.cfUnder w (w.factual ω) ω := by -- The regime: `{w.v ← w.equiv.symm (w.factual ω)}`. set r : Regime P.V P.X := Regime.single w.v (w.equiv.symm (w.factual ω)) with hr -- Factual agreement is definitional: `w.equiv.symm (w.equiv x) = x`. have hAgrees : P.FactualAgrees r ω := by intro v hv have hvw_eq : v = w.v := Finset.mem_singleton.mp hv subst hvw_eq simp [hr, POVar.factual, POVar.cf, Regime.single] -- Disjointness. have hdisj : _root_.Disjoint ({a.v} : Finset P.V) r.target := by simp [hr, Regime.single, hvw] -- Apply `hC.factual`. have hPoEq := hC.factual r {a.v} hdisj ω hAgrees have haEq : P.eval r ω a.v = P.eval Regime.empty ω a.v := by simpa [POSystem.poVariable] using congrFun hPoEq ⟨a.v, mem_singleton_self a.v⟩ change a.equiv (P.eval Regime.empty ω a.v) = a.equiv (P.eval r ω a.v) exact (congrArg a.equiv haEq).symm

Causalean.PO.POVar.factual_eq_cfUnder_self_selected · Causalean/PO/Assumptions/ConsistencyLemmas.lean:138
factual_mul_indicator_eq_cfUnder_mul_indicator theorem — Integrated form of consistency: Y · 1_{W=y} = Y(w=y) · 1_{W=y} pointwise, where a plays the role of Y and w the role of the treatment. Used in backdoor-style identification proofs where the factual outcome is replaced by the counterfactual on the event {W = y}.

hypotheses

P :

POSystem

β :

Type*
MeasurableSpace β

hC :

P.Consistency

a :

POVar P ℝ

w :

POVar P β

y :

β

hvw :

a.v ≠ w.v

conclusion

(fun ω => a.factual ω * (w.event y).indicator (fun _ => (1:ℝ)) ω)
= fun ω => a.cfUnder w y ω * (w.event y).indicator (fun _ => (1:ℝ)) ω

Proof (Lean source)

theorem POVar.factual_mul_indicator_eq_cfUnder_mul_indicator {P : POSystem} {β : Type*} [MeasurableSpace β] (hC : P.Consistency) (a : POVar P ℝ) (w : POVar P β) (y : β) (hvw : a.v ≠ w.v) : (fun ω => a.factual ω * (w.event y).indicator (fun _ => (1:ℝ)) ω) = fun ω => a.cfUnder w y ω * (w.event y).indicator (fun _ => (1:ℝ)) ω := by funext ω by_cases hω : ω ∈ w.event y · have hind : (w.event y).indicator (fun _ => (1:ℝ)) ω = 1 := Set.indicator_of_mem hω _ have hcf : a.cfUnder w y ω = a.factual ω := POVar.cf_eq_factual_on_event hC a w y hvw hω simp [hind, hcf] · have hind : (w.event y).indicator (fun _ => (1:ℝ)) ω = 0 := Set.indicator_of_notMem hω _ simp [hind]

Causalean.PO.POVar.factual_mul_indicator_eq_cfUnder_mul_indicator · Causalean/PO/Assumptions/ConsistencyLemmas.lean:166
factual_mul_indicator_eq_cfUnder_mul_indicator_fn theorem — Pointwise-function variant of POVar.factual_mul_indicator_eq_cfUnder_mul_indicator, phrased directly in terms of POVar.indicator (rather than Set.indicator on w.event y).

hypotheses

P :

POSystem

β :

Type*
MeasurableSpace β
MeasurableSingletonClass β

hC :

P.Consistency

y :

POVar P ℝ

w :

POVar P β

x :

β

h_ne :

y.v ≠ w.v

conclusion

(fun ω => y.factual ω * w.indicator x ω) = fun ω => y.cfUnder w x ω * w.indicator x ω

Proof (Lean source)

theorem POVar.factual_mul_indicator_eq_cfUnder_mul_indicator_fn {P : POSystem} {β : Type*} [MeasurableSpace β] [MeasurableSingletonClass β] (hC : P.Consistency) (y : POVar P ℝ) (w : POVar P β) (x : β) (h_ne : y.v ≠ w.v) : (fun ω => y.factual ω * w.indicator x ω) = fun ω => y.cfUnder w x ω * w.indicator x ω := by rw [w.indicator_eq_event_indicator x] exact POVar.factual_mul_indicator_eq_cfUnder_mul_indicator hC y w x h_ne

Causalean.PO.POVar.factual_mul_indicator_eq_cfUnder_mul_indicator_fn · Causalean/PO/Assumptions/ConsistencyLemmas.lean:188
factual_mul_indicator_eq_cf_mul_indicator theorem — Multi-target integrated consistency: Y · 1_E = Y(r) · 1_E pointwise, whenever every ω ∈ E factually agrees with r and a.v ∉ r.target.

hypotheses

P :

POSystem

hC :

P.Consistency

a :

POVar P ℝ

r :

Regime P.V P.X

h_notmem :

a.v ∉ r.target

E :

Set P.Ω

hE :

∀ ω ∈ E, P.FactualAgrees r ω

conclusion

(fun ω => a.factual ω * E.indicator (fun _ => (1:ℝ)) ω)
= (fun ω => a.cf r ω * E.indicator (fun _ => (1:ℝ)) ω)

Proof (Lean source)

theorem POVar.factual_mul_indicator_eq_cf_mul_indicator {P : POSystem} (hC : P.Consistency) (a : POVar P ℝ) (r : Regime P.V P.X) (h_notmem : a.v ∉ r.target) (E : Set P.Ω) (hE : ∀ ω ∈ E, P.FactualAgrees r ω) : (fun ω => a.factual ω * E.indicator (fun _ => (1:ℝ)) ω) = (fun ω => a.cf r ω * E.indicator (fun _ => (1:ℝ)) ω) := by funext ω by_cases hω : ω ∈ E · have hind : E.indicator (fun _ => (1:ℝ)) ω = 1 := Set.indicator_of_mem hω _ have hcf : a.cf r ω = a.factual ω := POVar.cf_eq_factual_of_factualAgrees hC a r h_notmem ω (hE ω hω) simp [hind, hcf] · have hind : E.indicator (fun _ => (1:ℝ)) ω = 0 := Set.indicator_of_notMem hω _ simp [hind]

Causalean.PO.POVar.factual_mul_indicator_eq_cf_mul_indicator · Causalean/PO/Assumptions/ConsistencyLemmas.lean:228

IndepCF 7 core · 9 supporting This file packages finite heterogeneous collections of regimed potential-outcome variables and defines independence or conditional independence between a single regimed variable and such a bundle. ★ POCFBundle★ CondIndepCF★ project

Independence of Counterfactual Bundles

This file packages finite heterogeneous collections of regimed potential-outcome variables and defines independence or conditional independence between a single regimed variable and such a bundle. These forms provide reusable assumptions for identification theorems.

The main structure is POCFBundle, whose jointValue map turns a finite dependent tuple of regimed potential outcomes into one measurable conditioning object. POSystem.IndepCF and POSystem.CondIndepCF unfold to IndepFun and CondIndepFun, and the projection lemmas let downstream files extract independence for a measurable function or a single coordinate of the bundle.

structure POCFBundle reviewed

Causalean.PO

A finite heterogeneous bundle of n regimed potential-outcome variables indexed by Fin n: each coordinate carries its own value type equipped with a measurable-space structure, and each coordinate is itself a potential-outcome variable paired with the intervention regime under which it is evaluated.

Definition (Lean source)

parameters

P :

fields

Length of the bundle.

n :

ℕ

Value type of each component.

type :

Fin n → Type*

Measurable-space structure on each component.

inst :

∀ i, MeasurableSpace (type i)

Component `RegimedVar`s.

vars :

∀ i, RegimedVar P (type i)

Causalean.PO.POCFBundle · Causalean/PO/Assumptions/IndepCF.lean:42 · uses POSystem

def jointValue reviewed

Causalean.PO.POCFBundle

For a finite bundle of regimed potential-outcome variables, the joint counterfactual-value map assigns to every sample point the tuple whose coordinate is that variable's potential outcome under its associated regime.

Definition (Lean source)

parameters

P :

shared

B :

shared

i :

Fin B.n

shared

def

jointValue B i :

P.Ω → (∀ i : Fin B.n, B.type i)

given by

fun ω i => (B.vars i).value ω

Causalean.PO.POCFBundle.jointValue · Causalean/PO/Assumptions/IndepCF.lean:72 · uses POCFBundle , POSystem

def nil reviewed

Causalean.PO.POCFBundle

For a potential-outcome system, the empty counterfactual bundle has no coordinates.

Definition (Lean source)

parameters

P :

def

nil P :

given by

clause 1

n := 0

clause 2

type := elim0

clause 3

inst := fun i => i.elim0

clause 4

vars := fun i => i.elim0

Causalean.PO.POCFBundle.nil · Causalean/PO/Assumptions/IndepCF.lean:83 · uses POCFBundle , POSystem

def cons reviewed

Causalean.PO.POCFBundle

For a regimed potential-outcome variable and a finite counterfactual bundle in the same potential-outcome system, the extended counterfactual bundle places that variable first and retains every original coordinate.

Definition (Lean source)

parameters

P :

α :

Type*

a :

RegimedVar P α

B :

def

cons a B :

given by

clause 1

n := B.n + 1

clause 2

type := Fin.cases α B.type

clause 3

inst := Fin.cases inst B.inst

clause 4

vars := Fin.cases a B.vars

Causalean.PO.POCFBundle.cons · Causalean/PO/Assumptions/IndepCF.lean:91 · uses POCFBundle , POSystem , RegimedVar

def IndepCF reviewed

Causalean.PO.POSystem

For a potential-outcome system, a regimed potential-outcome variable, a finite counterfactual bundle, and a measure on the sample space, the counterfactual-independence condition says that the variable's potential outcome is independent of the bundle's joint potential-outcome vector under that measure.

Definition (Lean source)

parameters

α :

Type*

P :

a :

RegimedVar P α

B :

μ :

Measure P.Ω := P.μ

def

IndepCF P a B μ :

Prop

given by

IndepFun a.value B.jointValue μ

Causalean.PO.POSystem.IndepCF · Causalean/PO/Assumptions/IndepCF.lean:103 · uses POCFBundle , POSystem , RegimedVar

def CondIndepCF reviewed

Causalean.PO.POSystem

For a potential-outcome system whose sample space is standard Borel, a regimed potential-outcome variable, a finite counterfactual bundle, a regimed conditioning variable, and a finite measure on the sample space, the conditional counterfactual-independence condition says that the first variable's potential outcome is conditionally independent of the bundle's joint potential-outcome vector given the σ-algebra generated by the conditioning variable.

Definition (Lean source)

parameters

α γ :

Type*

MeasurableSpace γ

P :

StandardBorelSpace P.Ω

a :

RegimedVar P α

B :

c :

RegimedVar P γ

μ :

Measure P.Ω := P.μ

IsFiniteMeasure μ

def

CondIndepCF P a B c μ :

Prop

given by

CondIndepFun (comap c.value inferInstance) (c.measurable_value.comap_le) a.value B.jointValue μ

Causalean.PO.POSystem.CondIndepCF · Causalean/PO/Assumptions/IndepCF.lean:111 · uses POCFBundle , POSystem , RegimedVar

lemma project reviewed

Causalean.PO.POSystem.CondIndepCF

Fix a potential-outcome system in which a regimed variable a is conditionally independent of a counterfactual bundle B given a regimed variable c. Then for any measurable function ψ of the bundle's joint value, the value of a remains conditionally independent, given c, of ψ composed with the bundle's joint value.

Formal statement

hypotheses

P :

shared

α β γ :

Type*

MeasurableSpace β

MeasurableSpace γ

StandardBorelSpace P.Ω

a :

RegimedVar P α

B :