PO.Bridge

theorem FiniteCellData.condExp_treated_sub_control_of_pair (hCI : CondIndepFun D.sigmaX D.sigmaX_le (fun ω => (D.Y0 ω, D.Y1 ω)) D.A μ) (hpos : ∀ d, ∀ᵐ ω ∂μ, D.armProb d (D.X ω) ≠ 0) : μ[fun ω => boolReal (D.Y1 ω) - boolReal (D.Y0 ω) | D.sigmaX] =ᵐ[μ] fun ω => D.mean true (D.X ω) - D.mean false (D.X ω) := by exact D.condExp_treated_sub_control (D.condIndep_potential_of_pair hCI) hpos

theorem POSystem.ofSCM_consistency (M : SCM N Ω) (s : SCM.FixedValues M) : (POSystem.ofSCM M s).Consistency where -- --------------------------------------------------------------- -- Factual consistency -- --------------------------------------------------------------- factual := by intro r Y hY_disj ℓ hFactual funext v simp only [POSystem.poVariable, POSystem.ofSCM] change inducedEval M s r ℓ v.val = inducedEval M s Regime.empty ℓ v.val rw [inducedEval_empty_eq_evalMap M s ℓ v.val] -- Clear the let-binding from inducedEval's `hmem` simp only [inducedEval] -- Goal: (M.fixSet (regimeTargetN M r) ...).evalMap (combinedFixed M s r) ℓ ⟨v.val.val, _⟩ -- = M.evalMap s ℓ ⟨v.val.val, _⟩ exact SCM.evalMap_fixSet_factual_eq M (regimeTargetN M r) (regimeTargetN_obs M r) (regimeTargetN_notFixed M r) s ℓ (combinedFixed M s r) -- hOld: combinedFixed agrees with s on M.fixed (fun w hw => combinedFixed_old M s r w hw) -- hNew: for D ∈ regimeTargetN M r, -- M.evalMap s ℓ ⟨.random D, _⟩ = combinedFixed M s r ⟨.fixed D, _⟩ (fun D hD => by obtain ⟨v', hv'tgt, hDval⟩ := regimeTargetN_mem_val M r D hD have hfa := hFactual v' hv'tgt simp only [POSystem.ofSCM] at hfa change inducedEval M s Regime.empty ℓ v' = r.assign v' hv'tgt at hfa rw [inducedEval_empty_eq_evalMap M s ℓ v'] at hfa -- hfa : M.evalMap s ℓ ⟨v'.val, _⟩ = r.assign v' hv'tgt : swigΩ Ω v'.val rw [combinedFixed_new M s r v' hv'tgt D hD hDval] obtain ⟨v'val, v'prop⟩ := v' cases hDval exact hfa) ⟨v.val.val, v.val.property⟩

