PO.ID.Partial.Balke­Pearl

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)

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]

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]

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

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]

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]

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)

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 _)

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]

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

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

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

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

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

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

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]

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

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

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

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]

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]

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]

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

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

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

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

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 ω))

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)]

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

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 => Fin.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

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

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

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]

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

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]

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 _ _ _ _)

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]

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]