PO.Core

The graph-free potential-outcome core: systems, variables, finite intervention regimes, and joint counterfactual distributions.

Regime 10 core · 16 supporting This file defines finite intervention regimes for the potential-outcome framework. ★ Regime★ ofList_target

Intervention Regimes

This file defines finite intervention regimes for the potential-outcome framework. A regime records the variables fixed by an intervention and the assigned value for each fixed variable, without assuming a graph or structural causal model.

structure Regime reviewed

Causalean.PO

An intervention regime specifies a finite set of targeted variables together with an assigned value in the corresponding value space for each targeted variable.

Definition (Lean source)

parameters

V :

Type*

DecidableEq V

X :

V → Type*

fields

target :

Finset V

assign :

∀ v : V

v ∈ target

then

X v

Causalean.PO.Regime · Causalean/PO/Core/Regime.lean:28

def empty reviewed

Causalean.PO.Regime

The empty intervention regime fixes no variables and therefore has no assignments.

Definition (Lean source)

def empty : Regime V X where target := ∅ assign := fun v hv => (notMem_empty v hv).elim

Causalean.PO.Regime.empty · Causalean/PO/Core/Regime.lean:40 · uses Regime

def Disjoint reviewed

Causalean.PO.Regime

Two intervention regimes are disjoint exactly when their target sets have no variable in common.

Definition (Lean source)

def Disjoint (r₁ r₂ : Regime V X) : Prop := _root_.Disjoint r₁.target r₂.target

Causalean.PO.Regime.Disjoint · Causalean/PO/Core/Regime.lean:49 · uses Regime

def leftBiasedUnion reviewed

Causalean.PO.Regime

The left-biased union of two regimes targets their union and uses the first regime's assignment wherever both regimes target the same variable.

Definition (Lean source)

noncomputable def leftBiasedUnion (r₁ r₂ : Regime V X) : Regime V X where target := r₁.target ∪ r₂.target assign := fun v hv => if h1 : v ∈ r₁.target then r₁.assign v h1 else r₂.assign v (by rcases Finset.mem_union.mp hv with h₁ | h₂ · exact (h1 h₁).elim · exact h₂)

Causalean.PO.Regime.leftBiasedUnion · Causalean/PO/Core/Regime.lean:53 · uses Regime

def sqcup reviewed

Causalean.PO.Regime

The disjoint union of two compatible intervention regimes targets the union of their target sets and uses the assignment from the unique component regime that targets each variable.

Definition (Lean source)

noncomputable def sqcup (r₁ r₂ : Regime V X) (_h : r₁.Disjoint r₂) : Regime V X := leftBiasedUnion r₁ r₂

Causalean.PO.Regime.sqcup · Causalean/PO/Core/Regime.lean:65 · uses Regime , Disjoint

def single reviewed

Causalean.PO.Regime

A singleton intervention regime fixes exactly one variable to the supplied value.

Definition (Lean source)

def single (v : V) (x : X v) : Regime V X where target := {v} assign := fun _ hw => (Finset.mem_singleton.mp hw).symm ▸ x

Causalean.PO.Regime.single · Causalean/PO/Core/Regime.lean:117 · uses Regime

def listLookup reviewed

Causalean.PO.Regime

Lookup in a list of variable-value assignments returns the listed value for a variable that appears among the listed labels.

Definition (Lean source)

def listLookup : (l : List ((v : V) × X v)) → (v : V) → v ∈ l.map fst → X v | [], v, hv => by simp at hv | ⟨w, x⟩ :: rest, v, hv => if h : v = w then h ▸ x else listLookup rest v (by rcases (List.mem_cons.mp hv) with hv | hv · exact (h hv).elim · exact hv)

Causalean.PO.Regime.listLookup · Causalean/PO/Core/Regime.lean:150

def ofListLeftBiased reviewed

Causalean.PO.Regime

A list of variable-value assignments determines a regime by using the first listed assignment for each targeted variable.

Definition (Lean source)

def ofListLeftBiased (l : List ((v : V) × X v)) : Regime V X where target := (l.map fst).toFinset assign := fun v hv => listLookup l v (List.mem_toFinset.mp hv)

Causalean.PO.Regime.ofListLeftBiased · Causalean/PO/Core/Regime.lean:167 · uses Regime

def ofList reviewed

Causalean.PO.Regime

A duplicate-free list of variable-value assignments determines the intervention regime that targets exactly the listed variables and assigns each target its listed value.

Definition (Lean source)

def ofList (l : List ((v : V) × X v)) (_h : (l.map fst).Nodup) : Regime V X := ofListLeftBiased l

Causalean.PO.Regime.ofList · Causalean/PO/Core/Regime.lean:174 · uses Regime

theorem ofList_target reviewed

Causalean.PO.Regime

For a duplicate-free list of variable-value assignments l, the target of the regime it determines is exactly the finite set of variables listed in l.