theorem integral_observedLaw_weighted_centered (d : Bool) (w c : γ → ℝ) (hm : Measurable w) (hc : Measurable c) (hw : Integrable w (μ.map D.X)) (hwc : Integrable (fun x => w x * c x) (μ.map D.X)) : ∫ z : γ × Bool × Bool, w z.1 * (armIndicator d z.2.1 * (boolReal z.2.2 - c z.1)) ∂D.observedLaw = ∫ x, w x * (D.armProb d x * (D.mean d x - c x)) ∂(μ.map D.X) := by have hY : Measurable (observedY D.A D.Y0 D.Y1) := by exact Measurable.ite (measurableSet_eq_fun D.measurable_A measurable_const) D.measurable_Y1 D.measurable_Y0 have hmap : Measurable (fun ω => (D.X ω, D.A ω, observedY D.A D.Y0 D.Y1 ω)) := D.measurable_X.prodMk (D.measurable_A.prodMk hY) have hweight : Integrable (fun ω => w (D.X ω)) μ := (integrable_map_measure hm.aestronglyMeasurable D.measurable_X.aemeasurable).1 hw have hweightc : Integrable (fun ω => w (D.X ω) * c (D.X ω)) μ := (integrable_map_measure (hm.mul hc).aestronglyMeasurable D.measurable_X.aemeasurable).1 hwc have hbase : Integrable (fun z : γ × Bool × Bool => w z.1) D.observedLaw := by rw [D.observedLaw_eq_map] exact (integrable_map_measure (hm.comp measurable_fst).aestronglyMeasurable hmap.aemeasurable).2 hweight have hbasec : Integrable (fun z : γ × Bool × Bool => w z.1 * c z.1) D.observedLaw := by rw [D.observedLaw_eq_map] exact (integrable_map_measure ((hm.mul hc).comp measurable_fst).aestronglyMeasurable hmap.aemeasurable).2 hweightc have hArm : Measurable (fun z : γ × Bool × Bool => armIndicator d z.2.1) := by unfold armIndicator exact Measurable.ite (measurableSet_eq_fun (measurable_fst.comp measurable_snd) measurable_const) measurable_const measurable_const have hBool : Measurable (fun z : γ × Bool × Bool => boolReal z.2.2) := by unfold boolReal exact Measurable.ite (measurableSet_eq_fun (measurable_snd.comp measurable_snd) measurable_const) measurable_const measurable_const have hArmBound : ∀ z : γ × Bool × Bool, ‖armIndicator d z.2.1‖ ≤ (1 : ℝ) := by intro z simp only [armIndicator] split_ifs <;> simp have hBoolBound : ∀ z : γ × Bool × Bool, ‖boolReal z.2.2‖ ≤ (1 : ℝ) := by intro z simp only [boolReal] split_ifs <;> simp have hLarm : Integrable (fun z : γ × Bool × Bool => w z.1 * armIndicator d z.2.1) D.observedLaw := hbase.mul_bdd hArm.aestronglyMeasurable (ae_of_all _ hArmBound) have hLprod : Integrable (fun z : γ × Bool × Bool => w z.1 * armIndicator d z.2.1 * boolReal z.2.2) D.observedLaw := hLarm.mul_bdd hBool.aestronglyMeasurable (ae_of_all _ hBoolBound) have hLcenter : Integrable (fun z : γ × Bool × Bool => w z.1 * c z.1 * armIndicator d z.2.1) D.observedLaw := hbasec.mul_bdd hArm.aestronglyMeasurable (ae_of_all _ hArmBound) have hRarm : Integrable (fun x => w x * D.armProb d x) (μ.map D.X) := hw.mul_bdd (D.measurable_armProb d).aestronglyMeasurable (ae_of_all _ (fun x => by rw [Real.norm_eq_abs, abs_le] exact ⟨by linarith [(D.armProb_mem_Icc d x).1], (D.armProb_mem_Icc d x).2⟩)) have hRprod : Integrable (fun x => w x * D.armProb d x * D.mean d x) (μ.map D.X) := hRarm.mul_bdd (D.measurable_mean d).aestronglyMeasurable (ae_of_all _ (fun x => by rw [Real.norm_eq_abs, abs_le] exact ⟨by linarith [(D.mean_mem_Icc d x).1], (D.mean_mem_Icc d x).2⟩)) have hRcenter : Integrable (fun x => w x * c x * D.armProb d x) (μ.map D.X) := hwc.mul_bdd (D.measurable_armProb d).aestronglyMeasurable (ae_of_all _ (fun x => by rw [Real.norm_eq_abs, abs_le] exact ⟨by linarith [(D.armProb_mem_Icc d x).1], (D.armProb_mem_Icc d x).2⟩)) calc _ = (∫ z : γ × Bool × Bool, w z.1 * armIndicator d z.2.1 * boolReal z.2.2 ∂D.observedLaw) - (∫ z : γ × Bool × Bool, (w z.1 * c z.1) * armIndicator d z.2.1 ∂D.observedLaw) := by rw [← integral_sub hLprod hLcenter] congr 1 funext z ring _ = (∫ x, w x * D.armProb d x * D.mean d x ∂(μ.map D.X)) - (∫ x, (w x * c x) * D.armProb d x ∂(μ.map D.X)) := by rw [integral_observedLaw_weighted_observedProduct D d w hm hw, integral_observedLaw_weighted_arm D d (fun x => w x * c x) (hm.mul hc) hwc] _ = _ := by rw [← integral_sub hRprod hRcenter] congr 1 funext x ring

