PO.ID.Exact.QTE

lemma integral_comp_YofD_eq [StandardBorelSpace P.Ω] [IsFiniteMeasure P.μ] (hA : S.DistributionalAssumptions) (d : Bool) {g : ℝ → ℝ} (hg : Measurable g) {C : ℝ} (hg_bdd : ∀ y, |g y| ≤ C) : ∫ ω, g (S.YofD d ω) ∂P.μ = ∫ ω, g (S.factualY ω) * S.ipwDensity d ω ∂P.μ := by classical -- Measurability of the composites and the indicator / propensity score. have hgY_meas : Measurable (fun ω => g (S.factualY ω)) := hg.comp S.measurable_factualY have hgYd_meas : Measurable (fun ω => g (S.YofD d ω)) := hg.comp (S.measurable_YofD d) have hind_meas : Measurable (S.dVar.indicator d) := S.dVar.measurable_indicator d (measurableSet_singleton d) have he_sm : StronglyMeasurable[S.sigmaX] (S.propScore d) := S.stronglyMeasurable_propScore d have he_pos : ∀ᵐ ω ∂P.μ, 0 < S.propScore d ω := S.propScore_pos hA d have hipw_meas : Measurable (S.ipwDensity d) := hind_meas.div (he_sm.mono S.sigmaX_le).measurable have hipw_nn : 0 ≤ᵐ[P.μ] S.ipwDensity d := by filter_upwards [he_pos] with ω hω refine div_nonneg ?_ hω.le rcases S.dVar.indicator_eq_one_or_zero d ω with h | h <;> simp [h] -- Integrability of the pieces (everything bounded by `C`, resp. `C·ipw`). have hgYd_int : Integrable (fun ω => g (S.YofD d ω)) P.μ := (integrable_const C).mono' hgYd_meas.aestronglyMeasurable (Filter.Eventually.of_forall (fun ω => by rw [Real.norm_eq_abs]; exact hg_bdd _)) have prod_int : Integrable (fun ω => S.dVar.indicator d ω * g (S.YofD d ω)) P.μ := (integrable_const C).mono' (hind_meas.mul hgYd_meas).aestronglyMeasurable (Filter.Eventually.of_forall (fun ω => by rw [Real.norm_eq_abs, abs_mul] have h1 : |S.dVar.indicator d ω| ≤ 1 := by rcases S.dVar.indicator_eq_one_or_zero d ω with h | h <;> rw [h] <;> simp calc |S.dVar.indicator d ω| * |g (S.YofD d ω)| ≤ 1 * C := mul_le_mul h1 (hg_bdd _) (abs_nonneg _) zero_le_one _ = C := one_mul _)) have hgYd_ipw_int : Integrable (fun ω => g (S.YofD d ω) * S.ipwDensity d ω) P.μ := by refine ((S.ipwDensity_integrable hA d).const_mul C).mono' (hgYd_meas.mul hipw_meas).aestronglyMeasurable ?_ filter_upwards [hipw_nn] with ω hω rw [Real.norm_eq_abs, abs_mul, abs_of_nonneg hω] exact mul_le_mul_of_nonneg_right (hg_bdd _) hω -- (a) Consistency: `g(Y)·ipw = g(Y(d))·ipw` (agree on `{D=d}`, both `0` off it). have hcons : (fun ω => g (S.factualY ω) * S.ipwDensity d ω) = (fun ω => g (S.YofD d ω) * S.ipwDensity d ω) := by funext ω by_cases hω : ω ∈ S.dVar.event d · have hcf : S.YofD d ω = S.factualY ω := POVar.cf_eq_factual_on_event hA.consistency S.yVar S.dVar d (Ne.symm S.hDY) hω rw [hcf] · have hind0 : S.dVar.indicator d ω = 0 := Set.indicator_of_notMem hω _ simp [POBackdoorSystem.ipwDensity, hind0] rw [hcons] -- (b) Conditional independence `Y(d) ⟂ D | σ(X)`, projected from unconfoundedness. let ψ : (∀ i : Fin S.cfBundle.n, S.cfBundle.type i) → ℝ := fun f => match d with | true => f (0 : Fin 2) | false => f (1 : Fin 2) have hψ_meas : Measurable ψ := by let instCf : ∀ a : Fin 2, MeasurableSpace (S.cfBundle.type a) := fun a => S.cfBundle.inst a cases d with | true => exact measurable_pi_apply (0 : Fin 2) | false => exact measurable_pi_apply (1 : Fin 2) have hYofD_eq : S.YofD d = ψ ∘ S.cfBundle.jointValue := by funext ω; cases d <;> rfl have hCI : CondIndepFun S.sigmaX S.sigmaX_le S.factualD (S.YofD d) P.μ := by have hproj := hA.unconfoundedness.project (ψ := ψ) hψ_meas rw [hYofD_eq]; exact hproj -- The set-indicator packaging `u (factualD ω) = 1_{D=d} ω`. let u : Bool → ℝ := ({d} : Set Bool).indicator (fun _ => (1 : ℝ)) have hu_meas : Measurable u := measurable_const.indicator (MeasurableSet.singleton d) have hu_eq : (fun ω => u (S.factualD ω)) = S.dVar.indicator d := by funext ω unfold POVar.indicator by_cases h : S.factualD ω = d · have h1 : S.factualD ω ∈ ({d} : Set Bool) := h have h2 : ω ∈ S.dVar.event d := h rw [show u (S.factualD ω) = (1 : ℝ) from Set.indicator_of_mem h1 _, Set.indicator_of_mem h2] · have h1 : S.factualD ω ∉ ({d} : Set Bool) := h have h2 : ω ∉ S.dVar.event d := h rw [show u (S.factualD ω) = (0 : ℝ) from Set.indicator_of_notMem h1 _, Set.indicator_of_notMem h2] -- (★) `E[1_{D=d}·g(Y(d)) | σX] =ᵐ e_d · E[g(Y(d)) | σX]`. have hstar0 := condExp_mul_of_condIndep (μ := P.μ) (m := S.sigmaX) S.sigmaX_le (f := S.factualD) (g := S.YofD d) S.measurable_factualD (S.measurable_YofD d) hCI (u := u) (v := g) hu_meas hg (by rw [hu_eq]; exact S.dVar.integrable_indicator d (measurableSet_singleton d)) hgYd_int (by have e1 : (fun ω => u (S.factualD ω) * g (S.YofD d ω)) = (fun ω => S.dVar.indicator d ω * g (S.YofD d ω)) := by funext ω; rw [congr_fun hu_eq ω] rw [e1]; exact prod_int) have hstar : P.μ[fun ω => S.dVar.indicator d ω * g (S.YofD d ω) | S.sigmaX] =ᵐ[P.μ] P.μ[S.dVar.indicator d | S.sigmaX] * P.μ[fun ω => g (S.YofD d ω) | S.sigmaX] := by have e1 : (fun ω => u (S.factualD ω) * g (S.YofD d ω)) = (fun ω => S.dVar.indicator d ω * g (S.YofD d ω)) := by funext ω; rw [congr_fun hu_eq ω] rw [e1, hu_eq] at hstar0 exact hstar0 -- (c) Pull the `σ(X)`-measurable factor `1/e_d` out and cancel. set k : P.Ω → ℝ := fun ω => 1 / S.propScore d ω with hk_def have hkey : (fun ω => g (S.YofD d ω) * S.ipwDensity d ω) = (fun ω => k ω * (S.dVar.indicator d ω * g (S.YofD d ω))) := by funext ω; simp only [hk_def, POBackdoorSystem.ipwDensity]; ring have kprod_int : Integrable (fun ω => k ω * (S.dVar.indicator d ω * g (S.YofD d ω))) P.μ := by rw [← hkey]; exact hgYd_ipw_int have hk_sm : StronglyMeasurable[S.sigmaX] k := by rw [hk_def] exact (measurable_const.div he_sm.measurable).stronglyMeasurable have hfin : P.μ[fun ω => k ω * (S.dVar.indicator d ω * g (S.YofD d ω)) | S.sigmaX] =ᵐ[P.μ] P.μ[fun ω => g (S.YofD d ω) | S.sigmaX] := by have hpull : P.μ[fun ω => k ω * (S.dVar.indicator d ω * g (S.YofD d ω)) | S.sigmaX] =ᵐ[P.μ] (fun ω => k ω * (P.μ[fun ω => S.dVar.indicator d ω * g (S.YofD d ω) | S.sigmaX]) ω) := by have h := MeasureTheory.condExp_mul_of_stronglyMeasurable_left (μ := P.μ) (m := S.sigmaX) (f := k) (g := fun ω => S.dVar.indicator d ω * g (S.YofD d ω)) hk_sm kprod_int prod_int filter_upwards [h] with ω hω; exact hω filter_upwards [hpull, hstar, he_pos] with ω h1 h2 hpos rw [h1] simp only [Pi.mul_apply] at h2 ⊢ rw [h2] have hps : (P.μ[S.dVar.indicator d | S.sigmaX]) ω = S.propScore d ω := rfl rw [hps] simp only [hk_def, one_div] exact inv_mul_cancel_left₀ hpos.ne' _ -- Assemble the integral chain via `∫ φ = ∫ E[φ | σX]`. rw [hkey, ← MeasureTheory.integral_condExp S.sigmaX_le (f := fun ω => g (S.YofD d ω)), ← MeasureTheory.integral_condExp S.sigmaX_le (f := fun ω => k ω * (S.dVar.indicator d ω * g (S.YofD d ω)))] exact MeasureTheory.integral_congr_ae hfin.symm

