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:25 · 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:36 · uses POSystem , Regime

structure Consistency reviewed

Causalean.PO.POSystem

A potential-outcome system is consistent when two conditions hold. First, for every intervention regime and every finite set of variables disjoint from the regime's target, a unit's potential outcomes for that set under the regime equal its factual potential outcomes whenever it factually agrees with the regime. Second, for every pair of disjoint regimes and every finite set of variables disjoint from the union of their targets, a unit's potential outcomes for that set under the composed regime equal its potential outcomes under the first regime alone, whenever it agrees with the second regime after the first has been applied.

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.

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.Consistency · Causalean/PO/Assumptions/Consistency.lean:47 · uses POSystem

ArmSupportTransfer 2 core · 0 supporting Within a positive-mass cell, conditioning is done by normalizing the restricted measure (see Causalean.Mathlib.Probability.normalizedRestrict). ★ ae_abs_potential_le_of_indep_positive_arm

Transferring an outcome bound from an observed arm to a potential outcome

Within a positive-mass cell, conditioning is done by normalizing the restricted measure (see Causalean.Mathlib.Probability.normalizedRestrict). This module provides the real-valued indicator of a treatment arm and the support-transfer step used in potential-outcome arguments: if a potential outcome is independent of the arm indicator under the cell law (ignorability), agrees with the observed outcome on that arm (consistency), and the arm has positive probability (positivity), then an almost-sure absolute bound on the observed outcome in the arm carries over to the potential outcome throughout the cell.

def armIndicator reviewed

Causalean.PO

Given a sample space and an event in it, the real-valued arm indicator equals one for sample points in the event and zero for all other sample points.

Definition (Lean source)

parameters

Ω :

Type*

A :

Set Ω

def

armIndicator A :

Ω → ℝ

given by

A.indicator (fun _ => 1)

Causalean.PO.armIndicator · Causalean/PO/Assumptions/ArmSupportTransfer.lean:25

theorem ae_abs_potential_le_of_indep_positive_arm reviewed

Causalean.PO

Within a measurable positive-mass cell, for a measurable arm event, if the potential outcome is measurable, the arm has positive normalized cell probability, the potential outcome is independent of the arm indicator under the normalized cell law, the observed and potential outcomes agree almost surely on that arm, and the observed outcome obeys an absolute bound there, then the potential outcome obeys the same absolute bound almost surely throughout the cell.

Formal statement

hypotheses

Ω :

Type*

MeasurableSpace Ω

Measure Ω

IsProbabilityMeasure P

C A :

Set Ω

hC :

MeasurableSet C

hCpos :

0 < P C

hA :

MeasurableSet A

Ypot Yobs :

Ω → ℝ

hYpot :

Measurable Ypot

hArmPos :

0 < normalizedRestrict P C A

hInd :

IndepFun Ypot (armIndicator A) (normalizedRestrict P C)

hConsistency :

Yobs =ᵐ[(normalizedRestrict P C).restrict A] Ypot

R :

ℝ

hObservedBound :

∀ᵐ ω ∂(normalizedRestrict P C).restrict A, |Yobs ω| ≤ R

conclusion

∀ᵐ ω ∂P.restrict C, |Ypot ω| ≤ R

Proof (Lean source)

theorem ae_abs_potential_le_of_indep_positive_arm {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P] {C A : Set Ω} (hC : MeasurableSet C) (hCpos : 0 < P C) (hA : MeasurableSet A) {Ypot Yobs : Ω → ℝ} (hYpot : Measurable Ypot) (hArmPos : 0 < normalizedRestrict P C A) (hInd : IndepFun Ypot (armIndicator A) (normalizedRestrict P C)) (hConsistency : Yobs =ᵐ[(normalizedRestrict P C).restrict A] Ypot) {R : ℝ} (hObservedBound : ∀ᵐ ω ∂(normalizedRestrict P C).restrict A, |Yobs ω| ≤ R) : ∀ᵐ ω ∂P.restrict C, |Ypot ω| ≤ R := by let B : Set Ω := {ω | R < |Ypot ω|} have hBadRange : MeasurableSet {y : ℝ | R < |y|} := by rw [show {y : ℝ | R < |y|} = {y : ℝ | R < ‖y‖} by ext y simp only [Real.norm_eq_abs]] exact measurableSet_lt measurable_const (by fun_prop) have hB : MeasurableSet B := hYpot hBadRange have hPotBoundArm : ∀ᵐ ω ∂(normalizedRestrict P C).restrict A, |Ypot ω| ≤ R := by filter_upwards [hConsistency, hObservedBound] with ω hEq hBound rw [← hEq] exact hBound have hBAzero : normalizedRestrict P C (B ∩ A) = 0 := by rw [measure_eq_zero_iff_ae_notMem] filter_upwards [ae_imp_of_ae_restrict hPotBoundArm] with ω hω intro hmem exact (not_lt_of_ge (hω hmem.2)) hmem.1 have hArmPreimage : armIndicator A ⁻¹' ({1} : Set ℝ) = A := by ext ω simp [armIndicator] have hFactor : normalizedRestrict P C (B ∩ A) = normalizedRestrict P C B * normalizedRestrict P C A := by simpa [B, hArmPreimage] using hInd.measure_inter_preimage_eq_mul {y : ℝ | R < |y|} ({1} : Set ℝ) hBadRange (measurableSet_singleton (1 : ℝ)) have hBzero : normalizedRestrict P C B = 0 := by have hprod : normalizedRestrict P C B * normalizedRestrict P C A = 0 := by rw [← hFactor, hBAzero] exact (mul_eq_zero.mp hprod).resolve_right hArmPos.ne' apply (ae_normalizedRestrict_iff hCpos).mp filter_upwards [(measure_eq_zero_iff_ae_notMem.mp hBzero)] with ω hω exact le_of_not_gt (by simpa [B] using hω)

Causalean.PO.ae_abs_potential_le_of_indep_positive_arm · Causalean/PO/Assumptions/ArmSupportTransfer.lean:34 · uses normalizedRestrict , armIndicator

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:201 · 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:46
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:51
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:83
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:99
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:135
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:163
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:185
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:225

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★ IndepCF★ 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:39 · 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:69 · 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:80 · 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:88 · 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:100 · 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:108 · 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 :