PO.ID.Partial.BalkePearl
Balke-Pearl linear-programming bounds for the ATE under an imperfect instrument.
Setup 19 core · 10 supporting This file defines the data layer for Balke-Pearl partial identification of the average treatment effect with a binary instrument, binary treatment, and binary outcome. ★ POBalkePearlSystem★ measurable_DofZ
Balke-Pearl Setup
This file defines the data layer for Balke-Pearl partial identification of the
average treatment effect with a binary instrument, binary treatment, and binary
outcome. The structure POBalkePearlSystem records the three binary system
variables and their distinctness; its namespace supplies the factual variables
factualZ, factualD, factualY, the counterfactuals DofZ, YofD, and
YofZD, the real-valued Boolean embedding used for integration, the target
estimand ATE, and the observable conditional cell probability cellProb.
Binary-IV system for Balke–Pearl ATE bounds (def:po-iv-balke-pearl-system). Inside a potential-outcome system, this bundles a binary instrument node Z, a binary treatment node D, and a binary outcome node Y, subject to the instrument, treatment, and outcome being pairwise distinct system variables.
For a potential-outcomes system and a binary Balke--Pearl system on it, the instrument variable is the system's instrument, packaged together with its binary measurement scale.
Definition (Lean source)
For a potential-outcomes system and a binary Balke--Pearl system on it, the treatment variable is the system's treatment, packaged together with its binary measurement scale.
Definition (Lean source)
For a potential-outcomes system and a binary Balke--Pearl system on it, the outcome variable is the system's outcome, packaged together with its binary measurement scale.
Definition (Lean source)
For a potential-outcomes system, a binary Balke--Pearl system on it, and an instrument value, the potential treatment function maps each unit to the treatment it would receive were the instrument set to that value.
Definition (Lean source)
For a potential-outcomes system, a binary Balke--Pearl system on it, and a treatment value, the potential outcome function maps each unit to the binary outcome it would have under that treatment value.
Definition (Lean source)
For a potential-outcomes system, a binary Balke--Pearl system on it, an instrument value, and a treatment value, the joint intervention regime sets the instrument to the specified instrument value and the treatment to the specified treatment value.
Definition (Lean source)
For a potential-outcomes system, a binary Balke--Pearl system on it, an instrument value, and a treatment value, the joint-intervention potential outcome function maps each unit to its outcome when the instrument and treatment are set jointly to those values.
Definition (Lean source)
For a potential-outcomes system and a binary Balke--Pearl system on it, the factual instrument function maps each unit to its observed binary instrument value.
Definition (Lean source)
For a potential-outcomes system and a binary Balke--Pearl system on it, the factual treatment function maps each unit to its observed binary treatment value.
Definition (Lean source)
For a potential-outcomes system and a binary Balke--Pearl system on it, the factual outcome function maps each unit to its observed binary outcome value.
Definition (Lean source)
The binary-to-real encoding maps every binary value to a real number: for true, its value is one, and for false, its value is zero.
For a potential-outcomes system, a binary Balke--Pearl system on it, and a treatment value, the real-valued potential outcome function maps each unit's binary potential outcome under that treatment to its zero--one real encoding.
Definition (Lean source)
For a potential-outcomes system, a binary Balke--Pearl system on it, and an instrument value, the instrument event is the set of units whose factual instrument equals that value.
Definition (Lean source)
For a potential-outcomes system, a binary Balke--Pearl system on it, and a treatment value, the treatment event is the set of units whose factual treatment equals that value.
Definition (Lean source)
For a potential-outcomes system, a binary Balke--Pearl system on it, and an outcome value, the outcome event is the set of units whose factual outcome equals that value.
Definition (Lean source)
For a fixed instrument value z, the potential treatment D(z) is measurable.
Formal statement
Proof (Lean source)
For a potential-outcomes system and a binary Balke--Pearl system on it, the average treatment effect is the expectation, under the system's probability measure, of the real-valued potential outcome under treatment minus that under control.
Definition (Lean source)
For a potential-outcomes system, a binary Balke--Pearl system on it, an outcome value, a treatment value, and an instrument value, the conditional cell probability is the probability that the factual outcome and treatment equal the specified values conditional on the factual instrument equaling the specified instrument value.
Definition (Lean source)
10 supporting declarations (lemmas, instances)
-
measurable_YofDlemma — The outcome under a fixed treatment value is measurable.hypothesesconclusionMeasurable (S.YofD d)Proof (Lean source)
@[fun_prop] lemma measurable_YofD (d : Bool) : Measurable (S.YofD d) := S.yVar.measurable_cfUnder S.dVar d -
measurable_YofZDlemma — The outcome under fixed instrument and treatment values is measurable.hypothesesconclusionMeasurable (S.YofZD z d)Proof (Lean source)
@[fun_prop] lemma measurable_YofZD (z d : Bool) : Measurable (S.YofZD z d) := S.yVar.measurable_cf _ -
measurable_factualZlemma — The factual instrument is measurable.Proof (Lean source)
@[fun_prop] lemma measurable_factualZ : Measurable S.factualZ := S.zVar.measurable_factual -
measurable_factualDlemma — The factual treatment is measurable.Proof (Lean source)
@[fun_prop] lemma measurable_factualD : Measurable S.factualD := S.dVar.measurable_factual -
measurable_factualYlemma — The factual outcome is measurable.Proof (Lean source)
@[fun_prop] lemma measurable_factualY : Measurable S.factualY := S.yVar.measurable_factual -
measurableSet_zEventlemma — The factual instrument event is measurable.hypothesesconclusionMeasurableSet (S.zEvent z)Proof (Lean source)
lemma measurableSet_zEvent (z : Bool) : MeasurableSet (S.zEvent z) := S.zVar.measurableSet_event _ (measurableSet_singleton _) -
measurableSet_dEventlemma — The factual treatment event is measurable.hypothesesconclusionMeasurableSet (S.dEvent d)Proof (Lean source)
lemma measurableSet_dEvent (d : Bool) : MeasurableSet (S.dEvent d) := S.dVar.measurableSet_event _ (measurableSet_singleton _) -
measurableSet_yEventlemma — The factual outcome event is measurable.hypothesesconclusionMeasurableSet (S.yEvent y)Proof (Lean source)
lemma measurableSet_yEvent (y : Bool) : MeasurableSet (S.yEvent y) := S.yVar.measurableSet_event _ (measurableSet_singleton _) -
measurable_boolToReallemma — The Boolean-to-real embedding is measurable.conclusionMeasurable (boolToReal)Proof (Lean source)
@[fun_prop] lemma measurable_boolToReal : Measurable (boolToReal) := by apply measurable_of_finite -
measurable_YofD_reallemma — The real-valued potential outcome under a fixed treatment is measurable.hypothesesconclusionMeasurable (S.YofD_real d)Proof (Lean source)
@[fun_prop] lemma measurable_YofD_real (d : Bool) : Measurable (S.YofD_real d) := measurable_boolToReal.comp (S.measurable_YofD d)
Assumptions 5 core · 2 supporting This file collects the structural assumptions for Balke-Pearl partial identification with a binary instrument, including the IV-specific consistency equalities, exclusion, instrument exogeneity, and positive instrument p ★ posZ_toReal_pos
Balke-Pearl Assumptions
This file collects the structural assumptions for Balke-Pearl partial identification with a binary instrument, including the IV-specific consistency equalities, exclusion, instrument exogeneity, and positive instrument probabilities. It also packages the counterfactual variables used by the exogeneity condition.
For a potential-outcome system and its Balke--Pearl observational system, and a binary instrument value, the treatment potential-outcome variable under that instrument value is the factual treatment variable evaluated in the intervention that fixes the instrument at that value.
Definition (Lean source)
For a potential-outcome system and its Balke--Pearl observational system, and a binary treatment value, the outcome potential-outcome variable under that treatment value is the factual outcome variable evaluated in the intervention that fixes treatment at that value.
Definition (Lean source)
For a potential-outcome system and its Balke--Pearl observational system, the counterfactual bundle collects, in order, treatment under instrument values zero and one and outcome under treatment values zero and one.
Definition (Lean source)
Balke-Pearl IV assumptions — def:po-iv-balke-pearl-assumptions.
Definition (Lean source)
Treatment consistency on instrument cells: on {Z=z}, factual D equals D(z).
Outcome consistency on treatment cells: on {D=d}, factual Y equals Y(d).
Instrument exogeneity: Z ⊥ (D(0),D(1),Y(0),Y(1)).
Under the Balke-Pearl IV base assumptions — IV-specific consistency of treatment and outcome on their respective cells, the exclusion restriction, instrument exogeneity, and positive instrument probability, the real-valued probability of each instrument cell z is strictly positive.
Formal statement
Proof (Lean source)
2 supporting declarations (lemmas, instances)
-
posZ_ne_zerolemma — Positive instrument probabilities are nonzero.hypothesesconclusionP.μ (S.zVar.event z) ≠ 0Proof (Lean source)
lemma posZ_ne_zero (hA : S.BaseAssumptions) (z : Bool) : P.μ (S.zVar.event z) ≠ 0 := ne_of_gt (hA.posZ z) -
posZ_ne_toplemma — Instrument-cell probabilities are finite.Proof (Lean source)
lemma posZ_ne_top (_ : S.BaseAssumptions) (z : Bool) : P.μ (S.zVar.event z) ≠ ⊤ := ne_of_lt (lt_of_le_of_lt prob_le_one (by norm_num))
LatentTable 5 core · 4 supporting This file defines the 16-cell latent type table for Balke-Pearl bounds and relates it to the average treatment effect and observed conditional cell probabilities. ★ ATE_eq_sum_latent
Balke-Pearl Latent Table
This file defines the 16-cell latent type table for Balke-Pearl bounds and relates it to the average treatment effect and observed conditional cell probabilities. The latent cells partition the population by the two treatment potential outcomes and the two outcome potential outcomes.
For a binary instrument value and two binary treatment potential outcomes, respectively under instrument values zero and one, the selected treatment potential outcome is the first when the instrument value is zero and the second when it is one.
For a binary treatment value and two binary outcome potential outcomes, respectively under treatment values zero and one, the selected outcome potential outcome is the first when treatment is zero and the second when it is one.
For a potential-outcome system and its Balke--Pearl observational system and binary values for treatment under instrument zero and one and outcome under treatment zero and one, the latent-type event is the set of sample points at which all four corresponding potential outcomes equal those values.
For a potential-outcome system and its Balke--Pearl observational system and binary values for treatment under instrument zero and one and outcome under treatment zero and one, the latent-type probability is the real-valued probability of the corresponding latent-type event.
Definition (Lean source)
The average treatment effect equals the probability-weighted sum, over the sixteen latent response types, of each type's treatment effect.
Formal statement
Proof (Lean source)
4 supporting declarations (lemmas, instances)
-
measurableSet_latentSetlemma — Each latent type event is measurable.hypothesesconclusionMeasurableSet (S.latentSet d0 d1 y0 y1)Proof (Lean source)
lemma measurableSet_latentSet (d0 d1 y0 y1 : Bool) : MeasurableSet (S.latentSet d0 d1 y0 y1) := by show MeasurableSet ({a | S.DofZ false a = d0} ∩ ({a | S.DofZ true a = d1} ∩ ({a | S.YofD false a = y0} ∩ {a | S.YofD true a = y1}))) refine MeasurableSet.inter ?_ (MeasurableSet.inter ?_ (MeasurableSet.inter ?_ ?_)) · exact S.measurable_DofZ false (measurableSet_singleton d0) · exact S.measurable_DofZ true (measurableSet_singleton d1) · exact S.measurable_YofD false (measurableSet_singleton y0) · exact S.measurable_YofD true (measurableSet_singleton y1) -
latentProb_nonneglemma — Latent type probabilities are nonnegative.hypothesesconclusion0 ≤ S.latentProb d0 d1 y0 y1Proof (Lean source)
lemma latentProb_nonneg (d0 d1 y0 y1 : Bool) : 0 ≤ S.latentProb d0 d1 y0 y1 := ENNReal.toReal_nonneg -
latentProb_sum_eq_onelemma — The 16 latent sets partition Ω, so their probabilities sum to 1.hypothesesProof (Lean source)
lemma latentProb_sum_eq_one : ∑ d0 : Bool, ∑ d1 : Bool, ∑ y0 : Bool, ∑ y1 : Bool, S.latentProb d0 d1 y0 y1 = 1 := by -- Work with flat index type. set f : Bool × Bool × Bool × Bool → Set P.Ω := fun i => S.latentSet i.1 i.2.1 i.2.2.1 i.2.2.2 have hmeas : ∀ i : Bool × Bool × Bool × Bool, MeasurableSet (f i) := fun ⟨d0, d1, y0, y1⟩ => S.measurableSet_latentSet d0 d1 y0 y1 have hdisj : Pairwise (onFun Disjoint f) := by intro ⟨d0, d1, y0, y1⟩ ⟨d0', d1', y0', y1'⟩ hne apply S.latentSet_disjoint intro h; exact absurd h hne have hcov : ⋃ i : Bool × Bool × Bool × Bool, f i = univ := S.latentSet_iUnion_prod_eq_univ -- Sum of ENNReal measures = 1. have hENNsum : ∑ i : Bool × Bool × Bool × Bool, P.μ (f i) = 1 := by have h1 := measure_iUnion (μ := P.μ) hdisj hmeas rw [hcov, measure_univ] at h1 rw [tsum_fintype] at h1 exact h1.symm -- Take .toReal of hENNsum using additivity. have hne_top : ∀ i : Bool × Bool × Bool × Bool, P.μ (f i) ≠ ⊤ := fun i => measure_ne_top _ _ have hreal : ∑ i : Bool × Bool × Bool × Bool, (P.μ (f i)).toReal = 1 := by have := congr_arg toReal hENNsum rw [ENNReal.toReal_sum (fun i _ => hne_top i)] at this simpa using this -- The nested sum equals the flat sum (latentProb = (P.μ (f ·)).toReal). have hflat : ∑ d0 : Bool, ∑ d1 : Bool, ∑ y0 : Bool, ∑ y1 : Bool, S.latentProb d0 d1 y0 y1 = ∑ i : Bool × Bool × Bool × Bool, (P.μ (f i)).toReal := by simp only [latentProb, f, ← Finset.sum_product', Finset.univ_product_univ] rw [hflat, hreal] -
cellProb_eq_sum_latenttheorem — Each observed conditional cell probability equals the sum of compatible latent type probabilities.hypothesesProof (Lean source)
theorem cellProb_eq_sum_latent (hA : S.BaseAssumptions) (y d z : Bool) : S.cellProb y d z = ∑ d0 : Bool, ∑ d1 : Bool, ∑ y0 : Bool, ∑ y1 : Bool, (if dArm z d0 d1 = d ∧ yArm d y0 y1 = y then 1 else 0) * S.latentProb d0 d1 y0 y1 := by -- Abbreviations. set E : Set P.Ω := S.cfCellEvent z d y with hE set T : Set (Bool × Bool × Bool × Bool) := {p | dArm z p.1 p.2.1 = d ∧ yArm d p.2.2.1 p.2.2.2 = y} with hT have hEpre : E = S.cfTuple ⁻¹' T := S.cfCellEvent_eq_preimage z d y have hT_meas : MeasurableSet T := (Set.toFinite T).measurableSet have hE_meas : MeasurableSet E := S.measurableSet_cfCellEvent z d y -- Step 1: consistency gives the set equality on numerator. have h1 : S.zEvent z ∩ S.yEvent y ∩ S.dEvent d = S.zEvent z ∩ E := S.zEvent_inter_cell_eq hA z d y -- Step 2: exogeneity factorization. have hindep : IndepFun S.factualZ S.cfTuple P.μ := S.indepFun_factualZ_cfTuple hA have hZeqEv : S.zEvent z = S.factualZ ⁻¹' {z} := rfl have h2 : P.μ (S.zEvent z ∩ E) = P.μ (S.zEvent z) * P.μ E := by rw [hEpre, hZeqEv] exact hindep.measure_inter_preimage_eq_mul {z} T (measurableSet_singleton _) hT_meas -- Step 3: decompose μ(E) over 16 latent cells. set fset : Bool × Bool × Bool × Bool → Set P.Ω := fun i => S.latentSet i.1 i.2.1 i.2.2.1 i.2.2.2 with hfset have hmeas : ∀ i, MeasurableSet (fset i) := fun ⟨d0, d1, y0, y1⟩ => S.measurableSet_latentSet d0 d1 y0 y1 have hdisj : Pairwise (onFun Disjoint fset) := by intro ⟨d0, d1, y0, y1⟩ ⟨d0', d1', y0', y1'⟩ hne apply S.latentSet_disjoint; intro h; exact absurd h hne have hcov : ⋃ i, fset i = univ := S.latentSet_iUnion_prod_eq_univ -- Express μ(E) as a sum over latent cells. have hE_decomp : P.μ E = ∑ i : Bool × Bool × Bool × Bool, (if dArm z i.1 i.2.1 = d ∧ yArm d i.2.2.1 i.2.2.2 = y then 1 else 0) * P.μ (fset i) := by -- E = E ∩ univ = E ∩ ⋃ fset = ⋃ (E ∩ fset i), and disjoint. have hE_union : E = ⋃ i, E ∩ fset i := by rw [← Set.inter_iUnion, hcov, Set.inter_univ] have hdisj' : Pairwise (onFun Disjoint (fun i => E ∩ fset i)) := by intro i j hij exact (hdisj hij).inter_left' E |>.inter_right' E have hmeas' : ∀ i, MeasurableSet (E ∩ fset i) := fun i => hE_meas.inter (hmeas i) have hμsum : P.μ E = ∑ i, P.μ (E ∩ fset i) := by conv_lhs => rw [hE_union] rw [measure_iUnion hdisj' hmeas', tsum_fintype] -- For each i, E ∩ fset i = fset i if compatible, else ∅. have hcell : ∀ i, P.μ (E ∩ fset i) = (if dArm z i.1 i.2.1 = d ∧ yArm d i.2.2.1 i.2.2.2 = y then 1 else 0) * P.μ (fset i) := by rintro ⟨d0, d1, y0, y1⟩ by_cases hcompat : dArm z d0 d1 = d ∧ yArm d y0 y1 = y · -- E ⊇ fset (d0,d1,y0,y1): on latentSet, cfTuple = (d0,d1,y0,y1) and that point ∈ T. have hsub : fset (d0, d1, y0, y1) ⊆ E := by intro ω hω rw [hEpre] change S.cfTuple ω ∈ T rw [S.cfTuple_on_latentSet d0 d1 y0 y1 hω] exact hcompat rw [Set.inter_eq_right.mpr hsub] simp [hcompat] · -- Disjoint: cfTuple = (d0,d1,y0,y1) ∉ T on latentSet. have hdisjE : Disjoint E (fset (d0, d1, y0, y1)) := by rw [Set.disjoint_right] intro ω hω hωE rw [hEpre] at hωE have : S.cfTuple ω ∈ T := hωE rw [S.cfTuple_on_latentSet d0 d1 y0 y1 hω] at this exact hcompat this rw [Set.disjoint_iff_inter_eq_empty.mp hdisjE] simp [hcompat] rw [hμsum] exact Finset.sum_congr rfl (fun i _ => hcell i) -- Combine: numerator = μ(Z=z) * μ(E). have hnum : P.μ (S.zEvent z ∩ S.yEvent y ∩ S.dEvent d) = P.μ (S.zEvent z) * P.μ E := by rw [h1, h2] -- Now go to ℝ via .toReal. unfold cellProb rw [hnum, ENNReal.toReal_mul] rw [hE_decomp] -- Convert sum-toReal and divide. have hpZne : (P.μ (S.zEvent z)).toReal ≠ 0 := hA.posZ_toReal_pos z |>.ne' rw [mul_div_cancel_left₀ _ hpZne] -- Now show: (∑ i, indicator * μ(fset i)).toReal = ∑ ... * latentProb. have hne_top : ∀ i : Bool × Bool × Bool × Bool, (if dArm z i.1 i.2.1 = d ∧ yArm d i.2.2.1 i.2.2.2 = y then (1 : ENNReal) else 0) * P.μ (fset i) ≠ ⊤ := by intro i by_cases h : dArm z i.1 i.2.1 = d ∧ yArm d i.2.2.1 i.2.2.2 = y · simp [h, measure_ne_top] · simp [h] rw [ENNReal.toReal_sum (fun i _ => hne_top i)] -- Flatten Bool × Bool × Bool × Bool sum into nested Bool sums. simp_rw [Fintype.sum_prod_type] refine Finset.sum_congr rfl (fun d0 _ => ?_) refine Finset.sum_congr rfl (fun d1 _ => ?_) refine Finset.sum_congr rfl (fun y0 _ => ?_) refine Finset.sum_congr rfl (fun y1 _ => ?_) simp only [fset, latentProb] by_cases hcompat : dArm z d0 d1 = d ∧ yArm d y0 y1 = y · simp [hcompat] · simp [hcompat]
Main 4 core · 2 supporting This file assembles the finite latent-type linear program for Balke-Pearl IV bounds. ★ ATE_mem_BPIdentifiedInterval
Balke-Pearl latent-table necessity theorem
This file assembles the finite latent-type linear program for Balke-Pearl IV bounds. It defines feasibility, the ATE objective, the identified objective range, proves that the realized latent table is feasible, and shows that the true ATE belongs to that range.
Balke–Pearl latent-table feasibility. A latent response-type table π — the joint distribution over the instrument's and treatment's potential values together with the outcome's potential values — is feasible for a Balke–Pearl IV system under a given assumption bundle when every table entry is nonnegative, the entries sum to one, and aggregating the table over the response types compatible with each observed instrument-treatment-outcome cell reproduces the observed conditional cell probability.
Definition (Lean source)
For a table of real weights indexed by the four binary latent response values, the Balke--Pearl linear-program objective is the sum, over all latent response types, of that type's weight times its binary outcome response under treatment minus its binary outcome response under control.
For a potential-outcomes system, a binary Balke--Pearl system on it, and proof that the system satisfies the Balke--Pearl base assumptions, the sharp identified interval for the average treatment effect is the set of values of the Balke--Pearl linear-program objective over all feasible latent response-type tables.
Definition (Lean source)
Necessity. Under the Balke-Pearl IV base assumptions, the true average treatment effect lies in the Balke-Pearl identified interval.
Formal statement
Proof (Lean source)
2 supporting declarations (lemmas, instances)
-
latentProb_feasibletheorem — The actual latent type distribution latentProb is feasible.hypothesesconclusionBPFeasible S hA S.latentProb where nonnegProof (Lean source)
theorem latentProb_feasible (hA : S.BaseAssumptions) : BPFeasible S hA S.latentProb where nonneg := fun d0 d1 y0 y1 => S.latentProb_nonneg d0 d1 y0 y1 sum_one := S.latentProb_sum_eq_one marginal := fun y d z => S.cellProb_eq_sum_latent hA y d z -
ATE_eq_BPObjectivetheorem — The system's ATE equals the Balke–Pearl objective evaluated at its realized latent table.Proof (Lean source)
theorem ATE_eq_BPObjective : S.ATE = BPObjective S.latentProb := by unfold BPObjective exact S.ATE_eq_sum_latent
ClosedForm 5 core · 5 supporting This file gives the explicit Balke-Pearl formulas for the endpoints of the identified interval for the average treatment effect under a binary instrument, as a maximum and a minimum of eight affine functions of the obser ★ ATE_mem_Icc_bpLower_bpUpper
Balke-Pearl bounds in closed form
This file gives the explicit Balke-Pearl formulas for the endpoints of the identified interval for the average treatment effect under a binary instrument, as a maximum and a minimum of eight affine functions of the observed cell probabilities, and proves that they bound the true effect.
For a potential-outcome system and its Balke--Pearl observational system, and one of the eight indices, the corresponding affine lower-bound expression is calculated from the observed outcome--treatment cell probabilities by naming those probabilities and applying the appropriate first, second, third, fourth, fifth, sixth, seventh, or eighth displayed formula.
Definition (Lean source)
For a potential-outcome system and its Balke--Pearl observational system, and one of the eight indices, the corresponding affine upper-bound expression is calculated from the observed outcome--treatment cell probabilities by naming those probabilities and applying the appropriate first, second, third, fourth, fifth, sixth, seventh, or eighth displayed formula.
Definition (Lean source)
For a potential-outcome system and its Balke--Pearl observational system, the closed-form lower endpoint is the largest of its eight affine lower-bound expressions.
Definition (Lean source)
For a potential-outcome system and its Balke--Pearl observational system, the closed-form upper endpoint is the smallest of its eight affine upper-bound expressions.
Definition (Lean source)
The Balke-Pearl bound in closed form. Under the Balke-Pearl IV base assumptions, the true average treatment effect lies between the largest of eight closed-form lower expressions and the smallest of eight closed-form upper expressions, both computable directly from the observed cell probabilities.
Formal statement
Proof (Lean source)
5 supporting declarations (lemmas, instances)
-
bpLowerTerm_le_BPObjectivetheorem — Every lower expression bounds the objective from below on feasible tables.hypothesesconclusionS.bpLowerTerm i ≤ BPObjective πProof (Lean source)
theorem bpLowerTerm_le_BPObjective (hA : S.BaseAssumptions) {π : Bool → Bool → Bool → Bool → ℝ} (hπ : BPFeasible S hA π) (i : Fin 8) : S.bpLowerTerm i ≤ BPObjective π := by have hs := hπ.sum_one have hn := hπ.nonneg have hm := hπ.marginal have e000 := hm false false false have e100 := hm true false false have e010 := hm false true false have e110 := hm true true false have e001 := hm false false true have e101 := hm true false true have e011 := hm false true true have e111 := hm true true true simp only [Fintype.sum_bool, dArm, yArm] at hs e000 e100 e010 e110 e001 e101 e011 e111 norm_num at hs e000 e100 e010 e110 e001 e101 e011 e111 fin_cases i <;> simp only [bpLowerTerm, BPObjective, Fintype.sum_bool, boolToReal] <;> simp only [e000, e100, e010, e110, e001, e101, e011, e111] <;> linarith [hn false false false false, hn false false false true, hn false false true false, hn false false true true, hn false true false false, hn false true false true, hn false true true false, hn false true true true, hn true false false false, hn true false false true, hn true false true false, hn true false true true, hn true true false false, hn true true false true, hn true true true false, hn true true true true] -
BPObjective_le_bpUpperTermtheorem — Every upper expression bounds the objective from above on feasible tables.hypothesesconclusionBPObjective π ≤ S.bpUpperTerm iProof (Lean source)
theorem BPObjective_le_bpUpperTerm (hA : S.BaseAssumptions) {π : Bool → Bool → Bool → Bool → ℝ} (hπ : BPFeasible S hA π) (i : Fin 8) : BPObjective π ≤ S.bpUpperTerm i := by have hs := hπ.sum_one have hn := hπ.nonneg have hm := hπ.marginal have e000 := hm false false false have e100 := hm true false false have e010 := hm false true false have e110 := hm true true false have e001 := hm false false true have e101 := hm true false true have e011 := hm false true true have e111 := hm true true true simp only [Fintype.sum_bool, dArm, yArm] at hs e000 e100 e010 e110 e001 e101 e011 e111 norm_num at hs e000 e100 e010 e110 e001 e101 e011 e111 fin_cases i <;> simp only [bpUpperTerm, BPObjective, Fintype.sum_bool, boolToReal] <;> simp only [e000, e100, e010, e110, e001, e101, e011, e111] <;> linarith [hn false false false false, hn false false false true, hn false false true false, hn false false true true, hn false true false false, hn false true false true, hn false true true false, hn false true true true, hn true false false false, hn true false false true, hn true false true false, hn true false true true, hn true true false false, hn true true false true, hn true true true false, hn true true true true] -
bpLower_le_BPObjectivetheorem — The closed-form lower endpoint bounds the objective on feasible tables.Proof (Lean source)
theorem bpLower_le_BPObjective (hA : S.BaseAssumptions) {π : Bool → Bool → Bool → Bool → ℝ} (hπ : BPFeasible S hA π) : S.bpLower ≤ BPObjective π := Finset.sup'_le _ _ (fun i _ => S.bpLowerTerm_le_BPObjective hA hπ i) -
BPObjective_le_bpUppertheorem — The closed-form upper endpoint bounds the objective on feasible tables.Proof (Lean source)
theorem BPObjective_le_bpUpper (hA : S.BaseAssumptions) {π : Bool → Bool → Bool → Bool → ℝ} (hπ : BPFeasible S hA π) : BPObjective π ≤ S.bpUpper := Finset.le_inf' _ _ (fun i _ => S.BPObjective_le_bpUpperTerm hA hπ i) -
BPIdentifiedInterval_subset_Icctheorem — The identified interval is contained in the closed-form interval.hypothesesconclusionS.BPIdentifiedInterval hA ⊆ Icc S.bpLower S.bpUpperProof (Lean source)
theorem BPIdentifiedInterval_subset_Icc (hA : S.BaseAssumptions) : S.BPIdentifiedInterval hA ⊆ Icc S.bpLower S.bpUpper := PartialID.identifiedSet_subset_Icc (fun _ h => S.bpLower_le_BPObjective hA h) (fun _ h => S.BPObjective_le_bpUpper hA h)
ClosedFormAttainment 3 core · 0 supporting The Balke–Pearl closed-form bounds on the average treatment effect with a binary instrument, treatment and outcome are exact: the largest of the eight lower expressions equals the infimum, and the smallest of the eight u ★ csInf_BPIdentifiedInterval_eq_bpLower★ csSup_BPIdentifiedInterval_eq_bpUpper★ bpLower_bpUpper_eq_csInf_csSup
Attainment of the Balke–Pearl closed-form endpoints
The Balke–Pearl closed-form bounds on the average treatment effect with a binary instrument,
treatment and outcome are exact: the largest of the eight lower expressions equals the infimum,
and the smallest of the eight upper expressions equals the supremum, of the linear-program
objective over all latent response-type tables compatible with the observed cell probabilities.
The proof combines validity of the closed form (every feasible table has objective between the
two endpoints) with explicit feasible tables attaining each endpoint. This is a statement about
the linear program; that every feasible table comes from an actual potential-outcome model is
the separate sharpness theorem balkePearl_sharp.
Main results
csInf_BPIdentifiedInterval_eq_bpLower— the infimum of the identified set isbpLower.csSup_BPIdentifiedInterval_eq_bpUpper— the supremum of the identified set isbpUpper.bpLower_bpUpper_eq_csInf_csSup— both equalities together, under the base assumptions.
The closed-form lower endpoint is exactly the LP minimum. Under the Balke-Pearl IV base assumptions, the infimum of the Balke-Pearl identified interval equals the closed-form lower bound bpLower.
Formal statement
Proof (Lean source)
The closed-form upper endpoint is exactly the LP maximum. Under the Balke-Pearl IV base assumptions, the supremum of the Balke-Pearl identified interval equals the closed-form upper bound bpUpper.
Formal statement
Proof (Lean source)
The Balke-Pearl closed form is sharp. Under the Balke-Pearl IV base assumptions, the interval [bpLower, bpUpper], computed from the observed cell probabilities alone, has both endpoints attained by observationally-equivalent latent tables — equivalently, bpLower is the infimum and bpUpper is the supremum of the Balke-Pearl identified interval. So no smaller interval contains every average treatment effect compatible with the data: the bound cannot be improved without further assumptions.
Formal statement
Proof (Lean source)
IntervalForm 1 core · 4 supporting This file restates the Balke-Pearl latent-table necessity result in the closed-interval vocabulary used by the partial-identification library. ★ ATE_mem_Icc_csInf_csSup
Balke-Pearl bounds in closed-interval form
This file restates the Balke-Pearl latent-table necessity result in the closed-interval vocabulary used by the partial-identification library. It proves boundedness of the linear-program objective and derives membership of the true ATE in the interval between the infimum and supremum of the feasible objective range.
Necessity, closed-interval form. Under the Balke-Pearl IV base assumptions, the true average treatment effect lies between the infimum and supremum of the Balke-Pearl identified interval — the LP minimum and maximum. This is ATE_mem_BPIdentifiedInterval rephrased through the engine bridge Causalean.PartialID.mem_Icc_csInf_csSup.
Formal statement
Proof (Lean source)
4 supporting declarations (lemmas, instances)
-
BPObjective_le_onelemma — Upper bound on the objective. For a feasible (nonneg, sum-one) table π, the LP objective ∑ (y1 - y0) · π is at most 1, since every contrast is ≤ 1 and π is a probability vector.Proof (Lean source)
lemma BPObjective_le_one {π : Bool → Bool → Bool → Bool → ℝ} (hnn : ∀ d0 d1 y0 y1, 0 ≤ π d0 d1 y0 y1) (hsum : ∑ d0 : Bool, ∑ d1 : Bool, ∑ y0 : Bool, ∑ y1 : Bool, π d0 d1 y0 y1 = 1) : BPObjective π ≤ 1 := by unfold BPObjective refine le_of_le_of_eq (Finset.sum_le_sum fun d0 _ => Finset.sum_le_sum fun d1 _ => Finset.sum_le_sum fun y0 _ => Finset.sum_le_sum fun y1 _ => ?_) hsum exact (mul_le_mul_of_nonneg_right (boolToReal_diff_mem_Icc y0 y1).2 (hnn d0 d1 y0 y1)).trans_eq (one_mul _) -
neg_one_le_BPObjectivelemma — Lower bound on the objective. Symmetrically, -1 ≤ BPObjective π.Proof (Lean source)
lemma neg_one_le_BPObjective {π : Bool → Bool → Bool → Bool → ℝ} (hnn : ∀ d0 d1 y0 y1, 0 ≤ π d0 d1 y0 y1) (hsum : ∑ d0 : Bool, ∑ d1 : Bool, ∑ y0 : Bool, ∑ y1 : Bool, π d0 d1 y0 y1 = 1) : -1 ≤ BPObjective π := by unfold BPObjective refine le_of_eq_of_le ?_ (Finset.sum_le_sum fun d0 _ => Finset.sum_le_sum fun d1 _ => Finset.sum_le_sum fun y0 _ => Finset.sum_le_sum fun y1 _ => (neg_one_mul (π d0 d1 y0 y1)).symm.trans_le (mul_le_mul_of_nonneg_right (boolToReal_diff_mem_Icc y0 y1).1 (hnn d0 d1 y0 y1))) -- Remaining goal: `-1 = ∑∑∑∑ (-(π …))`. Pull the negation out and use `hsum`. have hneg : (∑ d0 : Bool, ∑ d1 : Bool, ∑ y0 : Bool, ∑ y1 : Bool, -(π d0 d1 y0 y1)) = -(∑ d0 : Bool, ∑ d1 : Bool, ∑ y0 : Bool, ∑ y1 : Bool, π d0 d1 y0 y1) := by simp only [Finset.sum_neg_distrib] rw [hneg, hsum] -
bddBelow_BPIdentifiedIntervallemma — The Balke-Pearl identified interval is bounded below (by -1).hypothesesconclusionBddBelow (S.BPIdentifiedInterval hA)Proof (Lean source)
lemma bddBelow_BPIdentifiedInterval (hA : S.BaseAssumptions) : BddBelow (S.BPIdentifiedInterval hA) := by refine ⟨-1, ?_⟩ rintro _ ⟨⟨π, hπ⟩, rfl⟩ exact neg_one_le_BPObjective hπ.nonneg hπ.sum_one -
bddAbove_BPIdentifiedIntervallemma — The Balke-Pearl identified interval is bounded above (by 1).hypothesesconclusionBddAbove (S.BPIdentifiedInterval hA)Proof (Lean source)
lemma bddAbove_BPIdentifiedInterval (hA : S.BaseAssumptions) : BddAbove (S.BPIdentifiedInterval hA) := by refine ⟨1, ?_⟩ rintro _ ⟨⟨π, hπ⟩, rfl⟩ exact BPObjective_le_one hπ.nonneg hπ.sum_one