PO.Core

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

Regime 10 core · 21 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:29

def empty reviewed

Causalean.PO.Regime

For a collection of variables whose identities can be compared and their value spaces, the empty intervention regime targets no variable and consequently has no substantive assignments.

Definition (Lean source)

parameters

V :

Type u_1

V → Type u_2

shared

def

empty :

Regime V X

given by

clause 1

target := ∅

clause 2

assign := fun v hv => (notMem_empty v hv).elim

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

def Disjoint reviewed

Causalean.PO.Regime

For a collection of variables whose identities can be compared and their value spaces, two intervention regimes are disjoint exactly when no variable is targeted by both regimes.

Definition (Lean source)

parameters

V :

Type u_1

V → Type u_2

shared

r₁ r₂ :

Regime V X

def

Disjoint r₁ r₂ :

Prop

given by

_root_.Disjoint r₁.target r₂.target

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

def leftBiasedUnion reviewed

Causalean.PO.Regime

For a collection of variables whose identities can be compared and their value spaces, and two intervention regimes, the left-biased union targets every variable targeted by either regime and uses the first regime's assigned value whenever both assign that variable.

Definition (Lean source)

parameters

V :

Type u_1

V → Type u_2

shared

r₁ r₂ :

Regime V X

def

leftBiasedUnion r₁ r₂ :

Regime V X

given by

clause 1

target := r₁.target ∪ r₂.target

clause 2

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:52 · uses Regime

def sqcup reviewed

Causalean.PO.Regime

For a collection of variables whose identities can be compared and their value spaces, two intervention regimes, and the condition that they have no target variable in common, their disjoint union is their union regime, targeting every variable targeted by either regime and using its unique component assignment.

Definition (Lean source)

parameters

V :

Type u_1

V → Type u_2

shared

r₁ r₂ :

Regime V X

_h :

r₁.Disjoint r₂

def

sqcup r₁ r₂ _h :

Regime V X

given by

leftBiasedUnion r₁ r₂

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

def single reviewed

Causalean.PO.Regime

For a collection of variables whose identities can be compared, their value spaces, a variable, and a value in that variable's value space, the singleton intervention regime targets exactly that variable and assigns it that value.

Definition (Lean source)

parameters

V :

Type u_1

V → Type u_2

shared

v :

x :

X v

def

single v x :

Regime V X

given by

clause 1

target := {v}

clause 2

assign := fun _ hw => (Finset.mem_singleton.mp hw).symm ▸ x

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

def listLookup reviewed

Causalean.PO.Regime

For a collection of variables whose identities can be compared, their value spaces, a list of variable--value assignments, and a variable occurring in that list, the list lookup result is the value assigned to that variable by the first matching list entry: the empty-list case follows from the impossible occurrence assertion, while the nonempty-list case returns the head value when its variable matches and otherwise recurses on the tail.

Definition (Lean source)

parameters

V :

Type u_1

V → Type u_2

shared

l :

List ((v : V) × X v)

v :

v ∈ l.map fst

def

listLookup l v :

X v

given by

clause 1

| [], v, hv => by simp at hv

clause 2

| ⟨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:175

def ofListLeftBiased reviewed

Causalean.PO.Regime

For a collection of variables whose identities can be compared, their value spaces, and a list of variable--value assignments, the left-biased list-built regime targets the variables appearing in the list and assigns each the value at its first occurrence.

Definition (Lean source)

parameters

V :

Type u_1

V → Type u_2

shared

l :

List ((v : V) × X v)

def

ofListLeftBiased l :

Regime V X

given by

clause 1

target := (l.map fst).toFinset

clause 2

assign := fun v hv => listLookup l v (List.mem_toFinset.mp hv)

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

def ofList reviewed

Causalean.PO.Regime

For a collection of variables whose identities can be compared and their value spaces, a list of variable--value assignments, and the condition that no variable appears more than once in that list, the list-built intervention regime targets exactly the listed variables and assigns each its listed value.

Definition (Lean source)

parameters

V :

Type u_1

V → Type u_2

shared

l :

List ((v : V) × X v)

_h :

(l.map fst).Nodup

def

ofList l _h :

Regime V X

given by

ofListLeftBiased l

Causalean.PO.Regime.ofList · Causalean/PO/Core/Regime.lean:207 · 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

V :

Type u_1

V → Type u_2