Formal statement

hypotheses

l :

List ((v : V) × X v)

h :

(l.map fst).Nodup

conclusion

(ofList l h).target = (l.map fst).toFinset

Proof (Lean source)

@[simp] theorem ofList_target (l : List ((v : V) × X v)) (h : (l.map fst).Nodup) : (ofList l h).target = (l.map fst).toFinset := rfl

Causalean.PO.Regime.ofList_target · Causalean/PO/Core/Regime.lean:181 · uses ofList

16 supporting declarations (lemmas, instances)

empty_target lemma — The empty intervention regime has no target variables.

conclusion

(empty : Regime V X).target = ∅

Proof (Lean source)

@[simp] lemma empty_target : (empty : Regime V X).target = ∅ := rfl

Causalean.PO.Regime.empty_target · Causalean/PO/Core/Regime.lean:75
empty_disjoint_right lemma — The empty intervention regime is disjoint from every regime on its right.

hypotheses

r :

Regime V X

conclusion

(empty : Regime V X).Disjoint r

Proof (Lean source)

lemma empty_disjoint_right (r : Regime V X) : (empty : Regime V X).Disjoint r := by simp [Disjoint, empty]

Causalean.PO.Regime.empty_disjoint_right · Causalean/PO/Core/Regime.lean:78
empty_disjoint_left lemma — Every regime is disjoint from the empty intervention regime on its right.

hypotheses

r :

Regime V X

conclusion

r.Disjoint (empty : Regime V X)

Proof (Lean source)

lemma empty_disjoint_left (r : Regime V X) : r.Disjoint (empty : Regime V X) := by simp [Disjoint, empty]

Causalean.PO.Regime.empty_disjoint_left · Causalean/PO/Core/Regime.lean:82
sqcup_target lemma — The target of the disjoint union of two regimes is the union of their target sets.

hypotheses

r₁ r₂ :

Regime V X

h :

r₁.Disjoint r₂

conclusion

(r₁.sqcup r₂ h).target = r₁.target ∪ r₂.target

Proof (Lean source)

@[simp] lemma sqcup_target (r₁ r₂ : Regime V X) (h : r₁.Disjoint r₂) : (r₁.sqcup r₂ h).target = r₁.target ∪ r₂.target := rfl

Causalean.PO.Regime.sqcup_target · Causalean/PO/Core/Regime.lean:86
sqcup_assign_pos lemma — sqcup agrees with r₁ whenever v ∈ r₁.target.

hypotheses

r₁ r₂ :

Regime V X

h :

r₁.Disjoint r₂

v :

V

h1 :

v ∈ r₁.target

conclusion

(r₁.sqcup r₂ h).assign v (by simp [Regime.sqcup, Regime.leftBiasedUnion, h1])
= r₁.assign v h1

Proof (Lean source)

lemma sqcup_assign_pos (r₁ r₂ : Regime V X) (h : r₁.Disjoint r₂) (v : V) (h1 : v ∈ r₁.target) : (r₁.sqcup r₂ h).assign v (by simp [Regime.sqcup, Regime.leftBiasedUnion, h1]) = r₁.assign v h1 := by simp [Regime.sqcup, Regime.leftBiasedUnion, h1]

Causalean.PO.Regime.sqcup_assign_pos · Causalean/PO/Core/Regime.lean:90
sqcup_assign_neg lemma — sqcup agrees with r₂ whenever v ∉ r₁.target (and hence v ∈ r₂.target).

hypotheses

r₁ r₂ :

Regime V X

h :

r₁.Disjoint r₂

v :

V

h1 :

v ∉ r₁.target

h2 :

v ∈ r₂.target

conclusion

(r₁.sqcup r₂ h).assign v (by simp [Regime.sqcup, Regime.leftBiasedUnion, h2])
= r₂.assign v h2

Proof (Lean source)

lemma sqcup_assign_neg (r₁ r₂ : Regime V X) (h : r₁.Disjoint r₂) (v : V) (h1 : v ∉ r₁.target) (h2 : v ∈ r₂.target) : (r₁.sqcup r₂ h).assign v (by simp [Regime.sqcup, Regime.leftBiasedUnion, h2]) = r₂.assign v h2 := by simp [Regime.sqcup, Regime.leftBiasedUnion, h1]

Causalean.PO.Regime.sqcup_assign_neg · Causalean/PO/Core/Regime.lean:97
ext theorem — Extensionality for Regime: equal targets and pointwise-equal assignments.

hypotheses

r₁ r₂ :

Regime V X

htgt :

r₁.target = r₂.target

hassign :

∀ v (h₁ : v ∈ r₁.target) (h₂ : v ∈ r₂.target), r₁.assign v h₁ = r₂.assign v h₂

conclusion

r₁ = r₂

Proof (Lean source)