theorem cfUnderLaw_eq_ipwLaw [StandardBorelSpace P.Ω] [IsFiniteMeasure P.μ] (hA : S.DistributionalAssumptions) (d : Bool) : S.yVar.cfUnderLaw S.dVar d P.μ = S.ipwLaw d P.μ := by have hipw_int : Integrable (S.ipwDensity d) P.μ := S.ipwDensity_integrable hA d have hipw_nn : 0 ≤ᵐ[P.μ] S.ipwDensity d := by filter_upwards [S.propScore_pos hA d] with ω hω refine div_nonneg ?_ hω.le rcases S.dVar.indicator_eq_one_or_zero d ω with h | h <;> simp [h] -- Compare the two measures on every measurable set, via the `g = 1_s` transform. refine MeasureTheory.Measure.ext fun s hs => ?_ have hT_meas : MeasurableSet ((S.YofD d) ⁻¹' s) := S.measurable_YofD d hs have hU_meas : MeasurableSet (S.factualY ⁻¹' s) := S.measurable_factualY hs -- Bounded measurable test function `g = 1_s`. set g : ℝ → ℝ := s.indicator (fun _ => (1 : ℝ)) with hg_def have hg_meas : Measurable g := measurable_const.indicator hs have hg_bdd : ∀ y, |g y| ≤ 1 := by intro y by_cases hy : y ∈ s · simp [hg_def, Set.indicator_of_mem hy] · simp [hg_def, Set.indicator_of_notMem hy] -- `g ∘ Y(d)` and `g ∘ Y · ipw` rewritten as set indicators. have hcompYd : (fun ω => g (S.YofD d ω)) = ((S.YofD d) ⁻¹' s).indicator (fun _ => (1 : ℝ)) := by funext ω rw [hg_def] by_cases hω : S.YofD d ω ∈ s · rw [Set.indicator_of_mem hω, Set.indicator_of_mem (show ω ∈ (S.YofD d) ⁻¹' s from hω)] · rw [Set.indicator_of_notMem hω, Set.indicator_of_notMem (show ω ∉ (S.YofD d) ⁻¹' s from hω)] have hcompY : (fun ω => g (S.factualY ω) * S.ipwDensity d ω) = (S.factualY ⁻¹' s).indicator (S.ipwDensity d) := by funext ω by_cases hω : S.factualY ω ∈ s <;> simp [hg_def, hω] -- Express both sides as a preimage measure / set lintegral. have hLHS : S.yVar.cfUnderLaw S.dVar d P.μ s = P.μ ((S.YofD d) ⁻¹' s) := by change (P.μ.map (S.YofD d)) s = _ exact MeasureTheory.Measure.map_apply (S.measurable_YofD d) hs have hRHS : S.ipwLaw d P.μ s = ∫⁻ ω in (S.factualY ⁻¹' s), ofReal (S.ipwDensity d ω) ∂P.μ := by change ((P.μ.withDensity (fun ω => ofReal (S.ipwDensity d ω))).map S.factualY) s = _ rw [MeasureTheory.Measure.map_apply S.measurable_factualY hs, MeasureTheory.withDensity_apply _ hU_meas] -- Bochner-level identities. have key := S.integral_comp_YofD_eq hA d hg_meas hg_bdd have e_ind_Y : ∫ ω, g (S.factualY ω) * S.ipwDensity d ω ∂P.μ = ∫ ω in (S.factualY ⁻¹' s), S.ipwDensity d ω ∂P.μ := by rw [hcompY]; exact MeasureTheory.integral_indicator hU_meas have e_ind_Yd : ∫ ω, g (S.YofD d ω) ∂P.μ = (P.μ ((S.YofD d) ⁻¹' s)).toReal := by rw [hcompYd, MeasureTheory.integral_indicator hT_meas, MeasureTheory.integral_const, smul_eq_mul, mul_one, MeasureTheory.measureReal_restrict_apply_univ] rfl -- Glue everything through `ofReal`. have hchain : ∫⁻ ω in (S.factualY ⁻¹' s), ofReal (S.ipwDensity d ω) ∂P.μ = P.μ ((S.YofD d) ⁻¹' s) := by rw [← MeasureTheory.ofReal_integral_eq_lintegral_ofReal (hipw_int.restrict) (ae_restrict_of_ae hipw_nn), ← e_ind_Y, ← key, e_ind_Yd, ENNReal.ofReal_toReal (measure_ne_top P.μ _)] rw [hLHS, hRHS] exact hchain.symm

theorem qte_eq_of_law_eq (μ : Measure P.Ω) (τ : ℝ) {ν₁ ν₀ : Measure ℝ} (h₁ : S.yVar.cfUnderLaw S.dVar true μ = ν₁) (h₀ : S.yVar.cfUnderLaw S.dVar false μ = ν₀) : S.qte μ τ = quantile ν₁ τ - quantile ν₀ τ := by unfold qte rw [S.qtdQuantile_eq_quantile_cfUnderLaw true μ τ, S.qtdQuantile_eq_quantile_cfUnderLaw false μ τ, h₁, h₀]

theorem qte_backdoor [StandardBorelSpace P.Ω] [IsFiniteMeasure P.μ] (hA : S.Assumptions) (τ : ℝ) : S.qte P.μ τ = quantile (S.ipwLaw true P.μ) τ - quantile (S.ipwLaw false P.μ) τ := S.qte_eq_of_law_eq P.μ τ (S.cfUnderLaw_eq_ipwLaw hA.toDistributional true) (S.cfUnderLaw_eq_ipwLaw hA.toDistributional false)