theorem integral_pair_centered (d e : Bool) (W : γ → γ → ℝ) (c k : γ → ℝ) (hW : Measurable fun p : γ × γ => W p.1 p.2) (hc : Measurable c) (hk : Measurable k) (hInt : Integrable (fun p : γ × γ => |W p.1 p.2| * (1 + |c p.1|) * (1 + |k p.2|)) ((μ.map D.X).prod (μ.map D.X))) : ∫ z : (γ × Bool × Bool) × (γ × Bool × Bool), W z.1.1 z.2.1 * (armIndicator d z.1.2.1 * (boolReal z.1.2.2 - c z.1.1)) * (armIndicator e z.2.2.1 * (boolReal z.2.2.2 - k z.2.1)) ∂(D.observedLaw.prod D.observedLaw) = ∫ p : γ × γ, W p.1 p.2 * (D.armProb d p.1 * (D.mean d p.1 - c p.1)) * (D.armProb e p.2 * (D.mean e p.2 - k p.2)) ∂((μ.map D.X).prod (μ.map D.X)) := by -- Put `ν := μ.map D.X` and `ρ := D.observedLaw`. The hypothesis controls -- `W`, `W * c`, `W * k`, and `W * c * k` on `ν.prod ν` by domination. -- Transport that envelope to `ρ.prod ρ` with `pair_covariate_map`; both -- centered factors are bounded by `1 + |center|` pointwise. Fubini then -- applies to the displayed left integrand. For almost every first draw, -- use `integral_observedLaw_weighted_centered D e` on the second draw, -- with slice weight `y ↦ W x y`; Fubini's `prod_right_ae` gives the weight -- and weight-times-k integrability. Integrate the resulting function of x -- using the same one-draw theorem for d. The outer weight is the integral -- in y of `W x y * (armProb e y * (mean e y - k y))`; its integrability and -- its product with c follow from the original envelope and Fubini. letI : IsProbabilityMeasure D.observedLaw := observedLaw_isProbability D let ν : Measure γ := μ.map D.X let ρ : Measure (γ × Bool × Bool) := D.observedLaw have hν : IsProbabilityMeasure ν := Measure.isProbabilityMeasure_map D.measurable_X.aemeasurable letI : IsProbabilityMeasure ν := hν let E : γ × γ → ℝ := fun p => |W p.1 p.2| * (1 + |c p.1|) * (1 + |k p.2|) have hE : Integrable E (ν.prod ν) := hInt have hEm : Measurable E := by dsimp [E] fun_prop have hWint : Integrable (fun p : γ × γ => W p.1 p.2) (ν.prod ν) := by apply hE.mono' hW.aestronglyMeasurable filter_upwards with p dsimp [E] have hc0 : 0 ≤ |c p.1| := abs_nonneg _ have hk0 : 0 ≤ |k p.2| := abs_nonneg _ calc |W p.1 p.2| = |W p.1 p.2| * 1 * 1 := by ring _ ≤ |W p.1 p.2| * (1 + |c p.1|) * (1 + |k p.2|) := by gcongr <;> linarith have hWc : Integrable (fun p : γ × γ => W p.1 p.2 * c p.1) (ν.prod ν) := by apply hE.mono' (hW.mul (hc.comp measurable_fst)).aestronglyMeasurable filter_upwards with p dsimp [E] rw [abs_mul] have hc0 : 0 ≤ |c p.1| := abs_nonneg _ have hk0 : 0 ≤ |k p.2| := abs_nonneg _ calc |W p.1 p.2| * |c p.1| = |W p.1 p.2| * |c p.1| * 1 := by ring _ ≤ |W p.1 p.2| * (1 + |c p.1|) * (1 + |k p.2|) := by gcongr <;> linarith have hWk : Integrable (fun p : γ × γ => W p.1 p.2 * k p.2) (ν.prod ν) := by apply hE.mono' (hW.mul (hk.comp measurable_snd)).aestronglyMeasurable filter_upwards with p dsimp [E] rw [abs_mul] have hc0 : 0 ≤ |c p.1| := abs_nonneg _ have hk0 : 0 ≤ |k p.2| := abs_nonneg _ calc |W p.1 p.2| * |k p.2| = |W p.1 p.2| * 1 * |k p.2| := by ring _ ≤ |W p.1 p.2| * (1 + |c p.1|) * (1 + |k p.2|) := by gcongr <;> linarith have hWck : Integrable (fun p : γ × γ => W p.1 p.2 * c p.1 * k p.2) (ν.prod ν) := by apply hE.mono' ((hW.mul (hc.comp measurable_fst)).mul (hk.comp measurable_snd)).aestronglyMeasurable filter_upwards with p dsimp [E] rw [abs_mul, abs_mul] have hc0 : 0 ≤ |c p.1| := abs_nonneg _ have hk0 : 0 ≤ |k p.2| := abs_nonneg _ gcongr <;> linarith have hArm (a : Bool) : Measurable (fun z : γ × Bool × Bool => armIndicator a z.2.1) := by unfold armIndicator exact Measurable.ite (measurableSet_eq_fun (measurable_fst.comp measurable_snd) measurable_const) measurable_const measurable_const have hBool : Measurable (fun z : γ × Bool × Bool => boolReal z.2.2) := by unfold boolReal exact Measurable.ite (measurableSet_eq_fun (measurable_snd.comp measurable_snd) measurable_const) measurable_const measurable_const have hArmB (a b : Bool) : |armIndicator a b| ≤ (1 : ℝ) := by simp only [armIndicator] split_ifs <;> simp have hBoolB (b : Bool) : |boolReal b| ≤ (1 : ℝ) := by simp only [boolReal] split_ifs <;> simp have hCenteredB (b : Bool) (r : ℝ) : |boolReal b - r| ≤ 1 + |r| := by calc _ ≤ |boolReal b| + |r| := abs_sub _ _ _ ≤ 1 + |r| := add_le_add_left (hBoolB b) _ have hMeanB (a : Bool) (x : γ) : |D.mean a x| ≤ (1 : ℝ) := by rw [abs_of_nonneg (D.mean_mem_Icc a x).1] exact (D.mean_mem_Icc a x).2 have hProbB (a : Bool) (x : γ) : |D.armProb a x| ≤ (1 : ℝ) := by rw [abs_of_nonneg (D.armProb_mem_Icc a x).1] exact (D.armProb_mem_Icc a x).2 have hObsB (a : Bool) (z : γ × Bool × Bool) (r : ℝ) : |armIndicator a z.2.1 * (boolReal z.2.2 - r)| ≤ 1 + |r| := by rw [abs_mul] calc _ ≤ 1 * (1 + |r|) := by gcongr · exact hArmB a z.2.1 · exact hCenteredB z.2.2 r _ = _ := by ring let pairX : ((γ × Bool × Bool) × (γ × Bool × Bool)) → γ × γ := fun z => (z.1.1, z.2.1) have hpairX : Measurable pairX := (measurable_fst.comp measurable_fst).prodMk (measurable_fst.comp measurable_snd) have hρE : Integrable (fun z : (γ × Bool × Bool) × (γ × Bool × Bool) => E (pairX z)) (ρ.prod ρ) := by rw [← pair_covariate_map D] at hE exact (integrable_map_measure hEm.aestronglyMeasurable hpairX.aemeasurable).1 hE have hL : Integrable (fun z : (γ × Bool × Bool) × (γ × Bool × Bool) => W z.1.1 z.2.1 * (armIndicator d z.1.2.1 * (boolReal z.1.2.2 - c z.1.1)) * (armIndicator e z.2.2.1 * (boolReal z.2.2.2 - k z.2.1))) (ρ.prod ρ) := by apply hρE.mono' ?_ ?_ · have hm : Measurable (fun z : (γ × Bool × Bool) × (γ × Bool × Bool) => W z.1.1 z.2.1 * (armIndicator d z.1.2.1 * (boolReal z.1.2.2 - c z.1.1)) * (armIndicator e z.2.2.1 * (boolReal z.2.2.2 - k z.2.1))) := by fun_prop (disch := assumption) exact hm.aestronglyMeasurable · filter_upwards with z dsimp [E, pairX] simp only [Real.norm_eq_abs, abs_mul] gcongr · simpa only [abs_mul] using hObsB d z.1 (c z.1.1) · simpa only [abs_mul] using hObsB e z.2 (k z.2.1) let Q : γ → ℝ := fun y => D.armProb e y * (D.mean e y - k y) have hQm : Measurable Q := by exact (D.measurable_armProb e).mul ((D.measurable_mean e).sub hk) have hFQ : Integrable (fun p : γ × γ => W p.1 p.2 * Q p.2) (ν.prod ν) := by have h₁ := hWint.mul_bdd (((D.measurable_armProb e).comp measurable_snd).aestronglyMeasurable) (ae_of_all _ fun p => by simpa [Real.norm_eq_abs] using hProbB e p.2) have h₂ := h₁.mul_bdd (((D.measurable_mean e).comp measurable_snd).aestronglyMeasurable) (ae_of_all _ fun p => by simpa [Real.norm_eq_abs] using hMeanB e p.2) have h₃ := hWk.mul_bdd (((D.measurable_armProb e).comp measurable_snd).aestronglyMeasurable) (ae_of_all _ fun p => by simpa [Real.norm_eq_abs] using hProbB e p.2) convert h₂.sub h₃ using 1 <;> funext p <;> dsimp [Q] <;> ring have hFcQ : Integrable (fun p : γ × γ => (W p.1 p.2 * Q p.2) * c p.1) (ν.prod ν) := by have h₁ := hWc.mul_bdd (((D.measurable_armProb e).comp measurable_snd).aestronglyMeasurable) (ae_of_all _ fun p => by simpa [Real.norm_eq_abs] using hProbB e p.2) have h₂ := h₁.mul_bdd (((D.measurable_mean e).comp measurable_snd).aestronglyMeasurable) (ae_of_all _ fun p => by simpa [Real.norm_eq_abs] using hMeanB e p.2) have h₃ := hWck.mul_bdd (((D.measurable_armProb e).comp measurable_snd).aestronglyMeasurable) (ae_of_all _ fun p => by simpa [Real.norm_eq_abs] using hProbB e p.2) convert h₂.sub h₃ using 1 <;> funext p <;> dsimp [Q] <;> ring let g : γ → ℝ := fun x => ∫ y, W x y * Q y ∂ν have hg : Integrable g ν := hFQ.integral_prod_left have hgc : Integrable (fun x => g x * c x) ν := by convert hFcQ.integral_prod_left using 1 funext x dsimp [g] rw [integral_mul_const] have hgm : Measurable g := by exact ((hW.mul (hQm.comp measurable_snd)).stronglyMeasurable |>.integral_prod_right').measurable have hslice : ∀ᵐ z ∂ρ, Integrable (fun y => W z.1 y) ν ∧ Integrable (fun y => W z.1 y * k y) ν := by have hY : Measurable (observedY D.A D.Y0 D.Y1) := Measurable.ite (measurableSet_eq_fun D.measurable_A measurable_const) D.measurable_Y1 D.measurable_Y0 have hobs : Measurable (fun ω => (D.X ω, D.A ω, observedY D.A D.Y0 D.Y1 ω)) := D.measurable_X.prodMk (D.measurable_A.prodMk hY) have hmarg : ρ.map fst = ν := by dsimp [ρ, ν] rw [D.observedLaw_eq_map, Measure.map_map measurable_fst hobs] rfl have hs : ∀ᵐ x ∂ν, Integrable (fun y => W x y) ν ∧ Integrable (fun y => W x y * k y) ν := by filter_upwards [hWint.prod_right_ae, hWk.prod_right_ae] with x hx hy exact ⟨hx, hy⟩ have hs' : ∀ᵐ x ∂ρ.map fst, Integrable (fun y => W x y) ν ∧ Integrable (fun y => W x y * k y) ν := by rw [hmarg] exact hs exact ae_of_ae_map measurable_fst.aemeasurable hs' have hR : Integrable (fun p : γ × γ => W p.1 p.2 * (D.armProb d p.1 * (D.mean d p.1 - c p.1)) * Q p.2) (ν.prod ν) := by have h₁ := hFQ.mul_bdd (((D.measurable_armProb d).comp measurable_fst).aestronglyMeasurable) (ae_of_all _ fun p => by simpa [Real.norm_eq_abs] using hProbB d p.1) have h₂ := h₁.mul_bdd (((D.measurable_mean d).comp measurable_fst).aestronglyMeasurable) (ae_of_all _ fun p => by simpa [Real.norm_eq_abs] using hMeanB d p.1) have h₃ := hFcQ.mul_bdd (((D.measurable_armProb d).comp measurable_fst).aestronglyMeasurable) (ae_of_all _ fun p => by simpa [Real.norm_eq_abs] using hProbB d p.1) convert h₂.sub h₃ using 1 <;> funext p <;> dsimp [Q] <;> ring have hmarg : ρ.map fst = ν := by have hY : Measurable (observedY D.A D.Y0 D.Y1) := Measurable.ite (measurableSet_eq_fun D.measurable_A measurable_const) D.measurable_Y1 D.measurable_Y0 have hobs : Measurable (fun ω => (D.X ω, D.A ω, observedY D.A D.Y0 D.Y1 ω)) := D.measurable_X.prodMk (D.measurable_A.prodMk hY) dsimp [ρ, ν] rw [D.observedLaw_eq_map, Measure.map_map measurable_fst hobs] rfl have hCentered (a : Bool) (w r : γ → ℝ) (hwmeas : Measurable w) (hrmeas : Measurable r) (hw : Integrable w ν) (hwr : Integrable (fun x => w x * r x) ν) : ∫ z : γ × Bool × Bool, w z.1 * (armIndicator a z.2.1 * (boolReal z.2.2 - r z.1)) ∂ρ = ∫ x, w x * (D.armProb a x * (D.mean a x - r x)) ∂ν := by have hbase : Integrable (fun z : γ × Bool × Bool => w z.1) ρ := by -- … truncated; follow the source link for the rest …

theorem integral_uStatistic_arm (n : ℕ) (hn : 2 ≤ n) (d : Bool) (W : γ → γ → ℝ) (hSym : ∀ x y, W x y = W y x) (hW : Measurable fun p : γ × γ => W p.1 p.2) (hInt : Integrable (fun p : γ × γ => W p.1 p.2) ((μ.map D.X).prod (μ.map D.X))) : ∫ ω, uStatistic n (fun z z' : γ × Bool × Bool => W z.1 z'.1 * armIndicator d z.2.1 * armIndicator d z'.2.1) ω ∂iidLaw D.observedLaw n = ∫ p : γ × γ, W p.1 p.2 * D.armProb d p.1 * D.armProb d p.2 ∂((μ.map D.X).prod (μ.map D.X)) := by letI : IsProbabilityMeasure D.observedLaw := observedLaw_isProbability D let H : (γ × Bool × Bool) → (γ × Bool × Bool) → ℝ := fun z z' => W z.1 z'.1 * armIndicator d z.2.1 * armIndicator d z'.2.1 have hSymH : ∀ z z', H z z' = H z' z := by intro z z' dsimp [H] rw [hSym] ring have hA : Measurable (fun z : γ × Bool × Bool => armIndicator d z.2.1) := by unfold armIndicator exact Measurable.ite (measurableSet_eq_fun (measurable_fst.comp measurable_snd) measurable_const) measurable_const measurable_const have hH : Measurable (fun p : (γ × Bool × Bool) × (γ × Bool × Bool) => H p.1 p.2) := by dsimp [H] exact (hW.comp ((measurable_fst.comp measurable_fst).prodMk (measurable_fst.comp measurable_snd))).mul (hA.comp measurable_fst) |>.mul (hA.comp measurable_snd) have hAb (z : γ × Bool × Bool) : ‖armIndicator d z.2.1‖ ≤ 1 := by simp only [armIndicator] split_ifs <;> simp have hbase : Integrable (fun p : (γ × Bool × Bool) × (γ × Bool × Bool) => W p.1.1 p.2.1) (D.observedLaw.prod D.observedLaw) := by rw [← pair_covariate_map D] at hInt exact (integrable_map_measure hW.aestronglyMeasurable ((measurable_fst.comp measurable_fst).prodMk (measurable_fst.comp measurable_snd)).aemeasurable).1 hInt have hIntH : Integrable (fun p : (γ × Bool × Bool) × (γ × Bool × Bool) => H p.1 p.2) (D.observedLaw.prod D.observedLaw) := by have h₁ := hbase.mul_bdd (hA.comp measurable_fst).aestronglyMeasurable (ae_of_all _ fun p => hAb p.1) exact h₁.mul_bdd (hA.comp measurable_snd).aestronglyMeasurable (ae_of_all _ fun p => hAb p.2) calc _ = ∫ p : (γ × Bool × Bool) × (γ × Bool × Bool), H p.1 p.2 ∂(D.observedLaw.prod D.observedLaw) := integral_uStatistic_eq_pair D.observedLaw n hn H hH hIntH _ = _ := integral_pair_arm D d d W hW hInt

theorem ofSCM_condIndepCF_of_dSep (M : SCM N Ω) (s : SCM.FixedValues M) [StandardBorelSpace M.RandomValues] [StandardBorelSpace M.LatentValues] [StandardBorelSpace (POSystem.ofSCM M s).Ω] [∀ n, StandardBorelSpace (swigΩ Ω n)] [∀ n, Nonempty (swigΩ Ω n)] [∀ s' : M.FixedValues, IsFiniteMeasure (M.jointKernel s')] {X Y Z : Finset (SWIGNode N)} (hX : X ⊆ M.randomVars) (hY : Y ⊆ M.randomVars) (hZ : Z ⊆ M.randomVars) (hdSep : M.dag.dSep X Y Z) {α : Type*} [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] (a : RegimedVar (POSystem.ofSCM M s) α) (B : POCFBundle (POSystem.ofSCM M s)) [StandardBorelSpace (∀ i : Fin B.n, B.type i)] [Nonempty (∀ i : Fin B.n, B.type i)] (c : RegimedVar (POSystem.ofSCM M s) (ValuesOn Z (swigΩ Ω))) (aMap : ValuesOn X (swigΩ Ω) → α) (BMap : ValuesOn Y (swigΩ Ω) → (∀ i : Fin B.n, B.type i)) (haMap : Measurable aMap) (hBMap : Measurable BMap) (ha_value : a.value = aMap ∘ valuesProjection (Ω := swigΩ Ω) hX ∘ (fun ℓ : M.LatentValues => M.evalMap s ℓ)) (hB_value : B.jointValue = BMap ∘ valuesProjection (Ω := swigΩ Ω) hY ∘ (fun ℓ : M.LatentValues => M.evalMap s ℓ)) (hc_value : c.value = valuesProjection (Ω := swigΩ Ω) hZ ∘ (fun ℓ : M.LatentValues => M.evalMap s ℓ)) : (POSystem.ofSCM M s).CondIndepCF a B c (POSystem.ofSCM M s).μ := by let E : M.LatentValues → M.RandomValues := fun ℓ => M.evalMap s ℓ have hE : Measurable E := by have hmeas := M.evalMap_measurable simpa [E, uncurry, Function.comp_def] using hmeas.comp (prodMk measurable_const measurable_id) have hFull : SCM.FullCondIndep M X Y Z hX hY hZ (M.jointKernel s) := SCM.full_globalMarkov M X Y Z hX hY hZ hdSep s have hJointEq : M.jointKernel s = M.latentProduct.map E := by simpa [E] using SCM.jointKernel_apply_eq M s haveI : IsFiniteMeasure (M.latentProduct.map E) := hJointEq ▸ (inferInstance : IsFiniteMeasure (M.jointKernel s)) have hFullMap : CondIndepFun (comap (valuesProjection (Ω := swigΩ Ω) hZ) inferInstance) (comap_valuesProjection_le (Ω' := swigΩ Ω) hZ) (valuesProjection (Ω := swigΩ Ω) hX) (valuesProjection (Ω := swigΩ Ω) hY) (M.latentProduct.map E) := by simpa [SCM.FullCondIndep, hJointEq] using hFull have hPull : CondIndepFun (comap (valuesProjection (Ω := swigΩ Ω) hZ ∘ E) inferInstance) (comap_le ((measurable_valuesProjection (Ω' := swigΩ Ω) hZ).comp hE)) (valuesProjection (Ω := swigΩ Ω) hX ∘ E) (valuesProjection (Ω := swigΩ Ω) hY ∘ E) M.latentProduct := condIndepFun_comp_of_map hE (measurable_valuesProjection (Ω' := swigΩ Ω) hX) (measurable_valuesProjection (Ω' := swigΩ Ω) hY) (measurable_valuesProjection (Ω' := swigΩ Ω) hZ) hFullMap have hComp : CondIndepFun (comap (valuesProjection (Ω := swigΩ Ω) hZ ∘ E) inferInstance) (comap_le ((measurable_valuesProjection (Ω' := swigΩ Ω) hZ).comp hE)) (aMap ∘ valuesProjection (Ω := swigΩ Ω) hX ∘ E) (BMap ∘ valuesProjection (Ω := swigΩ Ω) hY ∘ E) M.latentProduct := by simpa [Function.comp_assoc] using hPull.comp haMap hBMap unfold CondIndepCF convert hComp using 3 · rfl · exact heq_of_eq hc_value · exact HEq.rfl · exact heq_of_eq ha_value · exact heq_of_eq hB_value · exact HEq.rfl