shared

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:224 · uses ofList

21 supporting declarations (lemmas, instances)

disjoint_iff lemma — Two intervention regimes are disjoint exactly when their target sets are disjoint as finite sets.

hypotheses

V :

Type u_1
V → Type u_2
shared

r₁ r₂ :

Regime V X

conclusion

r₁.Disjoint r₂ ↔ _root_.Disjoint r₁.target r₂.target

Proof (Lean source)

@[causal_defs_simps] lemma disjoint_iff (r₁ r₂ : Regime V X) : r₁.Disjoint r₂ ↔ _root_.Disjoint r₁.target r₂.target := Iff.rfl

Causalean.PO.Regime.disjoint_iff · Causalean/PO/Core/Regime.lean:71
leftBiasedUnion_target lemma — The left-biased union of two regimes targets the union of their target sets.

hypotheses

V :

Type u_1
V → Type u_2
shared

r₁ r₂ :

Regime V X

conclusion

(r₁.leftBiasedUnion r₂).target = r₁.target ∪ r₂.target

Proof (Lean source)

@[causal_defs_simps] lemma leftBiasedUnion_target (r₁ r₂ : Regime V X) : (r₁.leftBiasedUnion r₂).target = r₁.target ∪ r₂.target := rfl

Causalean.PO.Regime.leftBiasedUnion_target · Causalean/PO/Core/Regime.lean:82
sqcup_eq_leftBiasedUnion lemma — The disjoint union of two compatible regimes is their left-biased union; disjointness makes the left bias immaterial.

hypotheses

V :

Type u_1
V → Type u_2
shared

r₁ r₂ :

Regime V X

h :

r₁.Disjoint r₂

conclusion

r₁.sqcup r₂ h = r₁.leftBiasedUnion r₂

Proof (Lean source)

@[causal_defs_simps] lemma sqcup_eq_leftBiasedUnion (r₁ r₂ : Regime V X) (h : r₁.Disjoint r₂) : r₁.sqcup r₂ h = r₁.leftBiasedUnion r₂ := rfl

Causalean.PO.Regime.sqcup_eq_leftBiasedUnion · Causalean/PO/Core/Regime.lean:91
empty_target lemma — The empty intervention regime has no target variables.

hypotheses

V :

Type u_1
V → Type u_2
shared

conclusion

(empty : Regime V X).target = ∅

Proof (Lean source)

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

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

hypotheses

V :

Type u_1
V → Type u_2
shared

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 [causal_defs_simps]

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

hypotheses

V :

Type u_1
V → Type u_2
shared

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 [causal_defs_simps]

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

hypotheses

V :

Type u_1
V → Type u_2
shared

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:112
sqcup_assign_pos lemma — sqcup agrees with r₁ whenever v ∈ r₁.target.

hypotheses

V :

Type u_1
V → Type u_2
shared

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:116
sqcup_assign_neg lemma — sqcup agrees with r₂ whenever v ∉ r₁.target (and hence v ∈ r₂.target).

hypotheses

V :

Type u_1
V → Type u_2
shared

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:123
ext theorem — Extensionality for Regime: equal targets and pointwise-equal assignments.

hypotheses

V :

Type u_1
V → Type u_2
Regime V X
shared

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:130
single_target theorem — The singleton intervention regime targets exactly the one variable it fixes.

hypotheses

V :

Type u_1
V → Type u_2
shared

v :

V

x :

X v

conclusion

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

Proof (Lean source)

@[simp, causal_defs_simps] 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:148
single_assign_self theorem — Evaluating the singleton intervention assignment at its target returns the supplied value.

hypotheses

V :

Type u_1
V → Type u_2
shared

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:152
single_disjoint_single theorem — Singleton intervention regimes on two distinct variables are disjoint.

hypotheses

V :

Type u_1
V → Type u_2
V
shared

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 [causal_defs_simps, hvw]

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

hypotheses

V :

Type u_1
V → Type u_2
V
shared

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 [causal_defs_simps, Finset.disjoint_singleton_left, h]

Causalean.PO.Regime.single_disjoint_of_not_mem · Causalean/PO/Core/Regime.lean:161
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 :

Type u_1
V → Type u_2
V
shared

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 [causal_defs_simps, Finset.disjoint_singleton_right, h]

