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 — ATE = BPObjective applied to the realized latent table.hypothesesconclusionS.ATE = BPObjective S.latentProbProof (Lean source)
theorem ATE_eq_BPObjective (_hA : S.BaseAssumptions) : 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.identifiedInterval_subset_Icc (fun _ h => S.bpLower_le_BPObjective hA h) (fun _ h => S.BPObjective_le_bpUpper hA h)
ClosedFormAttainment 3 core · 0 supporting Attainment of the Balke-Pearl closed-form endpoints ★ csInf_BPIdentifiedInterval_eq_bpLower★ csSup_BPIdentifiedInterval_eq_bpUpper★ bpLower_bpUpper_eq_csInf_csSup
Attainment of the Balke-Pearl closed-form endpoints
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
Sharp 13 core · 32 supporting This file constructs the canonical binary-IV potential-outcome model that realizes any feasible latent table in the Balke-Pearl linear program. ★ balkePearl_sharp★ balkePearl_sharp_of_mem
Balke-Pearl Sharpness Construction
This file constructs the canonical binary-IV potential-outcome model that
realizes any feasible latent table in the Balke-Pearl linear program. The model
uses a binary instrument marginal from the original system and an independent
four-type latent table, then verifies consistency, exclusion, exogeneity,
matching observed cell probabilities, and realization of the linear-program
objective as the average treatment effect. The main public results are
balkePearl_sharp, which realizes any feasible table, and
balkePearl_sharp_of_mem, which realizes every point of the Balke-Pearl
identified interval.
The canonical sample space consists of one observed binary instrument value together with four binary latent response values: treatment under each instrument value and outcome under each treatment value.
The canonical variable-index set has exactly three elements, representing respectively the instrument, treatment, and outcome.
Definition (Lean source)
The canonical measurement-scale assignment assigns the binary scale to each of the three canonical variables.
For a binary instrument value and a canonical sample-space point, the latent treatment response is that point's treatment response under the specified instrument value.
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.
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)
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)
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.
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.
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)
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)
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
Proof (Lean source)
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
Proof (Lean source)
32 supporting declarations (lemmas, instances)
-
measurable_evallemma — The canonical evaluator is measurable under every intervention regime.Proof (Lean source)
@[fun_prop] lemma measurable_eval (r : Regime SV SX) : Measurable (eval r) := by exact measurable_of_finite _ -
eval_zerolemma — The Z-coordinate eval r ω 0: assignment if intervened on, else ω.1.hypothesesconclusioneval r ω ⟨0, by decide⟩= (if h : (⟨0, by decide⟩ : SV) ∈ r.target then r.assign _ h else ω.1) -
eval_one_rawlemma — The D-coordinate (raw).hypotheses -
eval_two_rawlemma — The Y-coordinate (raw).hypothesesProof (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 -
eval_onelemma — The D-coordinate folded via eval_zero.hypotheses -
eval_twolemma — The Y-coordinate folded via eval_one.hypotheses -
zMeasure_univlemma — zMeasure S has total mass 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] -
instIsProbZMeasureinstance — 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.parametersinstancegiven by⟨zMeasure_univ S⟩ -
piMeasure_univ_of_feasiblelemma — piMeasure π has total mass 1 when π has nonneg entries summing to 1.hypotheseshπ_nn :∀ d0 d1 y0 y1, 0 ≤ π d0 d1 y0 y1Proof (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 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 sum_nonneg fun y0 _ => 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 sum_nonneg fun d1 _ => sum_nonneg fun y0 _ => sum_nonneg fun y1 _ => hπ_nn _ _ _ _ rw [h4, hπ_sum] simp -
instIsProbPiMeasurelemma — A nonnegative latent table that sums to one induces a probability measure.hypotheseshπ_nn :∀ d0 d1 y0 y1, 0 ≤ π d0 d1 y0 y1conclusion -
instIsProbCanonicalMeasureinstance — 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. -
canonical_consistencylemma — Consistency for the canonical PO system.hypotheseshπ_sum :shared∑ d0, ∑ d1, ∑ y0, ∑ y1, π d0 d1 y0 y1 = 1conclusion(P' S π hπ_nn hπ_sum).ConsistencyProof (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 · -- Composition. 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 -
canonical_factualZlemma — S'.factualZ ω = ω.1.hypotheseshπ_sum :shared∑ d0, ∑ d1, ∑ y0, ∑ y1, π d0 d1 y0 y1 = 1ω :conclusion(S' S π hπ_nn hπ_sum).factualZ ω = ω.1Proof (Lean source)
lemma canonical_factualZ (ω : SOmega) : (S' S π hπ_nn hπ_sum).factualZ ω = ω.1 := by change (eval Regime.empty ω ⟨0, by decide⟩) = ω.1 rw [eval_zero] have : (⟨0, by decide⟩ : SV) ∉ (Regime.empty : Regime SV SX).target := by rw [Regime.empty_target]; exact notMem_empty _ rw [dif_neg this] -
canonical_factualDlemma — S'.factualD ω = D(ω.1).hypotheseshπ_sum :shared∑ d0, ∑ d1, ∑ y0, ∑ y1, π d0 d1 y0 y1 = 1ω :conclusion(S' S π hπ_nn hπ_sum).factualD ω = dArmω ω.1 ωProof (Lean source)
lemma canonical_factualD (ω : SOmega) : (S' S π hπ_nn hπ_sum).factualD ω = dArmω ω.1 ω := by change (eval Regime.empty ω ⟨1, by decide⟩) = dArmω ω.1 ω rw [eval_one] have h1nin : (⟨1, by decide⟩ : SV) ∉ (Regime.empty : Regime SV SX).target := by rw [Regime.empty_target]; exact notMem_empty _ rw [dif_neg h1nin] have h0nin : (⟨0, by decide⟩ : SV) ∉ (Regime.empty : Regime SV SX).target := by rw [Regime.empty_target]; exact notMem_empty _ rw [eval_zero, dif_neg h0nin] -
canonical_factualYlemma — S'.factualY ω = Y(D(ω.1)).hypotheseshπ_sum :shared∑ d0, ∑ d1, ∑ y0, ∑ y1, π d0 d1 y0 y1 = 1ω :Proof (Lean source)
lemma canonical_factualY (ω : SOmega) : (S' S π hπ_nn hπ_sum).factualY ω = yArmω (dArmω ω.1 ω) ω := by change (eval Regime.empty ω ⟨2, by decide⟩) = yArmω (dArmω ω.1 ω) ω rw [eval_two] have h2nin : (⟨2, by decide⟩ : SV) ∉ (Regime.empty : Regime SV SX).target := by rw [Regime.empty_target]; exact Finset.notMem_empty _ rw [dif_neg h2nin] have h0nin : (⟨0, by decide⟩ : SV) ∉ (Regime.empty : Regime SV SX).target := by rw [Regime.empty_target]; exact Finset.notMem_empty _ have h1nin : (⟨1, by decide⟩ : SV) ∉ (Regime.empty : Regime SV SX).target := by rw [Regime.empty_target]; exact Finset.notMem_empty _ rw [eval_one, dif_neg h1nin, eval_zero, dif_neg h0nin] -
canonical_DofZlemma — S'.DofZ z ω = (POBalkePearlSystem.dArm) z ω.2.1 ω.2.2.1.hypotheseshπ_sum :shared∑ d0, ∑ d1, ∑ y0, ∑ y1, π d0 d1 y0 y1 = 1z :ω :conclusion(S' S π hπ_nn hπ_sum).DofZ z ω = POBalkePearlSystem.dArm z ω.2.1 ω.2.2.1Proof (Lean source)
lemma canonical_DofZ (z : Bool) (ω : SOmega) : (S' S π hπ_nn hπ_sum).DofZ z ω = POBalkePearlSystem.dArm z ω.2.1 ω.2.2.1 := by change (eval (Regime.single (X := SX) ⟨0, by decide⟩ z) ω ⟨1, by decide⟩) = _ rw [eval_one] have h1nin : (⟨1, by decide⟩ : SV) ∉ (Regime.single (X := SX) (⟨0, by decide⟩ : SV) z).target := by rw [Regime.single_target]; intro h exact absurd (Finset.mem_singleton.mp h) (by decide) have h0in : (⟨0, by decide⟩ : SV) ∈ (Regime.single (X := SX) (⟨0, by decide⟩ : SV) z).target := by rw [Regime.single_target]; exact mem_singleton_self _ rw [dif_neg h1nin, eval_zero, dif_pos h0in, Regime.single_assign_self] unfold dArmω POBalkePearlSystem.dArm cases z <;> rfl -
canonical_YofDlemma — S'.YofD d ω = (POBalkePearlSystem.yArm) d ω.2.2.2.1 ω.2.2.2.2.hypotheseshπ_sum :shared∑ d0, ∑ d1, ∑ y0, ∑ y1, π d0 d1 y0 y1 = 1d :ω :conclusion(S' S π hπ_nn hπ_sum).YofD d ω = POBalkePearlSystem.yArm d ω.2.2.2.1 ω.2.2.2.2Proof (Lean source)
lemma canonical_YofD (d : Bool) (ω : SOmega) : (S' S π hπ_nn hπ_sum).YofD d ω = POBalkePearlSystem.yArm d ω.2.2.2.1 ω.2.2.2.2 := by change (eval (Regime.single (X := SX) ⟨1, by decide⟩ d) ω ⟨2, by decide⟩) = _ rw [eval_two] have h2nin : (⟨2, by decide⟩ : SV) ∉ (Regime.single (X := SX) (⟨1, by decide⟩ : SV) d).target := by rw [Regime.single_target]; intro h exact absurd (Finset.mem_singleton.mp h) (by decide) have h1in : (⟨1, by decide⟩ : SV) ∈ (Regime.single (X := SX) (⟨1, by decide⟩ : SV) d).target := by rw [Regime.single_target]; exact mem_singleton_self _ rw [dif_neg h2nin, eval_one, dif_pos h1in, Regime.single_assign_self] unfold yArmω POBalkePearlSystem.yArm cases d <;> rfl -
canonical_YofZDlemma — S'.YofZD z d ω = (POBalkePearlSystem.yArm) d ω.2.2.2.1 ω.2.2.2.2.hypotheseshπ_sum :shared∑ d0, ∑ d1, ∑ y0, ∑ y1, π d0 d1 y0 y1 = 1z d :ω :conclusion(S' S π hπ_nn hπ_sum).YofZD z d ω = POBalkePearlSystem.yArm d ω.2.2.2.1 ω.2.2.2.2Proof (Lean source)
lemma canonical_YofZD (z d : Bool) (ω : SOmega) : (S' S π hπ_nn hπ_sum).YofZD z d ω = POBalkePearlSystem.yArm d ω.2.2.2.1 ω.2.2.2.2 := by -- Unfold YofZD to show eval at the regimeZD. have hZ_eq : (S' S π hπ_nn hπ_sum).Z = (⟨0, by decide⟩ : SV) := rfl have hD_eq : (S' S π hπ_nn hπ_sum).D = (⟨1, by decide⟩ : SV) := rfl have h2nin : (⟨2, by decide⟩ : SV) ∉ ((S' S π hπ_nn hπ_sum).regimeZD z d).target := by unfold POBalkePearlSystem.regimeZD rw [Regime.sqcup_target, Regime.single_target, Regime.single_target, hZ_eq, hD_eq] intro h rcases Finset.mem_union.mp h with h | h · exact absurd (Finset.mem_singleton.mp h) (by decide) · exact absurd (Finset.mem_singleton.mp h) (by decide) have h1in : (⟨1, by decide⟩ : SV) ∈ ((S' S π hπ_nn hπ_sum).regimeZD z d).target := by unfold POBalkePearlSystem.regimeZD rw [Regime.sqcup_target] refine mem_union_right _ ?_ rw [Regime.single_target, hD_eq] exact Finset.mem_singleton_self _ -- The assign for D is `d`. have h11 : (⟨1, by decide⟩ : SV) ∉ (Regime.single (X := SX) (⟨0, by decide⟩ : SV) z).target := by rw [Regime.single_target]; intro h exact absurd (Finset.mem_singleton.mp h) (by decide) have h12 : (⟨1, by decide⟩ : SV) ∈ (Regime.single (X := SX) (⟨1, by decide⟩ : SV) d).target := Finset.mem_singleton_self _ have hAssignD : ((S' S π hπ_nn hπ_sum).regimeZD z d).assign ⟨1, by decide⟩ h1in = d := by change ((Regime.single (X := SX) (⟨0, by decide⟩ : SV) z).sqcup (Regime.single (X := SX) (⟨1, by decide⟩ : SV) d) _).assign _ h1in = d rw [sqcup_assign_right _ _ _ _ h11 h12 h1in, Regime.single_assign_self] change (eval ((S' S π hπ_nn hπ_sum).regimeZD z d) ω ⟨2, by decide⟩) = _ rw [eval_two_of_not_mem _ _ h2nin, eval_one_of_mem _ _ h1in, hAssignD] unfold yArmω POBalkePearlSystem.yArm cases d <;> rfl -
canonical_exclusionlemma — Exclusion: Y(z,d) = Y(d) pointwise (and so a.e.).hypotheseshπ_sum :shared∑ d0, ∑ d1, ∑ y0, ∑ y1, π d0 d1 y0 y1 = 1z d :conclusion(S' S π hπ_nn hπ_sum).YofZD z d = (S' S π hπ_nn hπ_sum).YofD dProof (Lean source)
lemma canonical_exclusion (z d : Bool) : (S' S π hπ_nn hπ_sum).YofZD z d = (S' S π hπ_nn hπ_sum).YofD d := by funext ω exact (canonical_YofZD S π hπ_nn hπ_sum z d ω).trans (canonical_YofD S π hπ_nn hπ_sum d ω).symm -
canonical_zEventlemma — The Z-event in the canonical model is {ω | ω.1 = z}.hypotheseshπ_sum :shared∑ d0, ∑ d1, ∑ y0, ∑ y1, π d0 d1 y0 y1 = 1z :conclusion(S' S π hπ_nn hπ_sum).zEvent z = {ω : SOmega | ω.1 = z}Proof (Lean source)
lemma canonical_zEvent (z : Bool) : (S' S π hπ_nn hπ_sum).zEvent z = {ω : SOmega | ω.1 = z} := by ext ω change (S' S π hπ_nn hπ_sum).factualZ ω = z ↔ ω.1 = z exact of_eq (congrArg (fun t => t = z) (canonical_factualZ S π hπ_nn hπ_sum ω)) -
canonical_zEvent_measurelemma — μ' (S'.zEvent z) = P.μ (S.zEvent z).hypotheseshπ_sum :shared∑ d0, ∑ d1, ∑ y0, ∑ y1, π d0 d1 y0 y1 = 1z :conclusion(P' S π hπ_nn hπ_sum).μ ((S' S π hπ_nn hπ_sum).zEvent z) = P.μ (S.zEvent z)Proof (Lean source)
lemma canonical_zEvent_measure (z : Bool) : (P' S π hπ_nn hπ_sum).μ ((S' S π hπ_nn hπ_sum).zEvent z) = P.μ (S.zEvent z) := by rw [canonical_zEvent] change (canonicalMeasure S π) {ω : SOmega | ω.1 = z} = P.μ (S.zEvent z) unfold canonicalMeasure -- Use Measure.prod_apply for {ω | ω.1 = z} = {z} ×ˢ Set.univ. have hsetEq : {ω : SOmega | ω.1 = z} = {z} ×ˢ (Set.univ : Set (Bool × Bool × Bool × Bool)) := by ext ω; simp [Set.mem_prod, Set.mem_singleton_iff] letI : IsProbabilityMeasure (piMeasure π) := instIsProbPiMeasure hπ_nn hπ_sum rw [hsetEq, Measure.prod_prod] -- piMeasure univ = 1 rw [piMeasure_univ_of_feasible hπ_nn hπ_sum, mul_one] -- zMeasure {z} = P.μ (S.zEvent z) unfold zMeasure rw [Measure.coe_finset_sum] simp only [Finset.sum_apply, Measure.coe_smul, Pi.smul_apply, smul_eq_mul] -- ∑ z' : Bool, P.μ (S.zEvent z') * Measure.dirac z' {z} rw [Fintype.sum_bool] -- Cases on z. cases z · simp [Measure.dirac_apply' _ (MeasurableSet.singleton false)] · simp [Measure.dirac_apply' _ (MeasurableSet.singleton true)] -
canonical_posZlemma — Positive Z probability.hypotheseshπ_sum :shared∑ d0, ∑ d1, ∑ y0, ∑ y1, π d0 d1 y0 y1 = 1hA :S.BaseAssumptionsz :conclusion0 < (P' S π hπ_nn hπ_sum).μ ((S' S π hπ_nn hπ_sum).zVar.event z)Proof (Lean source)
lemma canonical_posZ (hA : S.BaseAssumptions) (z : Bool) : 0 < (P' S π hπ_nn hπ_sum).μ ((S' S π hπ_nn hπ_sum).zVar.event z) := by change 0 < (P' S π hπ_nn hπ_sum).μ ((S' S π hπ_nn hπ_sum).zEvent z) rw [canonical_zEvent_measure] exact hA.posZ z -
canonical_factualZ_eq_fstlemma — The factualZ on the canonical model factors through Prod.fst.hypotheseshπ_sum :shared∑ d0, ∑ d1, ∑ y0, ∑ y1, π d0 d1 y0 y1 = 1conclusion(S' S π hπ_nn hπ_sum).factualZ = fun ω : SOmega => ω.1Proof (Lean source)
lemma canonical_factualZ_eq_fst : (S' S π hπ_nn hπ_sum).factualZ = fun ω : SOmega => ω.1 := by funext ω; exact canonical_factualZ S π hπ_nn hπ_sum ω -
canonical_cfBundle_factors_through_sndlemma — The cfBundle's jointValue factors through Prod.snd: it depends only on the latent factor.hypotheseshπ_sum :shared∑ d0, ∑ d1, ∑ y0, ∑ y1, π d0 d1 y0 y1 = 1Proof (Lean source)
lemma canonical_cfBundle_factors_through_snd : ∃ g : (Bool × Bool × Bool × Bool) → (∀ i : Fin (S' S π hπ_nn hπ_sum).cfBundle.n, (S' S π hπ_nn hπ_sum).cfBundle.type i), Measurable g ∧ (S' S π hπ_nn hπ_sum).cfBundle.jointValue = (fun ω : SOmega => g ω.2) := by refine ⟨fun p i => ?_, ?_, ?_⟩ · -- The bundle has 4 components: (D(false), D(true), Y(false), Y(true)). -- D(z) ω = dArm z ω.2.1 ω.2.2.1; Y(d) ω = yArm d ω.2.2.2.1 ω.2.2.2.2. -- We can express the value purely from p = ω.2. refine i.cases (motive := fun i => (S' S π hπ_nn hπ_sum).cfBundle.type i) (POBalkePearlSystem.dArm false p.1 p.2.1) ?_ intro j refine j.cases (motive := fun j => (S' S π hπ_nn hπ_sum).cfBundle.type j.succ) (POBalkePearlSystem.dArm true p.1 p.2.1) ?_ intro k refine k.cases (motive := fun k => (S' S π hπ_nn hπ_sum).cfBundle.type k.succ.succ) (POBalkePearlSystem.yArm false p.2.2.1 p.2.2.2) ?_ intro l refine l.cases (motive := fun l => (S' S π hπ_nn hπ_sum).cfBundle.type l.succ.succ.succ) (POBalkePearlSystem.yArm true p.2.2.1 p.2.2.2) ?_ exact fun m => elim0 m · exact measurable_of_finite _ · funext ω i change (S' S π hπ_nn hπ_sum).cfBundle.jointValue ω i = _ -- Case split on i : Fin 4. fin_cases i · -- D(false) ω = dArm false ω.2.1 ω.2.2.1 exact (canonical_DofZ S π hπ_nn hπ_sum false ω).trans rfl · -- D(true) ω = dArm true ω.2.1 ω.2.2.1 exact (canonical_DofZ S π hπ_nn hπ_sum true ω).trans rfl · -- Y(false) ω = yArm false ω.2.2.2.1 ω.2.2.2.2 exact (canonical_YofD S π hπ_nn hπ_sum false ω).trans rfl · -- Y(true) ω = yArm true ω.2.2.2.1 ω.2.2.2.2 exact (canonical_YofD S π hπ_nn hπ_sum true ω).trans rfl -
canonical_exogeneitylemma — Exogeneity: Z ⊥ cfBundle under the canonical product measure.hypotheseshπ_sum :shared∑ d0, ∑ d1, ∑ y0, ∑ y1, π d0 d1 y0 y1 = 1Proof (Lean source)
lemma canonical_exogeneity : (P' S π hπ_nn hπ_sum).IndepCF (.ofFactual (S' S π hπ_nn hπ_sum).zVar) (S' S π hπ_nn hπ_sum).cfBundle (P' S π hπ_nn hπ_sum).μ := by -- Unfold IndepCF to IndepFun. unfold POSystem.IndepCF -- Pick X = id : Bool → Bool, Y = g (above). obtain ⟨g, hg_meas, hg⟩ := canonical_cfBundle_factors_through_snd S π hπ_nn hπ_sum -- factualZ = ω.1, cfBundle.jointValue = g ∘ ω.2. have hZeq : (RegimedVar.ofFactual (S' S π hπ_nn hπ_sum).zVar).value = fun ω : SOmega => ω.1 := by funext ω change (S' S π hπ_nn hπ_sum).zVar.factual ω = ω.1 exact canonical_factualZ S π hπ_nn hπ_sum ω rw [hZeq, hg] -- The product measure independence theorem. letI : IsProbabilityMeasure (piMeasure π) := instIsProbPiMeasure hπ_nn hπ_sum change IndepFun (fun ω : SOmega => ω.1) (fun ω : SOmega => g ω.2) ((zMeasure S).prod (piMeasure π)) exact ProbabilityTheory.indepFun_prod measurable_id hg_meas -
canonical_baseAssumptionslemma — Bundle the canonical model's BaseAssumptions.hypotheseshπ_sum :shared∑ d0, ∑ d1, ∑ y0, ∑ y1, π d0 d1 y0 y1 = 1hA :S.BaseAssumptionsconclusion(S' S π hπ_nn hπ_sum).BaseAssumptions where consistency_DProof (Lean source)
lemma canonical_baseAssumptions (hA : S.BaseAssumptions) : (S' S π hπ_nn hπ_sum).BaseAssumptions where consistency_D := by intro z ω hω rw [canonical_DofZ S π hπ_nn hπ_sum z ω, canonical_factualD S π hπ_nn hπ_sum ω] have hz : ω.1 = z := by have hset := canonical_zEvent S π hπ_nn hπ_sum z change ω ∈ (S' S π hπ_nn hπ_sum).zEvent z at hω rw [hset] at hω exact hω rw [hz] unfold dArmω POBalkePearlSystem.dArm rfl consistency_Y := by intro d ω hω rw [canonical_YofD S π hπ_nn hπ_sum d ω, canonical_factualY S π hπ_nn hπ_sum ω] have hd : dArmω ω.1 ω = d := by change (S' S π hπ_nn hπ_sum).factualD ω = d at hω rw [canonical_factualD S π hπ_nn hπ_sum ω] at hω exact hω rw [hd] unfold yArmω POBalkePearlSystem.yArm rfl exclusion := fun z d => by rw [canonical_exclusion] exogeneity := canonical_exogeneity S π hπ_nn hπ_sum posZ := canonical_posZ S π hπ_nn hπ_sum hA -
piMeasure_singletonlemma — piMeasure π {(d0, d1, y0, y1)} = ENNReal.ofReal (π d0 d1 y0 y1).hypothesesProof (Lean source)
lemma piMeasure_singleton (d0 d1 y0 y1 : Bool) : piMeasure π {(d0, d1, y0, y1)} = ofReal (π d0 d1 y0 y1) := by unfold piMeasure simp only [Measure.coe_finset_sum, Finset.sum_apply] have hSing : MeasurableSet ({(d0, d1, y0, y1)} : Set (Bool × Bool × Bool × Bool)) := MeasurableSet.singleton _ -- Compute each summand: it's the dirac measure scaled by π. -- The summand at (d0', d1', y0', y1') = ofReal(π d0' d1' y0' y1') if matches, else 0. have hsummand : ∀ (d0' d1' y0' y1' : Bool), ((ofReal (π d0' d1' y0' y1') • Measure.dirac (d0', d1', y0', y1') : Measure (Bool × Bool × Bool × Bool)) {(d0, d1, y0, y1)}) = if (d0', d1', y0', y1') = (d0, d1, y0, y1) then ofReal (π d0' d1' y0' y1') else 0 := by intros d0' d1' y0' y1' rw [Measure.smul_apply, Measure.dirac_apply' _ hSing, smul_eq_mul] by_cases h : (d0', d1', y0', y1') = (d0, d1, y0, y1) · rw [Set.indicator_of_mem (Set.mem_singleton_iff.mpr h), if_pos h, Pi.one_apply, mul_one] · rw [Set.indicator_of_notMem (by rw [Set.mem_singleton_iff]; exact h), if_neg h, mul_zero] simp_rw [hsummand] -- Now isolate the unique nonzero term. rw [Finset.sum_eq_single d0 (fun d0' _ hne => ?_) (fun h => absurd (Finset.mem_univ _) h)] · rw [Finset.sum_eq_single d1 (fun d1' _ hne => ?_) (fun h => absurd (Finset.mem_univ _) h)] · rw [Finset.sum_eq_single y0 (fun y0' _ hne => ?_) (fun h => absurd (Finset.mem_univ _) h)] · rw [Finset.sum_eq_single y1 (fun y1' _ hne => ?_) (fun h => absurd (Finset.mem_univ _) h)] · simp · simp [hne] · refine Finset.sum_eq_zero (fun y1' _ => ?_) simp [hne] · refine Finset.sum_eq_zero (fun y0' _ => ?_) refine Finset.sum_eq_zero (fun y1' _ => ?_) simp [hne] · refine Finset.sum_eq_zero (fun d1' _ => ?_) refine Finset.sum_eq_zero (fun y0' _ => ?_) refine Finset.sum_eq_zero (fun y1' _ => ?_) simp [hne] -
canonical_latentSetlemma — The canonical latent set is Set.univ ×ˢ {(d0, d1, y0, y1)}.hypotheseshπ_sum :shared∑ d0, ∑ d1, ∑ y0, ∑ y1, π d0 d1 y0 y1 = 1d0 d1 y0 y1 :Proof (Lean source)
lemma canonical_latentSet (d0 d1 y0 y1 : Bool) : (S' S π hπ_nn hπ_sum).latentSet d0 d1 y0 y1 = (univ ×ˢ {(d0, d1, y0, y1)} : Set SOmega) := by ext ω rcases ω with ⟨z, d0', d1', y0', y1'⟩ change ((S' S π hπ_nn hπ_sum).DofZ false (z, d0', d1', y0', y1') = d0 ∧ (S' S π hπ_nn hπ_sum).DofZ true (z, d0', d1', y0', y1') = d1 ∧ (S' S π hπ_nn hπ_sum).YofD false (z, d0', d1', y0', y1') = y0 ∧ (S' S π hπ_nn hπ_sum).YofD true (z, d0', d1', y0', y1') = y1) ↔ _ rw [canonical_DofZ, canonical_DofZ, canonical_YofD, canonical_YofD] change ((POBalkePearlSystem.dArm false d0' d1' = d0) ∧ (POBalkePearlSystem.dArm true d0' d1' = d1) ∧ (POBalkePearlSystem.yArm false y0' y1' = y0) ∧ (POBalkePearlSystem.yArm true y0' y1' = y1)) ↔ (z, d0', d1', y0', y1') ∈ (univ ×ˢ {(d0, d1, y0, y1)} : Set SOmega) unfold POBalkePearlSystem.dArm POBalkePearlSystem.yArm simp only [Bool.false_eq_true, if_false, if_true] refine ⟨?_, ?_⟩ · rintro ⟨rfl, rfl, rfl, rfl⟩ exact Set.mk_mem_prod (Set.mem_univ _) rfl · rintro ⟨_, h2⟩ rw [Set.mem_singleton_iff] at h2 -- h2 : (z, d0', d1', y0', y1').2 = (d0, d1, y0, y1) -- Need: conjunction of equalities. simp only [Prod.mk.injEq] at h2 exact h2 -
canonical_latentSet_measurelemma — μ'(latentSet) = ENNReal.ofReal (π d0 d1 y0 y1).hypotheseshπ_sum :shared∑ d0, ∑ d1, ∑ y0, ∑ y1, π d0 d1 y0 y1 = 1d0 d1 y0 y1 :Proof (Lean source)
lemma canonical_latentSet_measure (d0 d1 y0 y1 : Bool) : (P' S π hπ_nn hπ_sum).μ ((S' S π hπ_nn hπ_sum).latentSet d0 d1 y0 y1) = ofReal (π d0 d1 y0 y1) := by rw [canonical_latentSet] change (canonicalMeasure S π) (univ ×ˢ {(d0, d1, y0, y1)}) = _ unfold canonicalMeasure letI : IsProbabilityMeasure (piMeasure π) := instIsProbPiMeasure hπ_nn hπ_sum rw [Measure.prod_prod, zMeasure_univ, one_mul, piMeasure_singleton] -
canonical_latentProb_eqlemma — S'.latentProb = π.hypotheseshπ_sum :shared∑ d0, ∑ d1, ∑ y0, ∑ y1, π d0 d1 y0 y1 = 1d0 d1 y0 y1 :conclusion(S' S π hπ_nn hπ_sum).latentProb d0 d1 y0 y1 = π d0 d1 y0 y1Proof (Lean source)
lemma canonical_latentProb_eq (d0 d1 y0 y1 : Bool) : (S' S π hπ_nn hπ_sum).latentProb d0 d1 y0 y1 = π d0 d1 y0 y1 := by unfold POBalkePearlSystem.latentProb rw [canonical_latentSet_measure] exact ENNReal.toReal_ofReal (hπ_nn _ _ _ _) -
canonical_cellProb_eqlemma — S'.cellProb y d z = S.cellProb y d z for any feasible π.hypotheseshπ_sum :shared∑ d0, ∑ d1, ∑ y0, ∑ y1, π d0 d1 y0 y1 = 1hA :S.BaseAssumptionshπ :POBalkePearlSystem.BPFeasible S hA πy d z :conclusion(S' S π hπ_nn hπ_sum).cellProb y d z = S.cellProb y d zProof (Lean source)
lemma canonical_cellProb_eq (hA : S.BaseAssumptions) (hπ : POBalkePearlSystem.BPFeasible S hA π) (y d z : Bool) : (S' S π hπ_nn hπ_sum).cellProb y d z = S.cellProb y d z := by rw [(S' S π hπ_nn hπ_sum).cellProb_eq_sum_latent (canonical_baseAssumptions S π hπ_nn hπ_sum hA) y d z, hπ.marginal y d z] 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 _ => ?_) rw [canonical_latentProb_eq] -
canonical_ATE_eqlemma — S'.ATE = BPObjective π.hypotheseshπ_sum :shared∑ d0, ∑ d1, ∑ y0, ∑ y1, π d0 d1 y0 y1 = 1hA :S.BaseAssumptionsconclusion(S' S π hπ_nn hπ_sum).ATE = POBalkePearlSystem.BPObjective πProof (Lean source)
lemma canonical_ATE_eq (hA : S.BaseAssumptions) : (S' S π hπ_nn hπ_sum).ATE = POBalkePearlSystem.BPObjective π := by rw [(S' S π hπ_nn hπ_sum).ATE_eq_BPObjective (canonical_baseAssumptions S π hπ_nn hπ_sum hA)] unfold POBalkePearlSystem.BPObjective 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 _ => ?_) rw [canonical_latentProb_eq]