PO.ID.Partial.Balke­Pearl.Sharp

ω :

SOmega

def

dArmω z ω :

given by

if z then ω.2.2.1 else ω.2.1

Causalean.PO.POBalkePearlSharp.dArmω · Causalean/PO/ID/Partial/BalkePearl/Sharp/CanonicalModel.lean:56 · uses SOmega

def yArmω reviewed

Causalean.PO.POBalkePearlSharp

For a binary treatment value and a canonical sample-space point, the latent outcome response is that point's outcome response under the specified treatment value.

Definition (Lean source)

parameters

d :

ω :

SOmega

def

yArmω d ω :

given by

if d then ω.2.2.2.2 else ω.2.2.2.1

Causalean.PO.POBalkePearlSharp.yArmω · Causalean/PO/ID/Partial/BalkePearl/Sharp/CanonicalModel.lean:60 · uses SOmega

def eval reviewed

Causalean.PO.POBalkePearlSharp

For an intervention regime on the canonical instrument, treatment, and outcome variables, a canonical sample-space point, and one of those variables, the canonical evaluator returns the variable's assigned value when the regime intervenes on it; otherwise it returns the point's instrument value, its treatment response to the resulting instrument value, or its outcome response to the resulting treatment value, respectively. For an intervened variable, the assigned value is used; for the instrument, the observed coordinate is used; for the treatment, the treatment response is used; and for the outcome, the outcome response is used.

Definition (Lean source)

parameters

r :

Regime SV SX

ω :

SOmega

v :

def

eval r ω v :

SX v

given by

by classical intro v exact if hv : v ∈ r.target then r.assign v hv else match v with | ⟨0, _⟩

=> ω.1 | ⟨1, _⟩ => let zEff : Bool := if h0 : (⟨0, by decide⟩ : SV) ∈ r.target then r.assign _ h0 else ω.1 dArmω zEff ω | ⟨2, _⟩ => let zEff : Bool := if h0 : (⟨0, by decide⟩ : SV) ∈ r.target then r.assign _ h0 else ω.1 let dEff : Bool := if h1 : (⟨1, by decide⟩ : SV) ∈ r.target then r.assign _ h1 else dArmω zEff ω yArmω dEff ω

Causalean.PO.POBalkePearlSharp.eval · Causalean/PO/ID/Partial/BalkePearl/Sharp/CanonicalModel.lean:64 · uses SOmega , SV , SX , Regime

def zMeasure reviewed

Causalean.PO.POBalkePearlSharp

For a potential-outcomes system and a binary Balke--Pearl system on it, the canonical instrument marginal measure assigns to each binary instrument value the probability of that system's corresponding factual instrument event.

Definition (Lean source)

parameters

P :

shared

S :

shared

def

zMeasure S :

Measure Bool

given by

∑ z : Bool, P.μ (S.zEvent z) • Measure.dirac z

Causalean.PO.POBalkePearlSharp.zMeasure · Causalean/PO/ID/Partial/BalkePearl/Sharp/CanonicalModel.lean:163 · uses POBalkePearlSystem , POSystem

def piMeasure reviewed

Causalean.PO.POBalkePearlSharp

For a table of real weights indexed by the four binary latent response values, the latent-table measure is the discrete measure that places at each response type the nonnegative extended-real part of its table weight.

Definition (Lean source)

parameters

π :

Bool → Bool → Bool → Bool → ℝ

def

piMeasure π :

Measure (Bool × Bool × Bool × Bool)

given by

∑ d0 : Bool, ∑ d1 : Bool, ∑ y0 : Bool, ∑ y1 : Bool, ofReal (π d0 d1 y0 y1) • Measure.dirac (d0, d1, y0, y1)

Causalean.PO.POBalkePearlSharp.piMeasure · Causalean/PO/ID/Partial/BalkePearl/Sharp/CanonicalModel.lean:167

def canonicalMeasure reviewed

Causalean.PO.POBalkePearlSharp

For a potential-outcomes system, a binary Balke--Pearl system on it, and a table of real weights indexed by the four binary latent response values, the canonical product measure is the product of the system's instrument marginal measure and the latent-table measure.

Definition (Lean source)

parameters

P :

shared

S :

shared

π :

Bool → Bool → Bool → Bool → ℝ

def

canonicalMeasure S π :

Measure SOmega

given by

(zMeasure S).prod (piMeasure π)

Causalean.PO.POBalkePearlSharp.canonicalMeasure · Causalean/PO/ID/Partial/BalkePearl/Sharp/CanonicalModel.lean:173 · uses SOmega , POBalkePearlSystem , POSystem

def canonicalPOSystem reviewed

Causalean.PO.POBalkePearlSharp

For a potential-outcomes system, a binary Balke--Pearl system on it, a table of real weights indexed by the four binary latent response values, the condition that every table entry is nonnegative, and the condition that all table entries sum to one, the canonical potential-outcomes system has the canonical variables, binary measurement scales, canonical sample space, canonical product probability measure, and canonical evaluator. Its probability-measure property follows from the two conditions on the latent table.