Causalean.PO.Regime.disjoint_single_of_not_mem · Causalean/PO/Core/Regime.lean:167
ofListLeftBiased_target lemma — The regime built from a list of assignments by taking the first listed value for each variable targets exactly the finite set of listed variables.

hypotheses

V :

Type u_1
V → Type u_2
shared

l :

List ((v : V) × X v)

conclusion

(ofListLeftBiased l : Regime V X).target = (l.map fst).toFinset

Proof (Lean source)

@[causal_defs_simps] lemma ofListLeftBiased_target (l : List ((v : V) × X v)) : (ofListLeftBiased l : Regime V X).target = (l.map fst).toFinset := rfl

Causalean.PO.Regime.ofListLeftBiased_target · Causalean/PO/Core/Regime.lean:197
ofList_eq_ofListLeftBiased lemma — On a duplicate-free list of assignments, the regime it determines is the left-biased list-built regime; the duplicate-freeness makes the left bias immaterial.

hypotheses

V :

Type u_1
V → Type u_2
shared

l :

List ((v : V) × X v)

h :

(l.map fst).Nodup

conclusion

(ofList l h : Regime V X) = ofListLeftBiased l

Proof (Lean source)

@[causal_defs_simps] lemma ofList_eq_ofListLeftBiased (l : List ((v : V) × X v)) (h : (l.map fst).Nodup) : (ofList l h : Regime V X) = ofListLeftBiased l := rfl

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

hypotheses

V :

Type u_1
V → Type u_2
shared

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:231
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 :

Type u_1
V → Type u_2
V
shared

x :

X v

rest :

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 [causal_defs_simps]

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

hypotheses

V :

Type u_1
V → Type u_2
V
shared

x :

X v

rest :

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:245
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 :

Type u_1
V → Type u_2
V
shared

x :

X w

rest :

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:251

System 5 core · 5 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:28

def component reviewed

Causalean.PO.POSystem

For a potential-outcome system, an intervention regime, and a variable, the coordinate potential outcome assigns to each unit the value that variable would take under that intervention.

Definition (Lean source)

parameters

P :

POSystem

shared

r :

Regime P.V P.X

v :

P.V

def

component P r v :

P.Ω → P.X v

given by

fun ω => P.eval r ω v

Causalean.PO.POSystem.component · Causalean/PO/Core/System.lean:61 · 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

P :

POSystem

shared

r :

Regime P.V P.X

v :

P.V

conclusion

Measurable (P.component r v)

Proof (Lean source)

@[fun_prop] 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:82 · uses POSystem , component , Regime

def poVariable reviewed

Causalean.PO.POSystem

For a potential-outcome system, an intervention regime, and a finite set of variables, the joint potential outcome assigns to each unit the vector of values that all variables in the set would take under that intervention.

Definition (Lean source)

parameters

P :

POSystem

shared

r :

Regime P.V P.X

Y :

Finset P.V

def

poVariable P r Y :

P.Ω → ValuesOn Y P.X

given by

fun ω v => P.eval r ω v.val

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

def poOperator reviewed

Causalean.PO.POSystem

For a potential-outcome system, an intervention regime, and a finite set of variables, the potential-outcome law is the distribution of those variables' joint potential outcome under that intervention, induced by the system's probability measure.

Definition (Lean source)

parameters

P :

POSystem

shared

r :

Regime P.V P.X

Y :

Finset P.V

def

poOperator P r Y :

Measure (ValuesOn Y P.X)

given by

(P.μ).map (P.poVariable r Y)

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

5 supporting declarations (lemmas, instances)

component_apply lemma — At a given unit, the coordinate potential outcome of a variable under a regime is the system's world evaluation of that variable at that unit under that regime.

hypotheses

P :

POSystem
shared

r :

Regime P.V P.X

v :

P.V

ω :

P.Ω

conclusion

P.component r v ω = P.eval r ω v

Proof (Lean source)

@[causal_defs_simps] lemma component_apply (r : Regime P.V P.X) (v : P.V) (ω : P.Ω) : P.component r v ω = P.eval r ω v := rfl

Causalean.PO.POSystem.component_apply · Causalean/PO/Core/System.lean:70
poVariable_apply lemma — Reading off one coordinate of the joint potential outcome of a finite variable set under a regime gives the system's world evaluation of that coordinate's variable, at the same unit and under the same regime.

hypotheses

P :

POSystem
shared

r :