theorem ext {r₁ r₂ : Regime V X} (htgt : r₁.target = r₂.target) (hassign : ∀ v (h₁ : v ∈ r₁.target) (h₂ : v ∈ r₂.target), r₁.assign v h₁ = r₂.assign v h₂) : r₁ = r₂ := by obtain ⟨t₁, a₁⟩ := r₁ obtain ⟨t₂, a₂⟩ := r₂ subst htgt congr 1 funext v hv exact hassign v hv hv

Causalean.PO.Regime.ext · Causalean/PO/Core/Regime.lean:104
single_target theorem — The singleton intervention regime targets exactly the one variable it fixes.

hypotheses

v :

V

x :

X v

conclusion

(single v x : Regime V X).target = {v}

Proof (Lean source)

@[simp] theorem single_target (v : V) (x : X v) : (single v x : Regime V X).target = {v} := rfl

Causalean.PO.Regime.single_target · Causalean/PO/Core/Regime.lean:123
single_assign_self theorem — Evaluating the singleton intervention assignment at its target returns the supplied value.

hypotheses

v :

V

x :

X v

conclusion

(single v x : Regime V X).assign v (mem_singleton_self _) = x

Proof (Lean source)

theorem single_assign_self (v : V) (x : X v) : (single v x : Regime V X).assign v (mem_singleton_self _) = x := rfl

Causalean.PO.Regime.single_assign_self · Causalean/PO/Core/Regime.lean:127
single_disjoint_single theorem — Singleton intervention regimes on two distinct variables are disjoint.

hypotheses

v w :

V

hvw :

v ≠ w

x :

X v

y :

X w

conclusion

(single v x : Regime V X).Disjoint (single w y)

Proof (Lean source)

theorem single_disjoint_single {v w : V} (hvw : v ≠ w) (x : X v) (y : X w) : (single v x : Regime V X).Disjoint (single w y) := by simp [Disjoint, single, hvw]

Causalean.PO.Regime.single_disjoint_single · Causalean/PO/Core/Regime.lean:131
single_disjoint_of_not_mem theorem — A singleton intervention regime is disjoint from any regime that does not target its variable.

hypotheses

v :

V

x :

X v

r :

Regime V X

h :

v ∉ r.target

conclusion

(single v x : Regime V X).Disjoint r

Proof (Lean source)

theorem single_disjoint_of_not_mem {v : V} (x : X v) (r : Regime V X) (h : v ∉ r.target) : (single v x : Regime V X).Disjoint r := by simp [Disjoint, single, Finset.disjoint_singleton_left, h]

Causalean.PO.Regime.single_disjoint_of_not_mem · Causalean/PO/Core/Regime.lean:136
disjoint_single_of_not_mem theorem — Any regime that does not target a variable is disjoint from the singleton intervention on that variable.

hypotheses

v :

V

x :

X v

r :

Regime V X

h :

v ∉ r.target

conclusion

r.Disjoint (single v x : Regime V X)

Proof (Lean source)

theorem disjoint_single_of_not_mem {v : V} (x : X v) (r : Regime V X) (h : v ∉ r.target) : r.Disjoint (single v x : Regime V X) := by simp [Disjoint, single, Finset.disjoint_singleton_right, h]

Causalean.PO.Regime.disjoint_single_of_not_mem · Causalean/PO/Core/Regime.lean:142
ofList_nil theorem — Building a regime from the empty list gives the empty intervention regime.

conclusion

(ofList [] (by simp) : Regime V X) = empty

Proof (Lean source)

@[simp] theorem ofList_nil : (ofList [] (by simp) : Regime V X) = empty := by congr 1

Causalean.PO.Regime.ofList_nil · Causalean/PO/Core/Regime.lean:188
ofList_cons_target theorem — The target of a regime built from a nonempty list inserts the head variable into the target from the tail.

hypotheses

v :

V
X v
List ((v : V) × X v)

h :

((⟨v, x⟩ :: rest : List ((v : V) × X v)).map fst).Nodup

conclusion

(ofList (⟨v, x⟩ :: rest) h).target = insert v (rest.map fst).toFinset

Proof (Lean source)

@[simp] theorem ofList_cons_target {v : V} {x : X v} {rest : List ((v : V) × X v)} (h : ((⟨v, x⟩ :: rest : List ((v : V) × X v)).map fst).Nodup) : (ofList (⟨v, x⟩ :: rest) h).target = insert v (rest.map fst).toFinset := by simp [ofList, ofListLeftBiased]

Causalean.PO.Regime.ofList_cons_target · Causalean/PO/Core/Regime.lean:193
listLookup_cons_self theorem — Looking up the head variable of a dependent assignment list returns the head value.

hypotheses

v :

V
X v
List ((v : V) × X v)

conclusion

listLookup (⟨v, x⟩ :: rest) v (by simp) = x

Proof (Lean source)