Definition (Lean source)

parameters

P :

shared

S :

shared

π :

Bool → Bool → Bool → Bool → ℝ

hπ_nn :

∀ d0 d1 y0 y1, 0 ≤ π d0 d1 y0 y1

hπ_sum :

∑ d0 : Bool, ∑ d1 : Bool, ∑ y0 : Bool, ∑ y1 : Bool, π d0 d1 y0 y1 = 1

def

canonicalPOSystem S π hπ_nn hπ_sum :

given by

letI : IsProbabilityMeasure (piMeasure π) := instIsProbPiMeasure hπ_nn hπ_sum { V := SV X := SX Ω := SOmega μ := canonicalMeasure S π eval := eval measurable_eval := measurable_eval }

Causalean.PO.POBalkePearlSharp.canonicalPOSystem · Causalean/PO/ID/Partial/BalkePearl/Sharp/CanonicalModel.lean:282 · uses POBalkePearlSystem , POSystem

def canonicalBP reviewed

Causalean.PO.POBalkePearlSharp

For a potential-outcomes system, a binary Balke--Pearl system on it, a table of real weights indexed by the four binary latent response values, the condition that every table entry is nonnegative, and the condition that all table entries sum to one, the canonical Balke--Pearl system designates the first, second, and third canonical variables as instrument, treatment, and outcome, respectively.

Definition (Lean source)

parameters

P :

shared

S :

shared

π :

Bool → Bool → Bool → Bool → ℝ

hπ_nn :

∀ d0 d1 y0 y1, 0 ≤ π d0 d1 y0 y1

hπ_sum :

∑ d0 : Bool, ∑ d1 : Bool, ∑ y0 : Bool, ∑ y1 : Bool, π d0 d1 y0 y1 = 1

def

canonicalBP S π hπ_nn hπ_sum :

POBalkePearlSystem (canonicalPOSystem S π hπ_nn hπ_sum)

given by

clause 1

Z := ⟨0, by decide⟩

clause 2

D := ⟨1, by decide⟩

clause 3

Y := ⟨2, by decide⟩

clause 4

hZbool := MeasurableEquiv.refl Bool

clause 5

hDbool := MeasurableEquiv.refl Bool

clause 6

hYbool := MeasurableEquiv.refl Bool

clause 7

hZD := by intro h; exact absurd (Fin.mk.inj_iff.mp h) (by decide)

clause 8

hZY := by intro h; exact absurd (Fin.mk.inj_iff.mp h) (by decide)

clause 9

hDY := by intro h; exact absurd (Fin.mk.inj_iff.mp h) (by decide)

Causalean.PO.POBalkePearlSharp.canonicalBP · Causalean/PO/ID/Partial/BalkePearl/Sharp/CanonicalModel.lean:299 · uses canonicalPOSystem , POBalkePearlSystem , POSystem

abbrev P' reviewed

Causalean.PO.POBalkePearlSharp

The canonical potential-outcomes system is the model built from the given nonnegative latent response-type probabilities that sum to one. It is the constructed system used to realize a feasible Balke--Pearl table.

Definition (Lean source)

parameters

P :

shared

S :

shared

π :

Bool → Bool → Bool → Bool → ℝ

shared

hπ_nn :

∀ (d0 d1 y0 y1 : Bool), 0 ≤ π d0 d1 y0 y1

shared

hπ_sum :

∑ d0, ∑ d1, ∑ y0, ∑ y1, π d0 d1 y0 y1 = 1

shared

def

P' S π hπ_nn hπ_sum :

given by

canonicalPOSystem S π hπ_nn hπ_sum

Causalean.PO.POBalkePearlSharp.P' · Causalean/PO/ID/Partial/BalkePearl/Sharp/CanonicalModel.lean:326 · uses POBalkePearlSystem , POSystem

abbrev S' reviewed

Causalean.PO.POBalkePearlSharp

The canonical Balke--Pearl system equips the constructed potential-outcomes system with its instrument, treatment, and outcome roles. It is used to verify that every feasible latent response-type table is realized by a Balke--Pearl model.

Definition (Lean source)

parameters

P :

shared

S :

shared

π :

Bool → Bool → Bool → Bool → ℝ

shared

hπ_nn :

∀ (d0 d1 y0 y1 : Bool), 0 ≤ π d0 d1 y0 y1

shared

hπ_sum :

∑ d0, ∑ d1, ∑ y0, ∑ y1, π d0 d1 y0 y1 = 1

shared

def

S' S π hπ_nn hπ_sum :

POBalkePearlSystem (canonicalPOSystem S π hπ_nn hπ_sum)

given by

canonicalBP S π hπ_nn hπ_sum

Causalean.PO.POBalkePearlSharp.S' · Causalean/PO/ID/Partial/BalkePearl/Sharp/CanonicalModel.lean:330 · uses canonicalPOSystem , POBalkePearlSystem , POSystem

lemma canonical_consistency reviewed