Regime P.V P.X

Y :

Finset P.V

ω :

P.Ω

v :

{w : P.V // w ∈ Y}

conclusion

P.poVariable r Y ω v = P.eval r ω v.val

Proof (Lean source)

@[causal_defs_simps] lemma poVariable_apply (r : Regime P.V P.X) (Y : Finset P.V) (ω : P.Ω) (v : {w : P.V // w ∈ Y}) : P.poVariable r Y ω v = P.eval r ω v.val := rfl

Causalean.PO.POSystem.poVariable_apply · Causalean/PO/Core/System.lean:100
measurable_poVariable lemma — The joint potential outcome for any finite set of variables under any intervention regime is measurable.

hypotheses

P :

POSystem
shared

r :

Regime P.V P.X

Y :

Finset P.V

conclusion

Measurable (P.poVariable r Y)

Proof (Lean source)

@[fun_prop] 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:113
poOperator_eq lemma — The potential-outcome law of a finite variable set under a regime is the pushforward of the system's probability measure along the joint potential outcome for that set and regime.

hypotheses

P :

POSystem
shared

r :

Regime P.V P.X

Y :

Finset P.V

conclusion

P.poOperator r Y = (P.μ).map (P.poVariable r Y)

Proof (Lean source)

@[causal_defs_simps] lemma poOperator_eq (r : Regime P.V P.X) (Y : Finset P.V) : P.poOperator r Y = (P.μ).map (P.poVariable r Y) := rfl

Causalean.PO.POSystem.poOperator_eq · Causalean/PO/Core/System.lean:132
instIsProbabilityMeasureValuesOnVXPoOperator instance — For a potential-outcomes system, an intervention regime, and a finite set of variables, the distribution of those variables' joint potential outcome under that regime is a probability measure.

parameters

P :

POSystem
shared

r :

Regime P.V P.X

Y :

Finset P.V

instance

instIsProbabilityMeasureValuesOnVXPoOperator P r Y :
IsProbabilityMeasure (P.poOperator r Y)

given by

by simp only [causal_defs_simps] exact isProbabilityMeasure_map (P.measurable_poVariable r Y).aemeasurable

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

Counterfactual 3 core · 4 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 and a finite ordered list of queries, each consisting of an intervention regime and a finite variable set, the cross-world evaluation map assigns to every unit the tuple whose $i$ th component is the joint potential outcome for the $i$ th query.

Definition (Lean source)

parameters

P :

POSystem

shared

qs :

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

P.Ω

i :

Fin qs.length

def

crossWorldEval P qs i :

ValuesOn (qs[i].2) P.X

given by

fun ω i => P.poVariable (qs[i].1) (qs[i].2) ω

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

def counterfactualDist reviewed

Causalean.PO.POSystem

For a potential-outcome system and a finite ordered list of counterfactual queries, the joint counterfactual distribution is the probability measure induced by applying the cross-world evaluation map to a random unit drawn from the system's probability measure.

Definition (Lean source)

parameters

P :

POSystem

shared

qs :

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

def

counterfactualDist P qs :

Measure ((i : Fin qs.length) → ValuesOn (qs[i].2) P.X)

given by

P.μ.map (P.crossWorldEval qs)

Causalean.PO.POSystem.counterfactualDist · Causalean/PO/Core/Counterfactual.lean:61 · 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

P :

POSystem

shared

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 simp only [causal_defs_simps] rw [MeasureTheory.Measure.map_map (measurable_pi_apply i) (P.measurable_crossWorldEval qs)] rfl

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

4 supporting declarations (lemmas, instances)

crossWorldEval_apply lemma — Reading off the i-th coordinate of the cross-world evaluation of a unit returns the joint potential outcome of the i-th query's variable set under the i-th query's regime, at that same unit.

hypotheses

P :

POSystem
shared

qs :

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

ω :

P.Ω

i :

Fin qs.length

conclusion

P.crossWorldEval qs ω i = P.poVariable (qs[i].1) (qs[i].2) ω

Proof (Lean source)

@[causal_defs_simps] lemma crossWorldEval_apply (qs : List (Regime P.V P.X × Finset P.V)) (ω : P.Ω) (i : Fin qs.length) : P.crossWorldEval qs ω i = P.poVariable (qs[i].1) (qs[i].2) ω := rfl

Causalean.PO.POSystem.crossWorldEval_apply · Causalean/PO/Core/Counterfactual.lean:39
measurable_crossWorldEval lemma — The cross-world evaluation map for a finite list of counterfactual queries is measurable.

hypotheses

P :

POSystem
shared

qs :

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

conclusion

Measurable (P.crossWorldEval qs)

Proof (Lean source)

@[fun_prop] 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:52
counterfactualDist_eq lemma — The joint counterfactual law of a finite list of queries is the pushforward of the system's probability measure along the cross-world evaluation map for those queries.

hypotheses

P :

POSystem
shared

qs :

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

conclusion

P.counterfactualDist qs = P.μ.map (P.crossWorldEval qs)

Proof (Lean source)

@[causal_defs_simps] lemma counterfactualDist_eq (qs : List (Regime P.V P.X × Finset P.V)) : P.counterfactualDist qs = P.μ.map (P.crossWorldEval qs) := rfl

Causalean.PO.POSystem.counterfactualDist_eq · Causalean/PO/Core/Counterfactual.lean:74
instIsProbabilityMeasureForallValuesOnVSndRegimeXFinsetGetElemListProdFinLengthLtNatValCounterfactualDist instance — For a potential-outcomes system and a finite ordered list of counterfactual queries, each consisting of an intervention regime and a finite variable set, the joint cross-world counterfactual distribution for that list is a probability measure.

parameters

P :

POSystem
shared

qs :

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

instance

instIsProbabilityMeasureForallValuesOnVSndRegimeXFinsetGetElemListProdFinLengthLtNatValCounterfactualDist P qs :
IsProbabilityMeasure (P.counterfactualDist qs)

given by

by simp only [causal_defs_simps] exact isProbabilityMeasure_map (P.measurable_crossWorldEval qs).aemeasurable

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

Variable 11 core · 22 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:29 · uses POSystem

def cf reviewed

Causalean.PO.POVar

For a potential-outcome system, a measurable analysis scale, a potential-outcome variable, and an intervention regime, the counterfactual value function maps every sample-space unit to that variable's potential outcome under the regime, expressed on the analysis scale.

Definition (Lean source)

parameters

P :

POSystem

shared

α :

Type u_1

shared

a :

POVar P α

r :

Regime P.V P.X

def

cf a r :

P.Ω → α

given by

fun ω => a.equiv (P.eval r ω a.v)

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

def factual reviewed

Causalean.PO.POVar

For a potential-outcome system, a measurable analysis scale, and a potential-outcome variable, the factual value function maps every sample-space unit to the variable's potential outcome under the empty intervention regime, expressed on the analysis scale.

Definition (Lean source)

parameters

P :

POSystem

shared

α :

Type u_1

shared

a :

POVar P α

def

factual a :

P.Ω → α

given by

a.cf Regime.empty

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

def event reviewed

Causalean.PO.POVar

For a potential-outcome system, a measurable analysis scale, a potential-outcome variable, and a value on that scale, the factual-value event is the set of all sample-space units whose factual value of the variable equals that value.

Definition (Lean source)

parameters

P :

POSystem

shared

α :

Type u_1

shared

a :

POVar P α

x :

def

event a x :

Set P.Ω

given by

a.factual ⁻¹' {x}

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

def cfUnder reviewed

Causalean.PO.POVar

For a potential-outcome system, a measurable outcome scale, a measurable intervention-variable scale, an outcome variable, an intervention variable, and a value of that intervention variable, the single-intervention counterfactual value function maps every sample-space unit to the outcome variable's potential outcome when the intervention variable is set to that value.

Definition (Lean source)

parameters

P :

POSystem

shared

α :

Type u_1

shared

β :

Type*

MeasurableSpace β

y :

POVar P α

w :

POVar P β

d :

def

cfUnder y w d :

P.Ω → α

given by

y.cf (Regime.single w.v (w.equiv.symm d))

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

def indicator reviewed

Causalean.PO.POVar

For a potential-outcome system, a measurable analysis scale, a potential-outcome variable, and a value on that scale, the factual-value indicator maps each sample-space unit to one when the variable's factual value equals that value and to zero otherwise.

Definition (Lean source)

parameters

P :

POSystem

shared

α :

Type u_1

shared

a :

POVar P α

x :

def

indicator a x :

P.Ω → ℝ

given by

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

Causalean.PO.POVar.indicator · Causalean/PO/Core/Variable.lean:145 · 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

P :

POSystem

shared

α :

Type u_1

shared

a :

POVar P α

x :

conclusion

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

Proof (Lean source)

@[indicator_simps, causal_defs_simps] 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:153 · 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:289 · uses POSystem

def value reviewed

Causalean.PO.RegimedVar

For a potential-outcome system, a measurable analysis scale, and a variable paired with an intervention regime, the regimed-variable value function maps every sample-space unit to the paired variable's potential outcome under its paired regime.

Definition (Lean source)

parameters

P :

POSystem

shared

α :

Type u_1

shared

rv :

RegimedVar P α

def

value rv :

P.Ω → α

given by

rv.var.cf rv.regime

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

def ofFactual reviewed

Causalean.PO.RegimedVar

For a potential-outcome system, a measurable analysis scale, and a potential-outcome variable, the factual bundle pairs that variable with the empty intervention regime.

Definition (Lean source)

parameters

P :

POSystem

shared

α :

Type u_1

shared

a :

POVar P α

def

ofFactual a :

RegimedVar P α

given by

⟨a, Regime.empty⟩

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

def ofSingle reviewed

Causalean.PO.RegimedVar

For a potential-outcome system, a measurable analysis scale, a potential-outcome variable, a system variable, and a value in that variable's native value space, the single-intervention bundle pairs the potential-outcome variable with the regime that fixes the system variable to that value.

Definition (Lean source)

parameters

P :

POSystem

shared

α :

Type u_1

shared

a :

POVar P α

w :

P.V

x :

P.X w

def

ofSingle a w x :

RegimedVar P α

given by

⟨a, Regime.single w x⟩

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

22 supporting declarations (lemmas, instances)

cf_apply lemma — At a given unit, the counterfactual value of a variable under a regime is the system's world evaluation of that variable at that unit under that regime, carried over to the analysis scale by the variable's measurable equivalence.

hypotheses

P :

POSystem
shared

α :

Type u_1
shared

a :

POVar P α

r :

Regime P.V P.X

ω :

P.Ω

conclusion

a.cf r ω = a.equiv (P.eval r ω a.v)

Proof (Lean source)

@[causal_defs_simps] lemma cf_apply (a : POVar P α) (r : Regime P.V P.X) (ω : P.Ω) : a.cf r ω = a.equiv (P.eval r ω a.v) := rfl

Causalean.PO.POVar.cf_apply · Causalean/PO/Core/Variable.lean:51
factual_eq lemma — The factual value function of a variable is its counterfactual value function under the empty intervention regime.

hypotheses

P :

POSystem
shared

α :

Type u_1
shared

a :

POVar P α

conclusion

a.factual = a.cf Regime.empty

Proof (Lean source)

@[causal_defs_simps] lemma factual_eq (a : POVar P α) : a.factual = a.cf Regime.empty := rfl

Causalean.PO.POVar.factual_eq · Causalean/PO/Core/Variable.lean:68
measurable_cf lemma — The counterfactual-value function of a potential-outcome variable under any intervention regime is measurable.

hypotheses

P :

POSystem
shared

α :

Type u_1
shared

a :

POVar P α

r :

Regime P.V P.X

conclusion

Measurable (a.cf r)

Proof (Lean source)

@[fun_prop] 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:77
measurable_factual lemma — The factual-value function of a potential-outcome variable is measurable.

hypotheses

P :

POSystem
shared

α :

Type u_1
shared

a :

POVar P α

conclusion

Measurable a.factual

Proof (Lean source)

@[fun_prop] lemma measurable_factual (a : POVar P α) : Measurable a.factual := a.measurable_cf _

Causalean.PO.POVar.measurable_factual · Causalean/PO/Core/Variable.lean:84
event_eq lemma — The factual-value event of a variable at a value is the preimage, under the variable's factual value function, of the one-point set at that value.

hypotheses

P :

POSystem
shared

α :

Type u_1
shared

a :

POVar P α

x :

α

conclusion

a.event x = a.factual ⁻¹' {x}

Proof (Lean source)

@[causal_defs_simps] lemma event_eq (a : POVar P α) (x : α) : a.event x = a.factual ⁻¹' {x} := rfl

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

hypotheses

P :

POSystem
shared

α :

Type u_1
shared

a :

POVar P α

x :

α

hx :

MeasurableSet ({x} : Set α)

conclusion

MeasurableSet (a.event x)

Proof (Lean source)

@[measurability] 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:104
cfUnder_eq lemma — The single-intervention counterfactual value function of an outcome variable at a treatment value is its counterfactual value function under the singleton regime that fixes the treatment variable to that value, read back through the treatment variable's measurable equivalence.

hypotheses

P :

POSystem
shared

α :

Type u_1
shared

β :

Type*
MeasurableSpace β

y :

POVar P α

w :

POVar P β

d :

β

conclusion

y.cfUnder w d = y.cf (Regime.single w.v (w.equiv.symm d))

Proof (Lean source)

@[causal_defs_simps] lemma cfUnder_eq {β : Type*} [MeasurableSpace β] (y : POVar P α) (w : POVar P β) (d : β) : y.cfUnder w d = y.cf (Regime.single w.v (w.equiv.symm d)) := rfl

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

hypotheses

P :

POSystem
shared

α :

Type u_1
shared

β :

Type*
MeasurableSpace β

y :

POVar P α

w :

POVar P β

d :

β

conclusion

Measurable (y.cfUnder w d)

Proof (Lean source)

@[fun_prop] 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:133
indicator_apply_eq_one lemma — Pointwise: a.indicator x ω = 1 on {a = x}.

hypotheses

P :

POSystem
shared

α :

Type u_1
shared

a :

POVar P α

x :

α

ω :

P.Ω

hω :

a.factual ω = x

conclusion

a.indicator x ω = 1

Proof (Lean source)

@[indicator_simps] lemma indicator_apply_eq_one (a : POVar P α) {x : α} {ω : P.Ω} (hω : a.factual ω = x) : a.indicator x ω = 1 := by simp only [causal_defs_simps] exact Set.indicator_of_mem (show ω ∈ a.event x from hω) _

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

hypotheses

P :

POSystem
shared

α :

Type u_1
shared

a :

POVar P α

x :

α

ω :

P.Ω

hω :

a.factual ω ≠ x

conclusion

a.indicator x ω = 0

Proof (Lean source)

@[indicator_simps] lemma indicator_apply_eq_zero (a : POVar P α) {x : α} {ω : P.Ω} (hω : a.factual ω ≠ x) : a.indicator x ω = 0 := by simp only [causal_defs_simps] exact Set.indicator_of_notMem (show ω ∉ a.event x from hω) _

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

hypotheses

P :

POSystem
shared

α :

Type u_1
shared

a :

POVar P α

x :

α

hx :

MeasurableSet ({x} : Set α)

conclusion

Measurable (a.indicator x)

Proof (Lean source)

@[fun_prop] lemma measurable_indicator (a : POVar P α) (x : α) (hx : MeasurableSet ({x} : Set α)) : Measurable (a.indicator x) := by simp only [causal_defs_simps] exact ((measurable_const : Measurable (fun _ : P.Ω => (1 : ℝ)))).indicator (a.measurableSet_event x hx)

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

hypotheses

P :

POSystem
shared

α :

Type u_1
shared

a :

POVar P α

x :

α

hx :

MeasurableSet ({x} : Set α)

conclusion

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

Proof (Lean source)

@[fun_prop] 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 simp only [causal_defs_simps] exact (measurable_const).indicator hev exact hmeas.stronglyMeasurable

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

hypotheses

P :

POSystem
shared

α :

Type u_1
shared

μ :

Measure P.Ω
IsFiniteMeasure μ

a :

POVar P α

x :

α

hx :

MeasurableSet ({x} : Set α)

conclusion

Integrable (a.indicator x) μ

Proof (Lean source)

@[fun_prop] 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:199
stronglyMeasurable_indicator lemma — The real-valued factual indicator of a potential-outcome variable at a singleton-measurable value is strongly measurable on the sample space.

hypotheses

P :

POSystem
shared

α :

Type u_1
shared

a :

POVar P α

x :

α

hx :

MeasurableSet ({x} : Set α)

conclusion

StronglyMeasurable (a.indicator x)

Proof (Lean source)

@[fun_prop] lemma stronglyMeasurable_indicator (a : POVar P α) (x : α) (hx : MeasurableSet ({x} : Set α)) : StronglyMeasurable (a.indicator x) := (a.measurable_indicator x hx).stronglyMeasurable

Causalean.PO.POVar.stronglyMeasurable_indicator · Causalean/PO/Core/Variable.lean:222
measurable_indicator_of_singleton lemma — On a value space whose one-point sets are measurable, the factual indicator of a potential-outcome variable at any value is a measurable function of the unit.

hypotheses

P :

POSystem
shared

α :

Type u_1
MeasurableSingletonClass α
shared

a :

POVar P α

x :

α

conclusion

Measurable (a.indicator x)

Proof (Lean source)

@[fun_prop] lemma measurable_indicator_of_singleton [MeasurableSingletonClass α] (a : POVar P α) (x : α) : Measurable (a.indicator x) := a.measurable_indicator x (MeasurableSet.singleton x)

Causalean.PO.POVar.measurable_indicator_of_singleton · Causalean/PO/Core/Variable.lean:230
stronglyMeasurable_indicator_of_singleton lemma — On a value space whose one-point sets are measurable, the factual indicator of a potential-outcome variable at any value is strongly measurable on the sample space.

hypotheses

P :

POSystem
shared

α :

Type u_1
MeasurableSingletonClass α
shared

a :

POVar P α

x :

α

conclusion

StronglyMeasurable (a.indicator x)

Proof (Lean source)

@[fun_prop] lemma stronglyMeasurable_indicator_of_singleton [MeasurableSingletonClass α] (a : POVar P α) (x : α) : StronglyMeasurable (a.indicator x) := (a.measurable_indicator x (MeasurableSet.singleton x)).stronglyMeasurable

Causalean.PO.POVar.stronglyMeasurable_indicator_of_singleton · Causalean/PO/Core/Variable.lean:237
stronglyMeasurable_indicator_comap_of_singleton lemma — On a value space whose one-point sets are measurable, the factual indicator of a potential-outcome variable at any value is strongly measurable with respect to the information carried by that variable's factual value.

hypotheses

P :

POSystem
shared

α :

Type u_1
MeasurableSingletonClass α
shared

a :

POVar P α

x :

α

conclusion

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

Proof (Lean source)

@[fun_prop] lemma stronglyMeasurable_indicator_comap_of_singleton [MeasurableSingletonClass α] (a : POVar P α) (x : α) : StronglyMeasurable[comap a.factual inferInstance] (a.indicator x) := a.stronglyMeasurable_indicator_comap x (MeasurableSet.singleton x)

Causalean.PO.POVar.stronglyMeasurable_indicator_comap_of_singleton · Causalean/PO/Core/Variable.lean:245
integrable_indicator_of_singleton lemma — On a value space whose one-point sets are measurable, the factual indicator of a potential-outcome variable at any value is integrable under every finite measure on the sample space.

hypotheses

P :

POSystem
shared

α :

Type u_1
MeasurableSingletonClass α
shared

μ :

Measure P.Ω
IsFiniteMeasure μ

a :

POVar P α

x :

α

conclusion

Integrable (a.indicator x) μ

Proof (Lean source)

@[fun_prop] lemma integrable_indicator_of_singleton [MeasurableSingletonClass α] {μ : Measure P.Ω} [IsFiniteMeasure μ] (a : POVar P α) (x : α) : Integrable (a.indicator x) μ := a.integrable_indicator x (MeasurableSet.singleton x)

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

hypotheses

P :

POSystem
shared

α :

Type u_1
shared

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:264
indicator_add_indicator_not lemma — Binary case: a.indicator true ω + a.indicator false ω = 1.

hypotheses

P :

POSystem
shared

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:272
value_eq lemma — The value function of a regimed variable is the counterfactual value function of its underlying variable under its bundled regime.

hypotheses

P :

POSystem
shared

α :

Type u_1
shared

rv :

RegimedVar P α

conclusion

rv.value = rv.var.cf rv.regime

Proof (Lean source)

@[causal_defs_simps] lemma value_eq (rv : RegimedVar P α) : rv.value = rv.var.cf rv.regime := rfl

Causalean.PO.RegimedVar.value_eq · Causalean/PO/Core/Variable.lean:308
measurable_value lemma — The value function of a regimed variable is measurable.

hypotheses

P :

POSystem
shared

α :

Type u_1
shared

rv :

RegimedVar P α

conclusion

Measurable rv.value

Proof (Lean source)

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

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