theorem restrict_consistency (hP : P.Consistency) : (P.restrict R).Consistency where factual := by intro r' Y hYr ω hag -- Build the ambient FactualAgrees witness. have hagP : P.FactualAgrees (P.liftRegime R r') ω := by intro v hv rcases Finset.mem_map.mp hv with ⟨w, hw, rfl⟩ have hv' : (w.val : P.V) ∈ (P.liftRegime R r').target := hv change P.eval Regime.empty ω w.val = (P.liftRegime R r').assign w.val hv' rw [P.liftRegime_assign R r' w hw] exact hag w hw -- Lift Y. set Yamb : Finset P.V := Y.map ⟨Subtype.val, Subtype.val_injective⟩ with hYamb_def have hYr_amb : _root_.Disjoint Yamb (P.liftRegime R r').target := by rw [hYamb_def, Finset.disjoint_left] intro v hvY hvr rcases Finset.mem_map.mp hvY with ⟨y, hy, rfl⟩ rcases Finset.mem_map.mp hvr with ⟨w, hw, hwy⟩ have : y = w := val_injective hwy.symm subst this exact (Finset.disjoint_left.mp hYr hy) hw have hpv := hP.factual (P.liftRegime R r') Yamb hYr_amb ω hagP -- Pointwise equality on Y. funext y have hyamb : (y.val.val : P.V) ∈ Yamb := by rw [hYamb_def]; exact Finset.mem_map.mpr ⟨y.val, y.property, rfl⟩ have heq := congrArg (fun f => f ⟨y.val.val, hyamb⟩) hpv -- Goal: (P.restrict R).poVariable r' Y ω y = (P.restrict R).poVariable Regime.empty Y ω y change P.eval (P.liftRegime R r') ω y.val.val = P.eval (P.liftRegime R Regime.empty) ω y.val.val rw [liftRegime_empty] exact heq