Causalean.PO.POBalkePearlSharp

For a potential-outcome system, a binary Balke–Pearl system, a canonical latent response-type table, nonnegativity of every table entry, and unit total table mass, the canonical potential-outcome construction satisfies factual consistency.

Formal statement

hypotheses

P :

shared

S :

shared

π :

Bool → Bool → Bool → Bool → ℝ

shared

hπ_nn :

∀ (d0 d1 y0 y1 : Bool), 0 ≤ π d0 d1 y0 y1

shared

hπ_sum :

∑ d0, ∑ d1, ∑ y0, ∑ y1, π d0 d1 y0 y1 = 1

shared

conclusion

(P' S π hπ_nn hπ_sum).Consistency

Proof (Lean source)

lemma canonical_consistency : (P' S π hπ_nn hπ_sum).Consistency := by refine ⟨?_⟩ · -- Factual consistency. intro r Y hYr ω hFA funext v -- v : {x // x ∈ Y} have hv_notr : v.val ∉ r.target := fun hvr => Finset.disjoint_left.mp hYr v.property hvr -- Show eval r ω v = eval Regime.empty ω v. change eval r ω v.val = eval Regime.empty ω v.val -- Case-split on v.val : Fin 3. -- We'll use eval_zero/eval_one/eval_two and Regime.empty_target. rcases v with ⟨v, hvY⟩ -- v : Fin 3. Match on Fin 3 with three cases. have hne_empty0 : (⟨0, by decide⟩ : SV) ∉ (Regime.empty : Regime SV SX).target := by rw [Regime.empty_target]; exact Finset.notMem_empty _ have hne_empty1 : (⟨1, by decide⟩ : SV) ∉ (Regime.empty : Regime SV SX).target := by rw [Regime.empty_target]; exact Finset.notMem_empty _ have hne_empty2 : (⟨2, by decide⟩ : SV) ∉ (Regime.empty : Regime SV SX).target := by rw [Regime.empty_target]; exact Finset.notMem_empty _ fin_cases v · -- v = ⟨0, _⟩ have hv0_notr : (⟨0, by decide⟩ : SV) ∉ r.target := hv_notr rw [eval_zero_of_not_mem r ω hv0_notr, eval_zero_of_not_mem (Regime.empty : Regime SV SX) ω hne_empty0] · -- v = ⟨1, _⟩ have hv1_notr : (⟨1, by decide⟩ : SV) ∉ r.target := hv_notr rw [eval_one_of_not_mem r ω hv1_notr, eval_one_of_not_mem (Regime.empty : Regime SV SX) ω hne_empty1] have hzEq : eval r ω ⟨0, by decide⟩ = eval Regime.empty ω ⟨0, by decide⟩ := by by_cases h0 : (⟨0, by decide⟩ : SV) ∈ r.target · exact (eval_zero_of_mem r ω h0).trans (hFA _ h0).symm · rw [eval_zero_of_not_mem r ω h0, eval_zero_of_not_mem (Regime.empty : Regime SV SX) ω hne_empty0] exact congrArg (fun z => dArmω z ω) hzEq · -- v = ⟨2, _⟩ have hv2_notr : (⟨2, by decide⟩ : SV) ∉ r.target := hv_notr rw [eval_two_of_not_mem r ω hv2_notr, eval_two_of_not_mem (Regime.empty : Regime SV SX) ω hne_empty2] have hzEq : eval r ω ⟨0, by decide⟩ = eval Regime.empty ω ⟨0, by decide⟩ := by by_cases h0 : (⟨0, by decide⟩ : SV) ∈ r.target · exact (eval_zero_of_mem r ω h0).trans (hFA _ h0).symm · rw [eval_zero_of_not_mem r ω h0, eval_zero_of_not_mem (Regime.empty : Regime SV SX) ω hne_empty0] have hdEq : eval r ω ⟨1, by decide⟩ = eval Regime.empty ω ⟨1, by decide⟩ := by by_cases h1 : (⟨1, by decide⟩ : SV) ∈ r.target · exact (eval_one_of_mem r ω h1).trans (hFA _ h1).symm · rw [eval_one_of_not_mem r ω h1, eval_one_of_not_mem (Regime.empty : Regime SV SX) ω hne_empty1] exact congrArg (fun z => dArmω z ω) hzEq exact congrArg (fun d => yArmω d ω) hdEq

Causalean.PO.POBalkePearlSharp.canonical_consistency · Causalean/PO/ID/Partial/BalkePearl/Sharp/CanonicalModel.lean:353 · uses P' , POBalkePearlSystem , POSystem , Consistency

15 supporting declarations (lemmas, instances)

measurable_eval lemma — The canonical evaluator is measurable under every intervention regime.

hypotheses

r :

Regime SV SX

conclusion

Measurable (eval r)

Proof (Lean source)

@[fun_prop] lemma measurable_eval (r : Regime SV SX) : Measurable (eval r) := by exact measurable_of_finite _

Causalean.PO.POBalkePearlSharp.measurable_eval · Causalean/PO/ID/Partial/BalkePearl/Sharp/CanonicalModel.lean:87
eval_zero lemma — The Z-coordinate eval r ω 0: assignment if intervened on, else ω.1.

hypotheses

r :

Regime SV SX

ω :

SOmega

conclusion

eval r ω ⟨0, by decide⟩
= (if h : (⟨0, by decide⟩ : SV) ∈ r.target then r.assign _ h else ω.1)

Proof (Lean source)

lemma eval_zero (r : Regime SV SX) (ω : SOmega) : eval r ω ⟨0, by decide⟩ = (if h : (⟨0, by decide⟩ : SV) ∈ r.target then r.assign _ h else ω.1) := rfl

Causalean.PO.POBalkePearlSharp.eval_zero · Causalean/PO/ID/Partial/BalkePearl/Sharp/CanonicalModel.lean:92
eval_one_raw lemma — The D-coordinate (raw).

hypotheses

r :

Regime SV SX

ω :

SOmega

conclusion

eval r ω ⟨1, by decide⟩
= (if h : (⟨1, by decide⟩ : SV) ∈ r.target then r.assign _ h else dArmω (if h0 : (⟨0, by decide⟩ : SV) ∈ r.target then r.assign _ h0 else ω.1) ω)

Proof (Lean source)

lemma eval_one_raw (r : Regime SV SX) (ω : SOmega) : eval r ω ⟨1, by decide⟩ = (if h : (⟨1, by decide⟩ : SV) ∈ r.target then r.assign _ h else dArmω (if h0 : (⟨0, by decide⟩ : SV) ∈ r.target then r.assign _ h0 else ω.1) ω) := rfl

Causalean.PO.POBalkePearlSharp.eval_one_raw · Causalean/PO/ID/Partial/BalkePearl/Sharp/CanonicalModel.lean:97
eval_two_raw lemma — The Y-coordinate (raw).

hypotheses

r :

Regime SV SX

ω :

SOmega

conclusion

eval r ω ⟨2, by decide⟩
= (if h : (⟨2, by decide⟩ : SV) ∈ r.target then r.assign _ h else yArmω (if h1 : (⟨1, by decide⟩ : SV) ∈ r.target then r.assign _ h1 else dArmω (if h0 : (⟨0, by decide⟩ : SV) ∈ r.target then r.assign _ h0 else ω.1) ω) ω)

Proof (Lean source)

lemma eval_two_raw (r : Regime SV SX) (ω : SOmega) : eval r ω ⟨2, by decide⟩ = (if h : (⟨2, by decide⟩ : SV) ∈ r.target then r.assign _ h else yArmω (if h1 : (⟨1, by decide⟩ : SV) ∈ r.target then r.assign _ h1 else dArmω (if h0 : (⟨0, by decide⟩ : SV) ∈ r.target then r.assign _ h0 else ω.1) ω) ω) := rfl

Causalean.PO.POBalkePearlSharp.eval_two_raw · Causalean/PO/ID/Partial/BalkePearl/Sharp/CanonicalModel.lean:104
eval_one lemma — The D-coordinate folded via eval_zero.

hypotheses

r :

Regime SV SX

ω :

SOmega

conclusion

eval r ω ⟨1, by decide⟩
= (if h : (⟨1, by decide⟩ : SV) ∈ r.target then r.assign _ h else dArmω (eval r ω ⟨0, by decide⟩) ω)

Proof (Lean source)

lemma eval_one (r : Regime SV SX) (ω : SOmega) : eval r ω ⟨1, by decide⟩ = (if h : (⟨1, by decide⟩ : SV) ∈ r.target then r.assign _ h else dArmω (eval r ω ⟨0, by decide⟩) ω) := by rw [eval_one_raw]; rfl

Causalean.PO.POBalkePearlSharp.eval_one · Causalean/PO/ID/Partial/BalkePearl/Sharp/CanonicalModel.lean:114
eval_two lemma — The Y-coordinate folded via eval_one.

hypotheses

r :

Regime SV SX

ω :

SOmega

conclusion

eval r ω ⟨2, by decide⟩
= (if h : (⟨2, by decide⟩ : SV) ∈ r.target then r.assign _ h else yArmω (eval r ω ⟨1, by decide⟩) ω)

Proof (Lean source)

lemma eval_two (r : Regime SV SX) (ω : SOmega) : eval r ω ⟨2, by decide⟩ = (if h : (⟨2, by decide⟩ : SV) ∈ r.target then r.assign _ h else yArmω (eval r ω ⟨1, by decide⟩) ω) := by rw [eval_two_raw]; rfl

Causalean.PO.POBalkePearlSharp.eval_two · Causalean/PO/ID/Partial/BalkePearl/Sharp/CanonicalModel.lean:121
eval_one_of_mem lemma — Given a regime and canonical state, if the first variable is intervened on, then the canonical evaluator returns that variable's assigned intervention value.

hypotheses

r :

Regime SV SX

ω :

SOmega

h :

(⟨1, by decide⟩ : SV) ∈ r.target

conclusion

eval r ω ⟨1, by decide⟩ = r.assign _ h

Proof (Lean source)

lemma eval_one_of_mem (r : Regime SV SX) (ω : SOmega) (h : (⟨1, by decide⟩ : SV) ∈ r.target) : eval r ω ⟨1, by decide⟩ = r.assign _ h := by exact (eval_one r ω).trans (dif_pos h)

Causalean.PO.POBalkePearlSharp.eval_one_of_mem · Causalean/PO/ID/Partial/BalkePearl/Sharp/CanonicalModel.lean:138
eval_two_of_not_mem lemma — Given a regime and canonical state, if the second variable is not intervened on, then the canonical evaluator returns the state's outcome arm indexed by the evaluated first variable.

hypotheses

r :

Regime SV SX

ω :

SOmega

h :

(⟨2, by decide⟩ : SV) ∉ r.target

conclusion

eval r ω ⟨2, by decide⟩ = yArmω (eval r ω ⟨1, by decide⟩) ω

Proof (Lean source)

lemma eval_two_of_not_mem (r : Regime SV SX) (ω : SOmega) (h : (⟨2, by decide⟩ : SV) ∉ r.target) : eval r ω ⟨2, by decide⟩ = yArmω (eval r ω ⟨1, by decide⟩) ω := by exact (eval_two r ω).trans (dif_neg h)

Causalean.PO.POBalkePearlSharp.eval_two_of_not_mem · Causalean/PO/ID/Partial/BalkePearl/Sharp/CanonicalModel.lean:150
zMeasure_univ lemma — zMeasure S has total mass 1.

hypotheses

P :

POSystem
shared

S :

POBalkePearlSystem P
shared

conclusion

(zMeasure S) univ = 1

Proof (Lean source)

lemma zMeasure_univ : (zMeasure S) univ = 1 := by unfold zMeasure rw [Measure.coe_finset_sum] simp only [Finset.sum_apply, Measure.coe_smul, Pi.smul_apply, smul_eq_mul] simp only [Measure.dirac_apply' _ MeasurableSet.univ, Set.indicator_univ, Pi.one_apply, mul_one] have hpart : (S.zEvent false) ∪ (S.zEvent true) = univ := by ext ω refine ⟨fun _ => trivial, fun _ => ?_⟩ cases h : S.zVar.factual ω · exact Or.inl h · exact Or.inr h have hdisj : Disjoint (S.zEvent false) (S.zEvent true) := by rw [Set.disjoint_left]; intro ω h1 h2 have h1' : S.zVar.factual ω = false := h1 have h2' : S.zVar.factual ω = true := h2 rw [h1'] at h2'; exact Bool.false_ne_true h2' have hmeas_t : MeasurableSet (S.zEvent true) := S.measurableSet_zEvent _ have hadd : P.μ (S.zEvent false) + P.μ (S.zEvent true) = P.μ univ := by rw [← measure_union hdisj hmeas_t, hpart] rw [Fintype.sum_bool, add_comm, hadd, measure_univ]

Causalean.PO.POBalkePearlSharp.zMeasure_univ · Causalean/PO/ID/Partial/BalkePearl/Sharp/CanonicalModel.lean:180
instIsProbZMeasure instance — For a potential-outcomes system and a binary Balke--Pearl system on that system, the canonical marginal distribution of the binary instrument is a probability measure.

parameters

P :

POSystem
shared

S :

POBalkePearlSystem P
shared

instance

instIsProbZMeasure S :
IsProbabilityMeasure (zMeasure S)

given by

⟨zMeasure_univ S⟩

Causalean.PO.POBalkePearlSharp.instIsProbZMeasure · Causalean/PO/ID/Partial/BalkePearl/Sharp/CanonicalModel.lean:203
piMeasure_univ_of_feasible lemma — piMeasure π has total mass 1 when π has nonneg entries summing to 1.

hypotheses

π :

Bool → Bool → Bool → Bool → ℝ

hπ_nn :

∀ d0 d1 y0 y1, 0 ≤ π d0 d1 y0 y1

hπ_sum :

∑ d0 : Bool, ∑ d1 : Bool, ∑ y0 : Bool, ∑ y1 : Bool, π d0 d1 y0 y1 = 1

conclusion

(piMeasure π) univ = 1

Proof (Lean source)

lemma piMeasure_univ_of_feasible {π : Bool → Bool → Bool → Bool → ℝ} (hπ_nn : ∀ d0 d1 y0 y1, 0 ≤ π d0 d1 y0 y1) (hπ_sum : ∑ d0 : Bool, ∑ d1 : Bool, ∑ y0 : Bool, ∑ y1 : Bool, π d0 d1 y0 y1 = 1) : (piMeasure π) univ = 1 := by unfold piMeasure -- Reduce iterated sum measure applied to univ to iterated sum of weights. simp only [Measure.coe_finset_sum, Finset.sum_apply, Measure.coe_smul, Pi.smul_apply, smul_eq_mul, Measure.dirac_apply' _ MeasurableSet.univ, Set.indicator_univ, Pi.one_apply, mul_one] -- Now goal: ∑ d0 ∑ d1 ∑ y0 ∑ y1, ofReal (π d0 d1 y0 y1) = 1 have h1 : ∀ d0 d1 y0, ∑ y1 : Bool, ofReal (π d0 d1 y0 y1) = ofReal (∑ y1 : Bool, π d0 d1 y0 y1) := by intros d0 d1 y0 rw [ENNReal.ofReal_sum_of_nonneg] intro y1 _; exact hπ_nn _ _ _ _ have h2 : ∀ d0 d1, ∑ y0 : Bool, ∑ y1 : Bool, ofReal (π d0 d1 y0 y1) = ofReal (∑ y0 : Bool, ∑ y1 : Bool, π d0 d1 y0 y1) := by intros d0 d1 simp_rw [h1] rw [ENNReal.ofReal_sum_of_nonneg] intro y0 _; exact Finset.sum_nonneg fun y1 _ => hπ_nn _ _ _ _ have h3 : ∀ d0, ∑ d1 : Bool, ∑ y0 : Bool, ∑ y1 : Bool, ofReal (π d0 d1 y0 y1) = ofReal (∑ d1 : Bool, ∑ y0 : Bool, ∑ y1 : Bool, π d0 d1 y0 y1) := by intros d0 simp_rw [h2] rw [ENNReal.ofReal_sum_of_nonneg] intro d1 _ exact Finset.sum_nonneg fun y0 _ => Finset.sum_nonneg fun y1 _ => hπ_nn _ _ _ _ have h4 : ∑ d0 : Bool, ∑ d1 : Bool, ∑ y0 : Bool, ∑ y1 : Bool, ofReal (π d0 d1 y0 y1) = ofReal (∑ d0 : Bool, ∑ d1 : Bool, ∑ y0 : Bool, ∑ y1 : Bool, π d0 d1 y0 y1) := by simp_rw [h3] rw [ENNReal.ofReal_sum_of_nonneg] intro d0 _ exact Finset.sum_nonneg fun d1 _ => Finset.sum_nonneg fun y0 _ => Finset.sum_nonneg fun y1 _ => hπ_nn _ _ _ _ rw [h4, hπ_sum] simp

Causalean.PO.POBalkePearlSharp.piMeasure_univ_of_feasible · Causalean/PO/ID/Partial/BalkePearl/Sharp/CanonicalModel.lean:211
instIsProbPiMeasure lemma — A nonnegative latent table that sums to one induces a probability measure.

hypotheses

π :

Bool → Bool → Bool → Bool → ℝ

hπ_nn :

∀ d0 d1 y0 y1, 0 ≤ π d0 d1 y0 y1

hπ_sum :

∑ d0 : Bool, ∑ d1 : Bool, ∑ y0 : Bool, ∑ y1 : Bool, π d0 d1 y0 y1 = 1

conclusion

IsProbabilityMeasure (piMeasure π)

Proof (Lean source)

lemma instIsProbPiMeasure {π : Bool → Bool → Bool → Bool → ℝ} (hπ_nn : ∀ d0 d1 y0 y1, 0 ≤ π d0 d1 y0 y1) (hπ_sum : ∑ d0 : Bool, ∑ d1 : Bool, ∑ y0 : Bool, ∑ y1 : Bool, π d0 d1 y0 y1 = 1) : IsProbabilityMeasure (piMeasure π) := ⟨piMeasure_univ_of_feasible hπ_nn hπ_sum⟩

Causalean.PO.POBalkePearlSharp.instIsProbPiMeasure · Causalean/PO/ID/Partial/BalkePearl/Sharp/CanonicalModel.lean:258
instIsProbCanonicalMeasure instance — For a potential-outcomes system, a binary Balke--Pearl system on that system, and a table of real weights indexed by the four binary latent response values, if the probability measure induced by that latent table is a probability measure, then the canonical product measure combining the instrument marginal and latent-table measure is a probability measure.

parameters

P :

POSystem
shared

S :

POBalkePearlSystem P
shared

π :

Bool → Bool → Bool → Bool → ℝ
IsProbabilityMeasure (piMeasure π)

instance

instIsProbCanonicalMeasure S :
IsProbabilityMeasure (canonicalMeasure S π)

given by

by unfold canonicalMeasure; infer_instance

Causalean.PO.POBalkePearlSharp.instIsProbCanonicalMeasure · Causalean/PO/ID/Partial/BalkePearl/Sharp/CanonicalModel.lean:268
sqcup_assign_right lemma — Given two disjoint regimes over a family of variable spaces, for a variable outside the first regime but inside the second, and a proof that it lies in their union, the union regime assigns the second regime's value.

hypotheses

V :

Type*
DecidableEq V
V → Type*

∀ v, MeasurableSpace (X v)

r₁ r₂ :

Regime V X

h :

r₁.Disjoint r₂

v :

V

hnin :

v ∉ r₁.target

hin :

v ∈ r₂.target

hsq :

v ∈ (r₁.sqcup r₂ h).target

conclusion

(r₁.sqcup r₂ h).assign v hsq = r₂.assign v hin

Proof (Lean source)

lemma sqcup_assign_right {V : Type*} [DecidableEq V] {X : V → Type*} [∀ v, MeasurableSpace (X v)] (r₁ r₂ : Regime V X) (h : r₁.Disjoint r₂) (v : V) (hnin : v ∉ r₁.target) (hin : v ∈ r₂.target) (hsq : v ∈ (r₁.sqcup r₂ h).target) : (r₁.sqcup r₂ h).assign v hsq = r₂.assign v hin := by exact Regime.sqcup_assign_neg r₁ r₂ h v hnin hin

Causalean.PO.POBalkePearlSharp.sqcup_assign_right · Causalean/PO/ID/Partial/BalkePearl/Sharp/CanonicalModel.lean:343
canonical_compositionConsistency lemma — For a potential-outcome system, a binary Balke–Pearl system, a canonical latent response-type table, nonnegativity of every table entry, and unit total table mass, the canonical potential-outcome construction satisfies composition consistency.

hypotheses

P :

POSystem
shared

S :

POBalkePearlSystem P
shared

π :

Bool → Bool → Bool → Bool → ℝ
shared

hπ_nn :

∀ (d0 d1 y0 y1 : Bool), 0 ≤ π d0 d1 y0 y1
shared

hπ_sum :

∑ d0, ∑ d1, ∑ y0, ∑ y1, π d0 d1 y0 y1 = 1
shared

conclusion

(P' S π hπ_nn hπ_sum).CompositionConsistency

Proof (Lean source)

lemma canonical_compositionConsistency : (P' S π hπ_nn hπ_sum).CompositionConsistency := by refine ⟨?_⟩ intro r₁ r₂ hd Y hY ω hIA -- Helper: agreement of `eval (r₁⊔r₂) ω` with `eval r₁ ω` at the Z-coord. have hzEq : eval (r₁.sqcup r₂ hd) ω ⟨0, by decide⟩ = eval r₁ ω ⟨0, by decide⟩ := by by_cases h01 : (⟨0, by decide⟩ : SV) ∈ r₁.target · have h0sq : (⟨0, by decide⟩ : SV) ∈ (r₁.sqcup r₂ hd).target := mem_union_left _ h01 exact (eval_zero_of_mem (r₁.sqcup r₂ hd) ω h0sq).trans ((sqcup_assign_left r₁ r₂ hd _ h01 h0sq).trans (eval_zero_of_mem r₁ ω h01).symm) · by_cases h02 : (⟨0, by decide⟩ : SV) ∈ r₂.target · have h0sq : (⟨0, by decide⟩ : SV) ∈ (r₁.sqcup r₂ hd).target := mem_union_right _ h02 exact (eval_zero_of_mem (r₁.sqcup r₂ hd) ω h0sq).trans ((sqcup_assign_right r₁ r₂ hd _ h01 h02 h0sq).trans (hIA _ h02).symm) · have h0sq : (⟨0, by decide⟩ : SV) ∉ (r₁.sqcup r₂ hd).target := by rw [Regime.sqcup_target]; intro h rcases Finset.mem_union.mp h with h | h · exact h01 h · exact h02 h rw [eval_zero_of_not_mem (r₁.sqcup r₂ hd) ω h0sq, eval_zero_of_not_mem r₁ ω h01] -- Helper: agreement at the D-coord. have hdEq : eval (r₁.sqcup r₂ hd) ω ⟨1, by decide⟩ = eval r₁ ω ⟨1, by decide⟩ := by by_cases h11 : (⟨1, by decide⟩ : SV) ∈ r₁.target · have h1sq : (⟨1, by decide⟩ : SV) ∈ (r₁.sqcup r₂ hd).target := mem_union_left _ h11 exact (eval_one_of_mem (r₁.sqcup r₂ hd) ω h1sq).trans ((sqcup_assign_left r₁ r₂ hd _ h11 h1sq).trans (eval_one_of_mem r₁ ω h11).symm) · by_cases h12 : (⟨1, by decide⟩ : SV) ∈ r₂.target · have h1sq : (⟨1, by decide⟩ : SV) ∈ (r₁.sqcup r₂ hd).target := mem_union_right _ h12 exact (eval_one_of_mem (r₁.sqcup r₂ hd) ω h1sq).trans ((sqcup_assign_right r₁ r₂ hd _ h11 h12 h1sq).trans (hIA _ h12).symm) · have h1sq : (⟨1, by decide⟩ : SV) ∉ (r₁.sqcup r₂ hd).target := by rw [Regime.sqcup_target]; intro h rcases Finset.mem_union.mp h with h | h · exact h11 h · exact h12 h rw [eval_one_of_not_mem (r₁.sqcup r₂ hd) ω h1sq, eval_one_of_not_mem r₁ ω h11] exact congrArg (fun z => dArmω z ω) hzEq funext v rcases v with ⟨v, hvY⟩ have hv_notr : v ∉ r₁.target ∪ r₂.target := Finset.disjoint_left.mp hY hvY have hv_notr1 : v ∉ r₁.target := fun h => hv_notr (mem_union_left _ h) have hv_not_sqcup : v ∉ (r₁.sqcup r₂ hd).target := by rw [Regime.sqcup_target]; exact hv_notr change eval (r₁.sqcup r₂ hd) ω v = eval r₁ ω v fin_cases v · exact hzEq · have hv1_not_sqcup : (⟨1, by decide⟩ : SV) ∉ (r₁.sqcup r₂ hd).target := hv_not_sqcup have hv1_notr1 : (⟨1, by decide⟩ : SV) ∉ r₁.target := hv_notr1 rw [eval_one_of_not_mem (r₁.sqcup r₂ hd) ω hv1_not_sqcup, eval_one_of_not_mem r₁ ω hv1_notr1] exact congrArg (fun z => dArmω z ω) hzEq · have hv2_not_sqcup : (⟨2, by decide⟩ : SV) ∉ (r₁.sqcup r₂ hd).target := hv_not_sqcup have hv2_notr1 : (⟨2, by decide⟩ : SV) ∉ r₁.target := hv_notr1 rw [eval_two_of_not_mem (r₁.sqcup r₂ hd) ω hv2_not_sqcup, eval_two_of_not_mem r₁ ω hv2_notr1] exact congrArg (fun d => yArmω d ω) hdEq

Causalean.PO.POBalkePearlSharp.canonical_compositionConsistency · Causalean/PO/ID/Partial/BalkePearl/Sharp/CanonicalModel.lean:408

Sharpness 2 core · 20 supporting This part verifies factual values, exclusion, exogeneity, and marginal identities for the canonical model, then proves realization of every feasible table and interval value. ★ balkePearl_sharp★ balkePearl_sharp_of_mem

Canonical identities and Balke-Pearl sharpness

This part verifies factual values, exclusion, exogeneity, and marginal identities for the canonical model, then proves realization of every feasible table and interval value.

theorem balkePearl_sharp reviewed

Causalean.PO.POBalkePearlSystem

Sharpness. Under the Balke-Pearl IV base assumptions, for a latent treatment-response table π that is feasible for the linear program — nonnegative, summing to one, and reproducing the observed cell probabilities as its marginals, there exists another potential-outcome system, satisfying the same base assumptions, whose observed cell probabilities agree with the original system's and whose average treatment effect equals the LP objective value of π: every feasible latent table is realised by some potential-outcome model.

Formal statement

hypotheses

P :

shared

S :

shared

hA :

S.BaseAssumptions

π :

Bool → Bool → Bool → Bool → ℝ

hπ :

BPFeasible S hA π

conclusion

∃ (P' : POSystem.{0,0,0}) (S' : POBalkePearlSystem P') (_hA' : S'.BaseAssumptions),

conclusion 1

y d z :

S'.cellProb y d z = S.cellProb y d z

conclusion 2

S'.ATE = BPObjective π

Proof (Lean source)

theorem balkePearl_sharp (hA : S.BaseAssumptions) (π : Bool → Bool → Bool → Bool → ℝ) (hπ : BPFeasible S hA π) : ∃ (P' : POSystem.{0,0,0}) (S' : POBalkePearlSystem P') (_hA' : S'.BaseAssumptions), (∀ y d z, S'.cellProb y d z = S.cellProb y d z) ∧ S'.ATE = BPObjective π := by refine ⟨POBalkePearlSharp.canonicalPOSystem S π hπ.nonneg hπ.sum_one, POBalkePearlSharp.canonicalBP S π hπ.nonneg hπ.sum_one, POBalkePearlSharp.canonical_baseAssumptions S π hπ.nonneg hπ.sum_one hA, ?_, ?_⟩ · intros y d z exact POBalkePearlSharp.canonical_cellProb_eq S π hπ.nonneg hπ.sum_one hA hπ y d z · exact POBalkePearlSharp.canonical_ATE_eq S π hπ.nonneg hπ.sum_one

Causalean.PO.POBalkePearlSystem.balkePearl_sharp · Causalean/PO/ID/Partial/BalkePearl/Sharp/Sharpness.lean:442 · uses POBalkePearlSystem , ATE , BPFeasible , BPObjective , BaseAssumptions , cellProb , POSystem

theorem balkePearl_sharp_of_mem reviewed

Causalean.PO.POBalkePearlSystem

Corollary of sharpness. Under the Balke-Pearl IV base assumptions, for a real number τ lying in the Balke-Pearl identified interval, there exists another potential-outcome system, satisfying the same base assumptions, whose observed cell probabilities agree with the original system's and whose average treatment effect equals τ: every value in the identified interval is the ATE of some BP-feasible model with matching observed cell probabilities.

Formal statement

hypotheses

P :

shared

S :