theorem listLookup_cons_self {v : V} {x : X v} {rest : List ((v : V) × X v)} : listLookup (⟨v, x⟩ :: rest) v (by simp) = x := by simp [listLookup]

Causalean.PO.Regime.listLookup_cons_self · Causalean/PO/Core/Regime.lean:202
listLookup_cons_of_ne theorem — Looking up a different variable skips the head of a dependent assignment list and continues in the tail.

hypotheses

v w :

V
X w
List ((v : V) × X v)

hvw :

v ≠ w

hv' :

v ∈ rest.map fst

conclusion

listLookup (⟨w, x⟩ :: rest) v (by simp [hv']) = listLookup rest v hv'

Proof (Lean source)

theorem listLookup_cons_of_ne {v w : V} {x : X w} {rest : List ((v : V) × X v)} (hvw : v ≠ w) (hv' : v ∈ rest.map fst) : listLookup (⟨w, x⟩ :: rest) v (by simp [hv']) = listLookup rest v hv' := by simp [listLookup, hvw]

Causalean.PO.Regime.listLookup_cons_of_ne · Causalean/PO/Core/Regime.lean:208

System 5 core · 2 supporting This file defines a graph-free potential-outcome system, its coordinate-level potential outcomes, subset-valued potential outcomes, and the induced pushforward law of a subset under a regime. ★ POSystem★ measurable_component

Potential Outcome Systems

This file defines a graph-free potential-outcome system, its coordinate-level potential outcomes, subset-valued potential outcomes, and the induced pushforward law of a subset under a regime. These are the base objects used by the counterfactual and identification layers of the library.

structure POSystem reviewed

Causalean.PO

A potential-outcome system consists of a finite set of variables, a measurable value space for each variable, a measurable sample space carrying a probability measure, and, for every intervention regime and sample point, a jointly measurable assignment of potential-outcome values to all variables.

Definition (Lean source)

fields

V :

Type*

DecidableEq V

Fintype V

X :

V → Type*

∀ v, MeasurableSpace (X v)

Ω :

Type*

MeasurableSpace Ω

μ :

Measure Ω

IsProbabilityMeasure μ

Derived world-evaluation map `Eval^P_r` -- def:po-operator.

eval :

Regime V X → Ω → ∀ v, X v

measurable_eval :

∀ r, Measurable (eval r)

Causalean.PO.POSystem · Causalean/PO/Core/System.lean:27

def component reviewed

Causalean.PO.POSystem

A coordinate potential outcome maps each unit to the value a selected variable would take under a selected intervention regime.

Definition (Lean source)

def component (r : Regime P.V P.X) (v : P.V) : P.Ω → P.X v := fun ω => P.eval r ω v

Causalean.PO.POSystem.component · Causalean/PO/Core/System.lean:55 · uses POSystem , Regime

lemma measurable_component reviewed

Causalean.PO.POSystem

For an intervention regime r and a variable v, the coordinate potential outcome of v under r is a measurable function of the unit.

Formal statement

hypotheses

r :

Regime P.V P.X

v :

P.V

conclusion

Measurable (P.component r v)

Proof (Lean source)

lemma measurable_component (r : Regime P.V P.X) (v : P.V) : Measurable (P.component r v) := (measurable_pi_apply v).comp (P.measurable_eval r)

Causalean.PO.POSystem.measurable_component · Causalean/PO/Core/System.lean:62 · uses POSystem , component , Regime

def poVariable reviewed

Causalean.PO.POSystem

A joint potential outcome maps each unit to the vector of values a selected finite set of variables would take under a selected intervention regime.

Definition (Lean source)

def poVariable (r : Regime P.V P.X) (Y : Finset P.V) : P.Ω → ValuesOn Y P.X := fun ω v => P.eval r ω v.val

Causalean.PO.POSystem.poVariable · Causalean/PO/Core/System.lean:69 · uses POSystem , Regime , ValuesOn

def poOperator reviewed

Causalean.PO.POSystem

A potential-outcome law is the distribution of a selected finite set of variables under a selected intervention regime.

Definition (Lean source)

noncomputable def poOperator (r : Regime P.V P.X) (Y : Finset P.V) : Measure (ValuesOn Y P.X) := (P.μ).map (P.poVariable r Y)

Causalean.PO.POSystem.poOperator · Causalean/PO/Core/System.lean:85 · uses POSystem , Regime , ValuesOn

2 supporting declarations (lemmas, instances)

measurable_poVariable lemma — The joint potential outcome for any finite set of variables under any intervention regime is measurable.

hypotheses

r :

Regime P.V P.X

Y :

Finset P.V

conclusion

Measurable (P.poVariable r Y)

Proof (Lean source)

lemma measurable_poVariable (r : Regime P.V P.X) (Y : Finset P.V) : Measurable (P.poVariable r Y) := by refine measurable_pi_lambda _ ?_ intro v exact (measurable_pi_apply v.val).comp (P.measurable_eval r)

Causalean.PO.POSystem.measurable_poVariable · Causalean/PO/Core/System.lean:77
instIsProbabilityMeasureValuesOnVXPoOperator instance — The potential-outcome law of a finite set of variables under a regime is a probability measure.

instance (r : Regime P.V P.X) (Y : Finset P.V) : IsProbabilityMeasure (P.poOperator r Y) := by unfold poOperator exact isProbabilityMeasure_map (P.measurable_poVariable r Y).aemeasurable

Causalean.PO.POSystem.instIsProbabilityMeasureValuesOnVXPoOperator · Causalean/PO/Core/System.lean:93

Counterfactual 3 core · 2 supporting This file constructs finite joint distributions of potential outcomes evaluated under possibly different intervention regimes. ★ counterfactualDist_marginal

Cross-World Counterfactual Distributions

This file constructs finite joint distributions of potential outcomes evaluated under possibly different intervention regimes. It supplies the cross-world evaluation map, its pushforward law, and the basic marginal reading of that law.

def crossWorldEval reviewed

Causalean.PO.POSystem

For a potential-outcome system, a finite list of queries, and a unit in the sample space, this function returns the tuple whose $i$ th component is the potential outcome, for the finite variable set in the $i$ th query, under the intervention regime in the $i$ th query.

Definition (Lean source)

def crossWorldEval (qs : List (Regime P.V P.X × Finset P.V)) : P.Ω → (i : Fin qs.length) → ValuesOn (qs[i].2) P.X := fun ω i => P.poVariable (qs[i].1) (qs[i].2) ω

Causalean.PO.POSystem.crossWorldEval · Causalean/PO/Core/Counterfactual.lean:24 · uses POSystem , Regime , ValuesOn

def counterfactualDist reviewed

Causalean.PO.POSystem

For a potential-outcome system and a finite list of counterfactual queries, the counterfactual distribution is the probability measure obtained by pushing the system's probability measure on the sample space through the cross-world evaluation map for those queries.

Definition (Lean source)

noncomputable def counterfactualDist (qs : List (Regime P.V P.X × Finset P.V)) : Measure ((i : Fin qs.length) → ValuesOn (qs[i].2) P.X) := P.μ.map (P.crossWorldEval qs)

Causalean.PO.POSystem.counterfactualDist · Causalean/PO/Core/Counterfactual.lean:44 · uses POSystem , Regime , ValuesOn

theorem counterfactualDist_marginal reviewed

Causalean.PO.POSystem

For a finite list of counterfactual queries qs and an index i into that list, the i-th coordinate marginal of the joint counterfactual distribution over all queries equals the potential-outcome law for query i alone.

Formal statement

hypotheses

qs :

List (Regime P.V P.X × Finset P.V)

i :

Fin qs.length

conclusion

(P.counterfactualDist qs).map (fun f => f i) = P.poOperator (qs[i].1) (qs[i].2)

Proof (Lean source)

theorem counterfactualDist_marginal (qs : List (Regime P.V P.X × Finset P.V)) (i : Fin qs.length) : (P.counterfactualDist qs).map (fun f => f i) = P.poOperator (qs[i].1) (qs[i].2) := by unfold counterfactualDist poOperator rw [MeasureTheory.Measure.map_map (measurable_pi_apply i) (P.measurable_crossWorldEval qs)] rfl

Causalean.PO.POSystem.counterfactualDist_marginal · Causalean/PO/Core/Counterfactual.lean:62 · uses POSystem , counterfactualDist , poOperator , Regime , ValuesOn

2 supporting declarations (lemmas, instances)

measurable_crossWorldEval lemma — The cross-world evaluation map for a finite list of counterfactual queries is measurable.

hypotheses

qs :

List (Regime P.V P.X × Finset P.V)

conclusion

Measurable (P.crossWorldEval qs)

Proof (Lean source)

lemma measurable_crossWorldEval (qs : List (Regime P.V P.X × Finset P.V)) : Measurable (P.crossWorldEval qs) := by refine measurable_pi_lambda _ ?_ intro i exact P.measurable_poVariable _ _

Causalean.PO.POSystem.measurable_crossWorldEval · Causalean/PO/Core/Counterfactual.lean:36
instIsProbabilityMeasureForallValuesOnVSndRegimeXFinsetGetElemListProdFinLengthLtNatValCounterfactualDist instance — The finite cross-world counterfactual distribution is a probability measure.

instance (qs : List (Regime P.V P.X × Finset P.V)) : IsProbabilityMeasure (P.counterfactualDist qs) := by unfold counterfactualDist exact isProbabilityMeasure_map (P.measurable_crossWorldEval qs).aemeasurable

Causalean.PO.POSystem.instIsProbabilityMeasureForallValuesOnVSndRegimeXFinsetGetElemListProdFinLengthLtNatValCounterfactualDist · Causalean/PO/Core/Counterfactual.lean:55

Variable 11 core · 12 supporting This file packages a variable of a potential-outcome system together with a common measurable value space, so that factual and counterfactual realizations can be handled uniformly. ★ POVar★ indicator_eq_event_indicator★ RegimedVar

Potential-Outcome Variables

This file packages a variable of a potential-outcome system together with a common measurable value space, so that factual and counterfactual realizations can be handled uniformly. It also provides event indicators and variables paired with intervention regimes for counterfactual independence statements.

The main public objects are POVar, its factual and counterfactual value maps factual, cf, and cfUnder, the factual-event indicator API, and RegimedVar for bundling a variable with the regime under which it is evaluated.

structure POVar reviewed

Causalean.PO

A potential-outcome variable records a system variable together with a measurable relabeling of its native value space into a chosen analysis scale α.

Definition (Lean source)

parameters

P :

POSystem

α :

Type*

MeasurableSpace α

fields

v :

P.V

equiv :

P.X v ≃ᵐ α

Causalean.PO.POVar · Causalean/PO/Core/Variable.lean:28 · uses POSystem

def cf reviewed

Causalean.PO.POVar

A counterfactual value function assigns each unit the value that a selected variable would have under a selected intervention regime, reported on its chosen analysis scale.

Definition (Lean source)

def cf (a : POVar P α) (r : Regime P.V P.X) : P.Ω → α := fun ω => a.equiv (P.eval r ω a.v)

Causalean.PO.POVar.cf · Causalean/PO/Core/Variable.lean:44 · uses POSystem , POVar , Regime

def factual reviewed

Causalean.PO.POVar

A factual value function assigns each unit the observed no-intervention value of a selected variable, reported on its chosen analysis scale.

Definition (Lean source)

def factual (a : POVar P α) : P.Ω → α := a.cf Regime.empty

Causalean.PO.POVar.factual · Causalean/PO/Core/Variable.lean:52 · uses POSystem , POVar

def event reviewed

Causalean.PO.POVar

A factual-value event is the set of units whose observed value of a selected variable equals a selected analysis-scale value.

Definition (Lean source)

def event (a : POVar P α) (x : α) : Set P.Ω := a.factual ⁻¹' {x}

Causalean.PO.POVar.event · Causalean/PO/Core/Variable.lean:68 · uses POSystem , POVar

def cfUnder reviewed

Causalean.PO.POVar

The potential outcome of variable y when the intervention variable w is set to the value d: the single-variable counterfactual y(w := d). (Binders follow the usual econometric convention — y is the outcome variable and d is the treatment/intervention value; w is the variable being intervened on.)

Definition (Lean source)

def cfUnder {β : Type*} [MeasurableSpace β] (y : POVar P α) (w : POVar P β) (d : β) : P.Ω → α := y.cf (Regime.single w.v (w.equiv.symm d))

Causalean.PO.POVar.cfUnder · Causalean/PO/Core/Variable.lean:80 · uses POSystem , POVar

def indicator reviewed

Causalean.PO.POVar

A factual-value indicator is the zero-one function that marks units whose observed value of a selected variable equals a selected analysis-scale value.

Definition (Lean source)

noncomputable def indicator (a : POVar P α) (x : α) : P.Ω → ℝ := (a.event x).indicator (fun _ => (1 : ℝ))

Causalean.PO.POVar.indicator · Causalean/PO/Core/Variable.lean:103 · uses POSystem , POVar

lemma indicator_eq_event_indicator reviewed

Causalean.PO.POVar

For a potential-outcome variable a and a value x in its range, the real-valued factual indicator a.indicator x equals the set-indicator of the factual event {a = x}.

Formal statement

hypotheses

a :

POVar P α

x :

conclusion

a.indicator x = (a.event x).indicator (fun _ => (1 : ℝ))

Proof (Lean source)

lemma indicator_eq_event_indicator (a : POVar P α) (x : α) : a.indicator x = (a.event x).indicator (fun _ => (1 : ℝ)) := rfl

Causalean.PO.POVar.indicator_eq_event_indicator · Causalean/PO/Core/Variable.lean:112 · uses POSystem , POVar , event , indicator

structure RegimedVar reviewed

Causalean.PO

A regimed variable pairs a potential-outcome variable with the intervention regime under which it should be evaluated.

Definition (Lean source)

parameters

P :

POSystem

α :

Type*

MeasurableSpace α

fields

var :

POVar P α

regime :

Regime P.V P.X

Causalean.PO.RegimedVar · Causalean/PO/Core/Variable.lean:191 · uses POSystem

def value reviewed

Causalean.PO.RegimedVar

A regimed variable's value function assigns each unit the counterfactual value implied by the variable-regime pair.

Definition (Lean source)

def value (rv : RegimedVar P α) : P.Ω → α := rv.var.cf rv.regime

Causalean.PO.RegimedVar.value · Causalean/PO/Core/Variable.lean:205 · uses POSystem , RegimedVar

def ofFactual reviewed

Causalean.PO.RegimedVar

Factual bundling views a potential-outcome variable as evaluated under the no-intervention regime.

Definition (Lean source)

def ofFactual (a : POVar P α) : RegimedVar P α := ⟨a, Regime.empty⟩

Causalean.PO.RegimedVar.ofFactual · Causalean/PO/Core/Variable.lean:215 · uses POSystem , POVar , RegimedVar

def ofSingle reviewed

Causalean.PO.RegimedVar

Single-intervention bundling views a potential-outcome variable as evaluated after fixing one system variable to a chosen native value.

Definition (Lean source)

def ofSingle (a : POVar P α) (w : P.V) (x : P.X w) : RegimedVar P α := ⟨a, Regime.single w x⟩

Causalean.PO.RegimedVar.ofSingle · Causalean/PO/Core/Variable.lean:221 · uses POSystem , POVar , RegimedVar

12 supporting declarations (lemmas, instances)

measurable_cf lemma — The counterfactual-value function of a potential-outcome variable under any intervention regime is measurable.

hypotheses

a :

POVar P α

r :

Regime P.V P.X

conclusion

Measurable (a.cf r)

Proof (Lean source)

lemma measurable_cf (a : POVar P α) (r : Regime P.V P.X) : Measurable (a.cf r) := a.equiv.measurable.comp ((measurable_pi_apply _).comp (P.measurable_eval r))

Causalean.PO.POVar.measurable_cf · Causalean/PO/Core/Variable.lean:58
measurable_factual lemma — The factual-value function of a potential-outcome variable is measurable.

hypotheses

a :

POVar P α

conclusion

Measurable a.factual

Proof (Lean source)

lemma measurable_factual (a : POVar P α) : Measurable a.factual := a.measurable_cf _

Causalean.PO.POVar.measurable_factual · Causalean/PO/Core/Variable.lean:64
measurableSet_event lemma — The event that a potential-outcome variable's factual value equals a given singleton-measurable value is measurable.

hypotheses

a :

POVar P α

x :

α

hx :

MeasurableSet ({x} : Set α)

conclusion

MeasurableSet (a.event x)

Proof (Lean source)

lemma measurableSet_event (a : POVar P α) (x : α) (hx : MeasurableSet ({x} : Set α)) : MeasurableSet (a.event x) := a.measurable_factual hx

Causalean.PO.POVar.measurableSet_event · Causalean/PO/Core/Variable.lean:74
measurable_cfUnder lemma — The single-intervention counterfactual-value function is measurable.

hypotheses

β :

Type*
MeasurableSpace β

y :

POVar P α

w :

POVar P β

d :

β

conclusion

Measurable (y.cfUnder w d)

Proof (Lean source)

lemma measurable_cfUnder {β : Type*} [MeasurableSpace β] (y : POVar P α) (w : POVar P β) (d : β) : Measurable (y.cfUnder w d) := y.measurable_cf _

Causalean.PO.POVar.measurable_cfUnder · Causalean/PO/Core/Variable.lean:92
indicator_apply_eq_one lemma — Pointwise: a.indicator x ω = 1 on {a = x}.

hypotheses

a :

POVar P α

x :

α

ω :

P.Ω

hω :

a.factual ω = x

conclusion

a.indicator x ω = 1

Proof (Lean source)

lemma indicator_apply_eq_one (a : POVar P α) {x : α} {ω : P.Ω} (hω : a.factual ω = x) : a.indicator x ω = 1 := by unfold POVar.indicator exact Set.indicator_of_mem (show ω ∈ a.event x from hω) _

Causalean.PO.POVar.indicator_apply_eq_one · Causalean/PO/Core/Variable.lean:118
indicator_apply_eq_zero lemma — Pointwise: a.indicator x ω = 0 off {a = x}.

hypotheses

a :

POVar P α

x :

α

ω :

P.Ω

hω :

a.factual ω ≠ x

conclusion

a.indicator x ω = 0

Proof (Lean source)

lemma indicator_apply_eq_zero (a : POVar P α) {x : α} {ω : P.Ω} (hω : a.factual ω ≠ x) : a.indicator x ω = 0 := by unfold POVar.indicator exact Set.indicator_of_notMem (show ω ∉ a.event x from hω) _

Causalean.PO.POVar.indicator_apply_eq_zero · Causalean/PO/Core/Variable.lean:124
measurable_indicator lemma — a.indicator x is measurable.

hypotheses

a :

POVar P α

x :

α

hx :

MeasurableSet ({x} : Set α)

conclusion

Measurable (a.indicator x)

Proof (Lean source)

lemma measurable_indicator (a : POVar P α) (x : α) (hx : MeasurableSet ({x} : Set α)) : Measurable (a.indicator x) := by unfold POVar.indicator exact ((measurable_const : Measurable (fun _ : P.Ω => (1 : ℝ)))).indicator (a.measurableSet_event x hx)

Causalean.PO.POVar.measurable_indicator · Causalean/PO/Core/Variable.lean:130
stronglyMeasurable_indicator_comap lemma — a.indicator x is strongly measurable w.r.t. the σ-algebra generated by a.factual.

hypotheses

a :

POVar P α

x :

α

hx :

MeasurableSet ({x} : Set α)

conclusion

StronglyMeasurable[comap a.factual inferInstance] (a.indicator x)

Proof (Lean source)

lemma stronglyMeasurable_indicator_comap (a : POVar P α) (x : α) (hx : MeasurableSet ({x} : Set α)) : StronglyMeasurable[MeasurableSpace.comap a.factual inferInstance] (a.indicator x) := by letI : MeasurableSpace P.Ω := MeasurableSpace.comap a.factual inferInstance have hev : MeasurableSet[MeasurableSpace.comap a.factual inferInstance] (a.event x) := ⟨{x}, hx, rfl⟩ have hmeas : Measurable[MeasurableSpace.comap a.factual inferInstance] (a.indicator x) := by unfold POVar.indicator exact (measurable_const).indicator hev exact hmeas.stronglyMeasurable

Causalean.PO.POVar.stronglyMeasurable_indicator_comap · Causalean/PO/Core/Variable.lean:137
integrable_indicator lemma — a.indicator x is integrable under any finite measure (bounded by 1).

hypotheses

μ :

Measure P.Ω
IsFiniteMeasure μ

a :

POVar P α

x :

α

hx :

MeasurableSet ({x} : Set α)

conclusion

Integrable (a.indicator x) μ

Proof (Lean source)

lemma integrable_indicator {μ : Measure P.Ω} [IsFiniteMeasure μ] (a : POVar P α) (x : α) (hx : MeasurableSet ({x} : Set α)) : Integrable (a.indicator x) μ := by refine MeasureTheory.Integrable.of_bound (a.measurable_indicator x hx).aestronglyMeasurable 1 (Filter.Eventually.of_forall ?_) intro ω unfold POVar.indicator by_cases hω : ω ∈ a.event x · simp [Set.indicator_of_mem hω] · simp [Set.indicator_of_notMem hω]

Causalean.PO.POVar.integrable_indicator · Causalean/PO/Core/Variable.lean:153
indicator_eq_one_or_zero lemma — a.indicator x ω is always 0 or 1.

hypotheses

a :

POVar P α

x :

α

ω :

P.Ω

conclusion

a.indicator x ω = 1 ∨ a.indicator x ω = 0

Proof (Lean source)

lemma indicator_eq_one_or_zero (a : POVar P α) (x : α) (ω : P.Ω) : a.indicator x ω = 1 ∨ a.indicator x ω = 0 := by unfold POVar.indicator by_cases hω : ω ∈ a.event x · exact inl (by simp [Set.indicator_of_mem hω]) · exact inr (by simp [Set.indicator_of_notMem hω])

Causalean.PO.POVar.indicator_eq_one_or_zero · Causalean/PO/Core/Variable.lean:166
indicator_add_indicator_not lemma — Binary case: a.indicator true ω + a.indicator false ω = 1.

hypotheses

a :

POVar P Bool

ω :

P.Ω

conclusion

a.indicator true ω + a.indicator false ω = 1

Proof (Lean source)

lemma indicator_add_indicator_not (a : POVar P Bool) (ω : P.Ω) : a.indicator true ω + a.indicator false ω = 1 := by unfold POVar.indicator by_cases hT : a.factual ω = true · have hT_t : ω ∈ a.event true := hT have hT_f : ω ∉ a.event false := by change a.factual ω ≠ false; rw [hT]; decide simp [Set.indicator_of_mem hT_t, Set.indicator_of_notMem hT_f] · have hF : a.factual ω = false := by cases h : a.factual ω <;> simp_all have hT_t : ω ∉ a.event true := hT have hT_f : ω ∈ a.event false := hF simp [Set.indicator_of_notMem hT_t, Set.indicator_of_mem hT_f]

Causalean.PO.POVar.indicator_add_indicator_not · Causalean/PO/Core/Variable.lean:174
measurable_value lemma — The value function of a regimed variable is measurable.

hypotheses

rv :

RegimedVar P α

conclusion

Measurable rv.value

Proof (Lean source)

lemma measurable_value (rv : RegimedVar P α) : Measurable rv.value := rv.var.measurable_cf _

Causalean.PO.RegimedVar.measurable_value · Causalean/PO/Core/Variable.lean:211