PO.ID.Partial.Proxy.Helpers
Supporting lemmas for the proxy-based partial-identification results.
BridgeW 1 core · 0 supporting This file proves the W-only bridge-substitution identity used by the proximal partial-identification bounds. ★ condIntYofA_eq_h_arm
W-proxy bridge identity for partial identification
This file proves the W-only bridge-substitution identity used by the proximal partial-identification bounds. It reduces the off-arm counterfactual integral to an observable bridge-function integral under consistency, latent exchangeability, the W-proxy independence condition, and the outcome bridge.
lemma condIntYofA_eq_h_arm reviewed
⚑ flagged
Causalean.PO.POProximalSystem
Off-arm bridge-substitution identity (W-proxy). Fix a treatment arm a and assume the W-only proximal bridge assumption bundle — latent exchangeability of the potential outcome Y(a) given treatment conditional on the latent confounder and covariates, independence of the proxy W from treatment given that same conditioning, the outcome-bridge equation, and consistency — together with the treatment and outcome variables being distinct. Then, restricted to the off-arm stratum {A ≠ a}, the average potential outcome Y(a) equals the average of the bridge function h evaluated at (a, W, X): ∫_{A≠a} Y(a) dμ = ∫_{A≠a} h(a, W, X) dμ.
Formal statement
hypotheses
conclusion
(∫ ω in {ω | S.A ω ≠ a}, S.YofA a ω ∂μ)
= (∫ ω in {ω | S.A ω ≠ a}, HA.h (a, S.W ω, S.X ω) ∂μ)
Proof (Lean source)
lemma condIntYofA_eq_h_arm (HA : POProximalSystem.WBasedAssumptions S μ) (a : Bool)
(hAY : S.Avar.v ≠ S.Yvar.v) :
(∫ ω in {ω | S.A ω ≠ a}, S.YofA a ω ∂μ)
= (∫ ω in {ω | S.A ω ≠ a}, HA.h (a, S.W ω, S.X ω) ∂μ) := by
-- Set s' := {A ≠ a}. Strategy:
-- (A) ∫_{A≠a} Y(a) dμ = ∫_{A≠a} E[Y(a) | σ_AUX] dμ (tower, indic σ_AUX-meas)
-- = ∫_{A≠a} E[Y(a) | σ_UX] dμ (latent_exch_to_condExp')
-- (B) E[Y(a) | σ_UX] =ᵐ[μ] E[h(a,W,X) | σ_UX] (KEY STEP, see below)
-- ⇒ ∫_{A≠a} E[Y(a) | σ_UX] dμ = ∫_{A≠a} E[h(a,W,X) | σ_UX] dμ
-- (C) ∫_{A≠a} E[h(a,W,X) | σ_UX] dμ
-- = ∫_{A≠a} E[h(a,W,X) | σ_AUX] dμ (condExp_h_drop_A')
-- = ∫_{A≠a} h(a,W,X) dμ (tower again)
set s' : Set P.Ω := {ω | S.A ω ≠ a} with hs'_def
set s : Set P.Ω := {ω | S.A ω = a} with hs_def
have hs'_meas : MeasurableSet s' := by
have : MeasurableSet ({a} : Set Bool) := measurableSet_singleton a
have hsm : MeasurableSet s := S.measurable_A this
have h_compl : s' = sᶜ := by ext ω; simp [s', s]
rw [h_compl]; exact hsm.compl
have hs_meas : MeasurableSet s := S.measurable_A (measurableSet_singleton a)
-- s' is also σ_AUX-measurable (it's the preimage of {¬a} under projection (A,U,X) ↦ A).
have hs'_in_AUX : MeasurableSet[S.σ_AUX] s' := by
refine ⟨Prod.fst ⁻¹' {b : Bool | b ≠ a}, ?_, ?_⟩
· exact measurable_fst (MeasurableSet.compl (measurableSet_singleton a))
· ext ω; rfl
-- Integrability shortcuts.
have hYInt : Integrable S.Y μ := HA.integrable_Y
have hYaInt : Integrable (S.YofA a) μ := HA.integrable_YofA a
have hhArmInt : Integrable (fun ω => HA.h (a, S.W ω, S.X ω)) μ := HA.integrable_h_arm a
have hhAInt : Integrable (fun ω => HA.h (S.A ω, S.W ω, S.X ω)) μ := HA.integrable_h
have h_meas_haWX : Measurable (fun ω => HA.h (a, S.W ω, S.X ω)) := by
have hp : Measurable (fun ω : P.Ω => (a, S.W ω, S.X ω)) := by
exact prodMk measurable_const
(prodMk S.measurable_W S.measurable_X)
exact HA.measurable_h.comp hp
-- Helpers (primed versions, taking individual fields).
have hLatent : μ[S.YofA a | S.σ_AUX] =ᵐ[μ] μ[S.YofA a | S.σ_UX] :=
POProximalSystem.latent_exch_to_condExp' a (HA.latent_exch a) hYaInt
have hHdropA : μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AUX]
=ᵐ[μ] μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_UX] :=
POProximalSystem.condExp_h_drop_A' HA.proxy_WA HA.measurable_h a hhArmInt
-- ============================================================
-- (A) ∫_{A≠a} Y(a) dμ = ∫_{A≠a} E[Y(a) | σ_UX] dμ.
-- ============================================================
-- Step A.1: tower w.r.t. σ_AUX (since 1_{A≠a} is σ_AUX-meas).
-- ∫_{A≠a} Y(a) = ∫ 1_{A≠a} · Y(a) = ∫ E[1_{A≠a} · Y(a) | σ_AUX]
-- = ∫ 1_{A≠a} · E[Y(a) | σ_AUX] = ∫_{A≠a} E[Y(a) | σ_AUX].
have hStepA1 : (∫ ω in s', S.YofA a ω ∂μ)
= (∫ ω in s', (μ[S.YofA a | S.σ_AUX]) ω ∂μ) := by
-- Use `setIntegral_condExp` directly: ∫_t f = ∫_t E[f|m] for t ∈ m.
have := MeasureTheory.setIntegral_condExp (μ := μ) (m := S.σ_AUX) S.σ_AUX_le hYaInt hs'_in_AUX
-- This gives us ∫_t E[f|m] = ∫_t f, which we need to flip.
exact this.symm
-- Step A.2: replace E[Y(a) | σ_AUX] by E[Y(a) | σ_UX] via hLatent (a.e. global).
have hStepA2 : (∫ ω in s', (μ[S.YofA a | S.σ_AUX]) ω ∂μ)
= (∫ ω in s', (μ[S.YofA a | S.σ_UX]) ω ∂μ) :=
integral_congr_ae (ae_restrict_of_ae hLatent)
-- ============================================================
-- (C) ∫_{A≠a} h(a,W,X) dμ = ∫_{A≠a} E[h(a,W,X) | σ_UX] dμ. (mirror of A)
-- ============================================================
have hStepC1 : (∫ ω in s', HA.h (a, S.W ω, S.X ω) ∂μ)
= (∫ ω in s', (μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AUX]) ω ∂μ) := by
have := MeasureTheory.setIntegral_condExp (μ := μ) (m := S.σ_AUX) S.σ_AUX_le hhArmInt hs'_in_AUX
exact this.symm
have hStepC2 : (∫ ω in s', (μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AUX]) ω ∂μ)
= (∫ ω in s', (μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_UX]) ω ∂μ) :=
integral_congr_ae (ae_restrict_of_ae hHdropA)
-- ============================================================
-- (B) KEY STEP: E[Y(a) | σ_UX] =ᵐ[μ] E[h(a,W,X) | σ_UX] globally.
--
-- Derivation on {A=a}:
-- On {A=a}: by consistency, Y =ᵐ Y(a).
-- ⇒ E[Y | σ_AUX] =ᵐ[restrict {A=a}] E[Y(a) | σ_AUX] (consistency_event')
-- By bridge: E[Y - h(A,W,X) | σ_AUX] =ᵐ 0 globally
-- ⇒ E[Y | σ_AUX] =ᵐ[μ] E[h(A,W,X) | σ_AUX] (linearity)
-- On {A=a}: h(A,W,X) = h(a,W,X) pointwise
-- ⇒ E[h(A,W,X) | σ_AUX] =ᵐ[restrict {A=a}] E[h(a,W,X) | σ_AUX]
-- Combining, on {A=a}: E[Y(a) | σ_AUX] =ᵐ E[h(a,W,X) | σ_AUX].
-- Apply hLatent + hHdropA (a.e. globally, hence a.e. on restrict) to translate:
-- on {A=a}: E[Y(a) | σ_UX] =ᵐ E[h(a,W,X) | σ_UX].
--
-- Lift from {A=a} to globally μ-a.e. — this is the SUBTLE STEP.
-- Both LHS and RHS are σ_UX-measurable. Generally, equality on a set need
-- not lift to global, but if A ⫫ (relevant σ_UX content) suitably... this
-- needs additional structural assumption (e.g. positivity of pushforward
-- under σ_UX) that is not in the WBased bundle.
-- ============================================================
-- needs: σ_UX-measurable functions equal μ-a.e.-on-{A=a} are equal μ-a.e.,
-- assuming μ({A=a}) > 0 and the σ_UX-pushforward sees both arms.
have hKey : μ[S.YofA a | S.σ_UX]
=ᵐ[μ] μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_UX] := by
-- Both sides are σ_UX-measurable. We assemble a.e.-equality on
-- `{A = a}` (the factual arm) and lift via the abstract single-arm
-- a.e.-equality lemma `ae_eq_of_ae_eq_restrict_arm`.
--
-- Step 1: on {A=a}, by consistency, Y =ᵐ Y(a), hence
-- E[Y | σ_AUX] =ᵐ[restrict {A=a}] E[Y(a) | σ_AUX].
have hConsist : μ[S.Y | S.σ_AUX]
=ᵐ[μ.restrict {ω | S.A ω = a}] μ[S.YofA a | S.σ_AUX] :=
POProximalSystem.consistency_event'
HA.consistency a hAY hYInt hYaInt
-- Step 2: bridge equation gives μ[Y - h(A,W,X) | σ_AUX] =ᵐ 0 globally
-- ⇒ μ[Y | σ_AUX] =ᵐ μ[h(A,W,X) | σ_AUX] globally.
have hCEsub : μ[fun ω => S.Y ω - HA.h (S.A ω, S.W ω, S.X ω) | S.σ_AUX]
=ᵐ[μ] μ[S.Y | S.σ_AUX] - μ[fun ω => HA.h (S.A ω, S.W ω, S.X ω) | S.σ_AUX] :=
MeasureTheory.condExp_sub (m := S.σ_AUX) hYInt hhAInt
have hBridge : μ[S.Y | S.σ_AUX]
=ᵐ[μ] μ[fun ω => HA.h (S.A ω, S.W ω, S.X ω) | S.σ_AUX] := by
have h1 := hCEsub.symm.trans HA.bridge
filter_upwards [h1] with ω hω
have : (μ[S.Y | S.σ_AUX]) ω - (μ[fun ω => HA.h (S.A ω, S.W ω, S.X ω) | S.σ_AUX]) ω = 0 := by
simpa [Pi.sub_apply, Pi.zero_apply] using hω
linarith
-- Step 3: on {A=a}, h(A,W,X) = h(a,W,X) pointwise, hence
-- μ[h(A,W,X) | σ_AUX] =ᵐ[restrict {A=a}] μ[h(a,W,X) | σ_AUX].
have hh_eq_on_arm : (fun ω => HA.h (S.A ω, S.W ω, S.X ω))
=ᵐ[μ.restrict {ω | S.A ω = a}] (fun ω => HA.h (a, S.W ω, S.X ω)) := by
apply ae_restrict_of_forall_mem hs_meas
intro ω hω
have : S.A ω = a := hω
simp [this]
have hCE_h_eq : μ[fun ω => HA.h (S.A ω, S.W ω, S.X ω) | S.σ_AUX]
=ᵐ[μ.restrict {ω | S.A ω = a}]
μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AUX] := by
-- Strategy: use linearity. Set d := h(A,W,X) - h(a,W,X), which is
-- 0 a.e. on {A=a}, thus E[d | σ_AUX] =ᵐ 0 on {A=a} (via the same
-- consistency-event argument).
set d : P.Ω → ℝ := fun ω => HA.h (S.A ω, S.W ω, S.X ω) - HA.h (a, S.W ω, S.X ω)
have hdint : Integrable d μ := hhAInt.sub hhArmInt
have hd_zero_on_arm : d =ᵐ[μ.restrict {ω | S.A ω = a}] 0 := by
apply ae_restrict_of_forall_mem hs_meas
intro ω hω
have : S.A ω = a := hω
simp [d, this]
-- Reuse the indicator-trick.
have hs_in_m : MeasurableSet[S.σ_AUX] {ω | S.A ω = a} := by
refine ⟨Prod.fst ⁻¹' {a}, ?_, ?_⟩
· exact measurable_fst (measurableSet_singleton a)
· ext ω; rfl
have hind_zero : ({ω | S.A ω = a}).indicator d =ᵐ[μ] 0 := by
simpa using Causalean.indicator_aeEq_of_aeEq_restrict hs_meas hd_zero_on_arm
have hd_zero_cond : μ[d | S.σ_AUX] =ᵐ[μ.restrict {ω | S.A ω = a}] 0 := by
have hindCE_zero : ({ω | S.A ω = a}).indicator (μ[d | S.σ_AUX])
=ᵐ[μ] 0 := Causalean.condExp_indicator_aeEq_zero hs_in_m hdint hind_zero
have hindCE_zero' :
({ω | S.A ω = a}).indicator (μ[d | S.σ_AUX])
=ᵐ[μ] ({ω | S.A ω = a}).indicator (0 : P.Ω → ℝ) := by
simpa using hindCE_zero
simpa using Causalean.aeEq_restrict_of_indicator_aeEq hs_meas hindCE_zero'
have hCE_dsub : μ[d | S.σ_AUX]
=ᵐ[μ] μ[fun ω => HA.h (S.A ω, S.W ω, S.X ω) | S.σ_AUX]
- μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AUX] :=
MeasureTheory.condExp_sub (m := S.σ_AUX) hhAInt hhArmInt
have hCE_dsub_restrict :
μ[d | S.σ_AUX]
=ᵐ[μ.restrict {ω | S.A ω = a}]
μ[fun ω => HA.h (S.A ω, S.W ω, S.X ω) | S.σ_AUX]
- μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AUX] :=
ae_restrict_of_ae hCE_dsub
have hdiff_zero : (μ[fun ω => HA.h (S.A ω, S.W ω, S.X ω) | S.σ_AUX]
- μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AUX])
=ᵐ[μ.restrict {ω | S.A ω = a}] 0 :=
hCE_dsub_restrict.symm.trans hd_zero_cond
filter_upwards [hdiff_zero] with ω hω
have : (μ[fun ω => HA.h (S.A ω, S.W ω, S.X ω) | S.σ_AUX]) ω
- (μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AUX]) ω = 0 := by
simpa [Pi.sub_apply, Pi.zero_apply] using hω
linarith
-- Step 4: combine: on {A=a},
-- E[Y(a) | σ_AUX] =ᵐ E[Y | σ_AUX] =ᵐ E[h(A,W,X) | σ_AUX] =ᵐ E[h(a,W,X) | σ_AUX].
have hCE_eq_on_arm : μ[S.YofA a | S.σ_AUX]
=ᵐ[μ.restrict {ω | S.A ω = a}]
μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AUX] :=
(hConsist.symm.trans (ae_restrict_of_ae hBridge)).trans hCE_h_eq
-- Step 5: translate σ_AUX to σ_UX via hLatent and hHdropA (a.e. globally
-- ⇒ a.e. on restrict).
have hCE_UX_eq_on_arm : μ[S.YofA a | S.σ_UX]
=ᵐ[μ.restrict {ω | S.A ω = a}]
μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_UX] := by
have h1 : μ[S.YofA a | S.σ_AUX] =ᵐ[μ.restrict {ω | S.A ω = a}]
μ[S.YofA a | S.σ_UX] := ae_restrict_of_ae hLatent
have h2 : μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AUX]
=ᵐ[μ.restrict {ω | S.A ω = a}]
μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_UX] :=
ae_restrict_of_ae hHdropA
exact h1.symm.trans (hCE_eq_on_arm.trans h2)
-- Step 6: lift via the single-arm a.e.-equality support lemma.
-- Both sides are σ_UX-measurable.
have hf_m : Measurable[S.σ_UX] (μ[S.YofA a | S.σ_UX]) :=
MeasureTheory.stronglyMeasurable_condExp.measurable
have hg_m : Measurable[S.σ_UX] (μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_UX]) :=
MeasureTheory.stronglyMeasurable_condExp.measurable
exact ae_eq_of_ae_eq_restrict_arm (mΩ := P.measΩ)
S.σ_UX S.σ_UX_le
(measurableSet_eq_fun hf_m hg_m) hCE_UX_eq_on_arm (HA.overlap_strong a)
-- (B) integrated form.
have hStepB : (∫ ω in s', (μ[S.YofA a | S.σ_UX]) ω ∂μ)
= (∫ ω in s', (μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_UX]) ω ∂μ) :=
integral_congr_ae (ae_restrict_of_ae hKey)
-- Chain (A) → (B) → (C).
rw [hStepA1, hStepA2, hStepB, ← hStepC2, ← hStepC1]
BridgeWZ 1 core · 0 supporting This file proves the two-proxy bridge-substitution identity used in proximal partial identification. ★ condIntYofA_eq_hq_armSwap_twoProxy
Two-Proxy Bridge Substitution
This file proves the two-proxy bridge-substitution identity used in proximal partial identification. It represents the off-arm mean of the treatment-specific potential outcome as a same-arm integral of the outcome bridge multiplied by the treatment-side proxy bridge.
Under the probability-ratio convention for the proxy bridge, no separate stratum odds-ratio factor appears in this identity; that factor is recovered later after conditioning on the treatment and covariates. The proof follows the paper's sequence of latent exchangeability, outcome bridge substitution, likelihood-ratio arm swap, and proxy independence factorization.
lemma condIntYofA_eq_hq_armSwap_twoProxy reviewed
⚑ flagged
Causalean.PO.POProximalSystem
Two-proxy bridge-substitution identity, same-arm form (Ghassami-Shpitser-Tchetgen Tchetgen 2024, Theorem 3, equation (★), in the codebase's probability-ratio q convention). Fix a treatment arm a and assume the two-proxy bridge assumption bundle — consistency, latent exchangeability of Y(a), the likelihood-ratio arm-swap relation linking the off-arm and on-arm measures, the outcome bridge h, the treatment-proxy bridge q, and conditional independence of the two proxies W and Z given treatment and covariates — together with the treatment and outcome variables being distinct. Then the average potential outcome Y(a) over the off-arm stratum {A ≠ a} equals the on-arm average of the product of the outcome bridge h(a, W, X) and the treatment-proxy bridge q(Z, a, X): ∫_{A≠a} Y(a) dμ = ∫_{A=a} h(a, W, X) · q(Z, a, X) dμ.
Formal statement
hypotheses
conclusion
(∫ ω in {ω | S.A ω ≠ a}, S.YofA a ω ∂μ)
= ∫ ω in {ω | S.A ω = a}, HA.h (a, S.W ω, S.X ω) * HA.q (S.Z ω, a, S.X ω) ∂μ
Proof (Lean source)
lemma condIntYofA_eq_hq_armSwap_twoProxy
(HA : POProximalSystem.TwoProxyAssumptions S μ) (a : Bool)
(hAY : S.Avar.v ≠ S.Yvar.v) :
(∫ ω in {ω | S.A ω ≠ a}, S.YofA a ω ∂μ)
= ∫ ω in {ω | S.A ω = a},
HA.h (a, S.W ω, S.X ω) * HA.q (S.Z ω, a, S.X ω) ∂μ := by
-- Set up measurable sets and integrability shortcuts.
set s' : Set P.Ω := {ω | S.A ω ≠ a} with hs'_def
set s : Set P.Ω := {ω | S.A ω = a} with hs_def
have hs_meas : MeasurableSet s := S.measurable_A (measurableSet_singleton a)
have hs'_meas : MeasurableSet s' := by
have h_compl : s' = sᶜ := by ext ω; simp [s', s]
rw [h_compl]; exact hs_meas.compl
have hs_in_AUX : MeasurableSet[S.σ_AUX] s := by
refine ⟨Prod.fst ⁻¹' {a}, ?_, ?_⟩
· exact measurable_fst (measurableSet_singleton a)
· ext ω; rfl
have hs'_in_AUX : MeasurableSet[S.σ_AUX] s' := by
refine ⟨Prod.fst ⁻¹' {b : Bool | b ≠ a}, ?_, ?_⟩
· exact measurable_fst (MeasurableSet.compl (measurableSet_singleton a))
· ext ω; rfl
have hs_in_UX_Bool : MeasurableSet ({a} : Set Bool) := measurableSet_singleton a
-- Integrability shortcuts.
have hYInt : Integrable S.Y μ := HA.integrable_Y
have hYaInt : Integrable (S.YofA a) μ := HA.integrable_YofA a
have hhArmInt : Integrable (fun ω => HA.h (a, S.W ω, S.X ω)) μ :=
HA.integrable_h_arm a
have hhAInt : Integrable (fun ω => HA.h (S.A ω, S.W ω, S.X ω)) μ :=
HA.integrable_h
have hqInt : Integrable (fun ω => HA.q (S.Z ω, a, S.X ω)) μ := HA.integrable_q a
have hhqInt : Integrable
(fun ω => HA.h (a, S.W ω, S.X ω) * HA.q (S.Z ω, a, S.X ω)) μ :=
HA.integrable_hq_arm a
have hLInt : Integrable (HA.likelihoodRatio_swapA a) μ :=
HA.integrable_likelihoodRatio_swapA a
have hYaLInt : Integrable
(fun ω => (μ[S.YofA a | S.σ_UX]) ω * HA.likelihoodRatio_swapA a ω) μ :=
HA.integrable_condExpYofA_mul_L a
-- Measurabilities.
have h_meas_haWX : Measurable (fun ω => HA.h (a, S.W ω, S.X ω)) := by
have hp : Measurable (fun ω : P.Ω => (a, S.W ω, S.X ω)) :=
prodMk measurable_const
(prodMk S.measurable_W S.measurable_X)
exact HA.measurable_h.comp hp
have h_meas_qZaX : Measurable (fun ω => HA.q (S.Z ω, a, S.X ω)) := by
have hp : Measurable (fun ω : P.Ω => (S.Z ω, a, S.X ω)) :=
prodMk S.measurable_Z
(prodMk measurable_const S.measurable_X)
exact HA.measurable_q.comp hp
have hL_m : Measurable[S.σ_UX] (HA.likelihoodRatio_swapA a) :=
HA.measurable_likelihoodRatio_swapA a
-- ============================================================
-- (a) latent_exch + tower at σ_AUX:
-- ∫_{A≠a} Y(a) dμ = ∫_{A≠a} μ[Y(a) | σ_AUX] dμ
-- = ∫_{A≠a} μ[Y(a) | σ_UX] dμ.
-- ============================================================
have hLatent : μ[S.YofA a | S.σ_AUX] =ᵐ[μ] μ[S.YofA a | S.σ_UX] :=
POProximalSystem.latent_exch_to_condExp' a (HA.latent_exch a) hYaInt
have hStepA : (∫ ω in s', S.YofA a ω ∂μ)
= (∫ ω in s', (μ[S.YofA a | S.σ_UX]) ω ∂μ) := by
have h1 : (∫ ω in s', S.YofA a ω ∂μ)
= (∫ ω in s', (μ[S.YofA a | S.σ_AUX]) ω ∂μ) := by
have := MeasureTheory.setIntegral_condExp (μ := μ) (m := S.σ_AUX)
S.σ_AUX_le hYaInt hs'_in_AUX
exact this.symm
have h2 : (∫ ω in s', (μ[S.YofA a | S.σ_AUX]) ω ∂μ)
= (∫ ω in s', (μ[S.YofA a | S.σ_UX]) ω ∂μ) :=
integral_congr_ae (ae_restrict_of_ae hLatent)
exact h1.trans h2
-- ============================================================
-- (c) likelihoodRatio_swapA_spec change-of-measure:
-- ∫_{A≠a} μ[Y(a) | σ_UX] dμ
-- = ∫_{A=a} μ[Y(a) | σ_UX] · L dμ.
-- ============================================================
have hCondYa_meas : Measurable[S.σ_UX] (μ[S.YofA a | S.σ_UX]) :=
MeasureTheory.stronglyMeasurable_condExp.measurable
have hStepC : (∫ ω in s', (μ[S.YofA a | S.σ_UX]) ω ∂μ)
= (∫ ω in s, (μ[S.YofA a | S.σ_UX]) ω
* HA.likelihoodRatio_swapA a ω ∂μ) := by
-- Apply L2 with arms (a, ¬a). Needs a ≠ ¬a (true since Bool).
have h_swap := setIntegral_eq_setIntegral_mul_of_likelihoodRatio_swap
(m := S.σ_UX) (mΩ := P.measΩ) S.σ_UX_le s s'
hs_meas hs'_meas
(L := HA.likelihoodRatio_swapA a)
(f := μ[S.YofA a | S.σ_UX])
(hCondYa_meas.aestronglyMeasurable.mul hL_m.aestronglyMeasurable)
hCondYa_meas.aestronglyMeasurable
MeasureTheory.integrable_condExp.integrableOn hYaLInt.integrableOn
(by
-- Spec form: μ[1_{A=a}|σ_UX] · L =ᵐ μ[1_{A=¬a}|σ_UX].
have := HA.likelihoodRatio_swapA_spec a
simpa only [hs_def, hs'_def] using this)
-- h_swap : ∫_{A=¬a} f = ∫_{A=a} f * L.
exact h_swap
-- ============================================================
-- (b) On restrict {A=a}: μ[Y(a)|σ_UX] =ᵐ μ[h(a,W,X)|σ_AUX].
-- Chain:
-- μ[Y(a)|σ_UX] =ᵐ[μ] μ[Y(a)|σ_AUX] (latent_exch, global)
-- μ[Y(a)|σ_AUX] =ᵐ[restrict {A=a}] μ[Y|σ_AUX] (consistency_event' symm)
-- μ[Y|σ_AUX] =ᵐ[μ] μ[h(A,W,X)|σ_AUX] (bridge_h)
-- μ[h(A,W,X)|σ_AUX] =ᵐ[restrict {A=a}] μ[h(a,W,X)|σ_AUX] (h matches on arm)
-- ============================================================
-- Step b.1: μ[Y|σ_AUX] =ᵐ[μ] μ[h(A,W,X)|σ_AUX] globally.
have hCEsub : μ[fun ω => S.Y ω - HA.h (S.A ω, S.W ω, S.X ω) | S.σ_AUX]
=ᵐ[μ] μ[S.Y | S.σ_AUX]
- μ[fun ω => HA.h (S.A ω, S.W ω, S.X ω) | S.σ_AUX] :=
MeasureTheory.condExp_sub (m := S.σ_AUX) hYInt hhAInt
have hBridge_AUX : μ[S.Y | S.σ_AUX]
=ᵐ[μ] μ[fun ω => HA.h (S.A ω, S.W ω, S.X ω) | S.σ_AUX] := by
have h1 := hCEsub.symm.trans HA.bridge_h
filter_upwards [h1] with ω hω
have : (μ[S.Y | S.σ_AUX]) ω
- (μ[fun ω => HA.h (S.A ω, S.W ω, S.X ω) | S.σ_AUX]) ω = 0 := by
simpa [Pi.sub_apply, Pi.zero_apply] using hω
linarith
-- Step b.2: on restrict {A=a}, μ[h(A,W,X)|σ_AUX] =ᵐ μ[h(a,W,X)|σ_AUX].
have hCE_h_eq : μ[fun ω => HA.h (S.A ω, S.W ω, S.X ω) | S.σ_AUX]
=ᵐ[μ.restrict s] μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AUX] := by
set d : P.Ω → ℝ := fun ω => HA.h (S.A ω, S.W ω, S.X ω)
- HA.h (a, S.W ω, S.X ω)
have hdint : Integrable d μ := hhAInt.sub hhArmInt
have hd_zero_on_arm : d =ᵐ[μ.restrict s] 0 := by
apply ae_restrict_of_forall_mem hs_meas
intro ω hω
have : S.A ω = a := hω
simp [d, this]
have hind_zero : s.indicator d =ᵐ[μ] 0 := by
simpa using Causalean.indicator_aeEq_of_aeEq_restrict hs_meas hd_zero_on_arm
have hd_zero_cond : μ[d | S.σ_AUX] =ᵐ[μ.restrict s] 0 := by
have hindCE_zero : s.indicator (μ[d | S.σ_AUX]) =ᵐ[μ] 0 :=
Causalean.condExp_indicator_aeEq_zero hs_in_AUX hdint hind_zero
have hindCE_zero' :
s.indicator (μ[d | S.σ_AUX]) =ᵐ[μ] s.indicator (0 : P.Ω → ℝ) := by
simpa using hindCE_zero
simpa using Causalean.aeEq_restrict_of_indicator_aeEq hs_meas hindCE_zero'
have hCE_dsub : μ[d | S.σ_AUX]
=ᵐ[μ] μ[fun ω => HA.h (S.A ω, S.W ω, S.X ω) | S.σ_AUX]
- μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AUX] :=
MeasureTheory.condExp_sub (m := S.σ_AUX) hhAInt hhArmInt
have hCE_dsub_restrict : μ[d | S.σ_AUX]
=ᵐ[μ.restrict s]
μ[fun ω => HA.h (S.A ω, S.W ω, S.X ω) | S.σ_AUX]
- μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AUX] :=
ae_restrict_of_ae hCE_dsub
have hdiff_zero : (μ[fun ω => HA.h (S.A ω, S.W ω, S.X ω) | S.σ_AUX]
- μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AUX])
=ᵐ[μ.restrict s] 0 :=
hCE_dsub_restrict.symm.trans hd_zero_cond
filter_upwards [hdiff_zero] with ω hω
have : (μ[fun ω => HA.h (S.A ω, S.W ω, S.X ω) | S.σ_AUX]) ω
- (μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AUX]) ω = 0 := by
simpa [Pi.sub_apply, Pi.zero_apply] using hω
linarith
-- Step b.3: combine to get on restrict {A=a}:
-- μ[Y(a)|σ_UX] =ᵐ μ[h(a,W,X)|σ_AUX].
have hConsist : μ[S.Y | S.σ_AUX]
=ᵐ[μ.restrict s] μ[S.YofA a | S.σ_AUX] :=
POProximalSystem.consistency_event'
HA.consistency a hAY hYInt hYaInt
have hYa_AUX_eq_h_AUX : μ[S.YofA a | S.σ_AUX]
=ᵐ[μ.restrict s] μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AUX] :=
Filter.EventuallyEq.trans (Filter.EventuallyEq.symm hConsist)
(Filter.EventuallyEq.trans (ae_restrict_of_ae hBridge_AUX) hCE_h_eq)
have hYa_UX_eq_h_AUX : μ[S.YofA a | S.σ_UX]
=ᵐ[μ.restrict s] μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AUX] :=
Filter.EventuallyEq.trans
(Filter.EventuallyEq.symm (ae_restrict_of_ae hLatent))
hYa_AUX_eq_h_AUX
-- Substitute under integral on {A=a}.
have hStepB : (∫ ω in s, (μ[S.YofA a | S.σ_UX]) ω
* HA.likelihoodRatio_swapA a ω ∂μ)
= (∫ ω in s, (μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AUX]) ω
* HA.likelihoodRatio_swapA a ω ∂μ) := by
refine integral_congr_ae ?_
filter_upwards [hYa_UX_eq_h_AUX] with ω hω
rw [hω]
-- ============================================================
-- (b'/d) Replace L by μ[q(Z,a,X)|σ_AUX] (via bridge_q on restrict {A=a}),
-- then use proxy_WZ_indep to factor μ[h·q|σ_AUX] = μ[h|σ_AUX] · μ[q|σ_AUX]
-- and tower {A=a} ∈ σ_AUX to fold the integral back to ∫_{A=a} h·q.
-- ============================================================
-- Step d.1: bridge_q gives, on restrict {A=a},
-- L =ᵐ μ[q(Z,a,X)|σ_AUX].
have hBridgeQ : μ[fun ω => HA.q (S.Z ω, a, S.X ω) | S.σ_AUX]
=ᵐ[μ.restrict s] HA.likelihoodRatio_swapA a := HA.bridge_q a
have hStepD1 : (∫ ω in s, (μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AUX]) ω
* HA.likelihoodRatio_swapA a ω ∂μ)
= (∫ ω in s, (μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AUX]) ω
* (μ[fun ω => HA.q (S.Z ω, a, S.X ω) | S.σ_AUX]) ω ∂μ) := by
refine integral_congr_ae ?_
filter_upwards [hBridgeQ.symm] with ω hω
rw [hω]
-- Step d.2: proxy_WZ_indep + condExp_mul_of_condIndep to factor.
-- We need (W, X) ⟂ (Z, X) | σ_AUX. Apply prodMk-left twice (with symmetry).
have hX_m_AUX : Measurable[S.σ_AUX] S.X := by
-- X = (fun (p : Bool × γ_U × γ_X) => p.2.2) ∘ S.AUX, with σ_AUX = comap AUX.
intro t ht
refine ⟨(fun p : Bool × γ_U × γ_X => p.2.2) ⁻¹' t, ?_, ?_⟩
· exact (measurable_snd.comp measurable_snd) ht
· ext ω; rfl
-- Lift proxy_WZ_indep : W ⟂ Z | σ_AUX to (W,X) ⟂ Z | σ_AUX.
have hWX_Z : CondIndepFun S.σ_AUX S.σ_AUX_le
(fun ω => (S.W ω, S.X ω)) S.Z μ :=
condIndepFun_prodMk_of_measurable_left S.σ_AUX_le
S.measurable_W S.measurable_Z hX_m_AUX HA.proxy_WZ_indep
-- Symm: Z ⟂ (W,X) | σ_AUX.
have hZ_WX : CondIndepFun S.σ_AUX S.σ_AUX_le
S.Z (fun ω => (S.W ω, S.X ω)) μ := hWX_Z.symm
-- Lift to (Z,X) ⟂ (W,X) | σ_AUX.
have hZX_WX : CondIndepFun S.σ_AUX S.σ_AUX_le
(fun ω => (S.Z ω, S.X ω)) (fun ω => (S.W ω, S.X ω)) μ := by
have hWX_meas : Measurable (fun ω : P.Ω => (S.W ω, S.X ω)) :=
prodMk S.measurable_W S.measurable_X
exact condIndepFun_prodMk_of_measurable_left S.σ_AUX_le
S.measurable_Z hWX_meas hX_m_AUX hZ_WX
-- Symm again: (W,X) ⟂ (Z,X) | σ_AUX.
-- … truncated; follow the source link for the rest …
Common 1 core · 6 supporting This file provides reusable conditional-expectation and stratum-decomposition lemmas for W-based, Z-based, and two-proxy partial-identification bounds. ★ condExp_Y_eq_condExp_h_arm_AX_twoProxy
Common proximal-proxy partial-identification helpers
This file provides reusable conditional-expectation and stratum-decomposition lemmas for W-based, Z-based, and two-proxy partial-identification bounds. It connects bridge functions to observed conditional means and supplies a generic set-integral pull-out lemma for sigma-measurable factors.
lemma condExp_Y_eq_condExp_h_arm_AX_twoProxy reviewed
⚑ flagged
Causalean.PO.POProximalSystem
Fix a treatment arm a and assume the two-proxy bridge assumption bundle, with the treatment and outcome variables distinct. Then, restricted to the stratum {A = a}, the conditional expectation of the observed outcome Y given the σ-algebra generated by treatment and covariates equals the conditional expectation of the outcome bridge function evaluated at (a, W, X) given that same σ-algebra.
Formal statement
hypotheses
conclusion
μ[S.Y | S.σ_AX] =ᵐ[μ.restrict {ω | S.A ω = a}] μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AX]
Proof (Lean source)
lemma condExp_Y_eq_condExp_h_arm_AX_twoProxy
(HA : POProximalSystem.TwoProxyAssumptions S μ) (a : Bool)
(_hAY : S.Avar.v ≠ S.Yvar.v) :
μ[S.Y | S.σ_AX]
=ᵐ[μ.restrict {ω | S.A ω = a}]
μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AX] :=
condExp_Y_eq_condExp_h_arm_AX_core (h := HA.h) a
HA.integrable_Y HA.integrable_h (HA.integrable_h_arm a) HA.bridge_h
6 supporting declarations (lemmas, instances)
-
meanYofA_eq_stratalemma — E[Y(a)] = ∫_{A = ¬a} Y(a) dμ + ∫_{A = a} Y dμ. Combines the stratum decomposition μ = μ.restrict {A=a} + μ.restrict {A=¬a} with consistency on the {A = a} arm.hypothesesconclusionS.meanYofA μ a= (∫ ω in {ω | S.A ω ≠ a}, S.YofA a ω ∂μ) + (∫ ω in {ω | S.A ω = a}, S.Y ω ∂μ)Proof (Lean source)
lemma meanYofA_eq_strata (HC : POSystem.Consistency P) (a : Bool) (hAY : S.Avar.v ≠ S.Yvar.v) (hYofA : Integrable (S.YofA a) μ) : S.meanYofA μ a = (∫ ω in {ω | S.A ω ≠ a}, S.YofA a ω ∂μ) + (∫ ω in {ω | S.A ω = a}, S.Y ω ∂μ) := by -- Step 1: split the unrestricted integral by the partition {A = a} ∪ {A ≠ a}. have hs_meas : MeasurableSet {ω : P.Ω | S.A ω = a} := S.measurable_A (measurableSet_singleton a) have hsplit : S.meanYofA μ a = (∫ ω in {ω | S.A ω = a}, S.YofA a ω ∂μ) + (∫ ω in {ω | S.A ω ≠ a}, S.YofA a ω ∂μ) := by have := MeasureTheory.integral_add_compl (μ := μ) (f := S.YofA a) hs_meas hYofA have hcompl : ({ω : P.Ω | S.A ω = a})ᶜ = {ω | S.A ω ≠ a} := by ext ω; simp simp only [POProximalSystem.meanYofA] at * rw [← this, hcompl] -- Step 2: on {A = a}, Y(a) =ᵐ Y by consistency. have hYeq : S.YofA a =ᵐ[μ.restrict {ω | S.A ω = a}] S.Y := by apply ae_restrict_of_forall_mem hs_meas intro ω hω exact POVar.cf_eq_factual_on_event HC S.Yvar S.Avar a hAY.symm hω have hint_eq : (∫ ω in {ω | S.A ω = a}, S.YofA a ω ∂μ) = (∫ ω in {ω | S.A ω = a}, S.Y ω ∂μ) := integral_congr_ae hYeq rw [hsplit, hint_eq, add_comm] -
YofA_essbound_abovelemma — Y(a) inherits Y's a.e. upper bound under latent exchangeability and consistency. Requires overlap_strong: every σ_UX-measurable null-on-{A=a} set is globally null, so the single-arm bound lifts globally.hypothesesa :HC :POSystem.Consistency Platent_exch :CondIndepFun S.σ_UX S.σ_UX_le (S.YofA a) S.A μhAY :S.Avar.v ≠ S.Yvar.voverlap :∀ s : Set P.ΩM :ℝhY :∀ᵐ ω ∂μ, S.Y ω ≤ Mconclusion∀ᵐ ω ∂μ, S.YofA a ω ≤ MProof (Lean source)
lemma YofA_essbound_above {a : Bool} (HC : POSystem.Consistency P) (latent_exch : CondIndepFun S.σ_UX S.σ_UX_le (S.YofA a) S.A μ) (hAY : S.Avar.v ≠ S.Yvar.v) (overlap : ∀ s : Set P.Ω, MeasurableSet[S.σ_UX] s → μ (s ∩ {ω | S.A ω = a}) = 0 → μ s = 0) {M : ℝ} (hY : ∀ᵐ ω ∂μ, S.Y ω ≤ M) : ∀ᵐ ω ∂μ, S.YofA a ω ≤ M := by have hYeq : S.Y =ᵐ[μ.restrict {ω | S.A ω = a}] S.YofA a := by have hs : MeasurableSet {ω : P.Ω | S.A ω = a} := S.measurable_A (measurableSet_singleton a) apply ae_restrict_of_forall_mem hs intro ω hω exact (POVar.cf_eq_factual_on_event HC S.Yvar S.Avar a hAY.symm hω).symm exact ae_le_YofA_of_ae_le_Y (mΩ := P.measΩ) (σ_UX := S.σ_UX) S.σ_UX_le S.measurable_A (S.measurable_YofA a) a latent_exch hYeq overlap hY -
YofA_essbound_belowlemma — Y(a) inherits Y's a.e. lower bound. Mirror of YofA_essbound_above.hypothesesa :HC :POSystem.Consistency Platent_exch :CondIndepFun S.σ_UX S.σ_UX_le (S.YofA a) S.A μhAY :S.Avar.v ≠ S.Yvar.voverlap :∀ s : Set P.ΩM :ℝhY :∀ᵐ ω ∂μ, M ≤ S.Y ωconclusion∀ᵐ ω ∂μ, M ≤ S.YofA a ωProof (Lean source)
lemma YofA_essbound_below {a : Bool} (HC : POSystem.Consistency P) (latent_exch : CondIndepFun S.σ_UX S.σ_UX_le (S.YofA a) S.A μ) (hAY : S.Avar.v ≠ S.Yvar.v) (overlap : ∀ s : Set P.Ω, MeasurableSet[S.σ_UX] s → μ (s ∩ {ω | S.A ω = a}) = 0 → μ s = 0) {M : ℝ} (hY : ∀ᵐ ω ∂μ, M ≤ S.Y ω) : ∀ᵐ ω ∂μ, M ≤ S.YofA a ω := by have hYeq : S.Y =ᵐ[μ.restrict {ω | S.A ω = a}] S.YofA a := by have hs : MeasurableSet {ω : P.Ω | S.A ω = a} := S.measurable_A (measurableSet_singleton a) apply ae_restrict_of_forall_mem hs intro ω hω exact (POVar.cf_eq_factual_on_event HC S.Yvar S.Avar a hAY.symm hω).symm exact ae_le_YofA_of_ae_le_Y_below (mΩ := P.measΩ) (σ_UX := S.σ_UX) S.σ_UX_le S.measurable_A (S.measurable_YofA a) a latent_exch hYeq overlap hY -
condExp_Y_eq_condExp_h_arm_AX_corelemma — Core observed-data collapse identity (no assumption-bundle dependency).hypothesesh :Bool × γ_W × γ_X → ℝa :hYInt :Integrable S.Y μhhAInt :Integrable (fun ω => h (S.A ω, S.W ω, S.X ω)) μhhArmInt :Integrable (fun ω => h (a, S.W ω, S.X ω)) μhbridge :(μ[fun ω => S.Y ω - h (S.A ω, S.W ω, S.X ω) | S.σ_AUX]) =ᵐ[μ] 0conclusionμ[S.Y | S.σ_AX] =ᵐ[μ.restrict {ω | S.A ω = a}] μ[fun ω => h (a, S.W ω, S.X ω) | S.σ_AX]Proof (Lean source)
lemma condExp_Y_eq_condExp_h_arm_AX_core {h : Bool × γ_W × γ_X → ℝ} (a : Bool) (hYInt : Integrable S.Y μ) (hhAInt : Integrable (fun ω => h (S.A ω, S.W ω, S.X ω)) μ) (hhArmInt : Integrable (fun ω => h (a, S.W ω, S.X ω)) μ) (hbridge : (μ[fun ω => S.Y ω - h (S.A ω, S.W ω, S.X ω) | S.σ_AUX]) =ᵐ[μ] 0) : μ[S.Y | S.σ_AX] =ᵐ[μ.restrict {ω | S.A ω = a}] μ[fun ω => h (a, S.W ω, S.X ω) | S.σ_AX] := by have hs_meas : MeasurableSet {ω : P.Ω | S.A ω = a} := S.measurable_A (measurableSet_singleton a) -- Step 1: bridge equation gives μ[Y | σ_AUX] =ᵐ[μ] μ[h(A,W,X) | σ_AUX] globally. have hCEsub : μ[fun ω => S.Y ω - h (S.A ω, S.W ω, S.X ω) | S.σ_AUX] =ᵐ[μ] μ[S.Y | S.σ_AUX] - μ[fun ω => h (S.A ω, S.W ω, S.X ω) | S.σ_AUX] := MeasureTheory.condExp_sub (m := S.σ_AUX) hYInt hhAInt have hBridge_AUX : μ[S.Y | S.σ_AUX] =ᵐ[μ] μ[fun ω => h (S.A ω, S.W ω, S.X ω) | S.σ_AUX] := by have h1 := hCEsub.symm.trans hbridge filter_upwards [h1] with ω hω have : (μ[S.Y | S.σ_AUX]) ω - (μ[fun ω => h (S.A ω, S.W ω, S.X ω) | S.σ_AUX]) ω = 0 := by simpa [Pi.sub_apply, Pi.zero_apply] using hω linarith -- Step 2: on {A=a}, h(A,W,X) = h(a,W,X), hence -- μ[h(A,W,X) | σ_AUX] =ᵐ[restrict {A=a}] μ[h(a,W,X) | σ_AUX]. -- Indicator-zero argument (same pattern as `BridgeW.lean`'s `hCE_h_eq`). have hCE_h_eq : μ[fun ω => h (S.A ω, S.W ω, S.X ω) | S.σ_AUX] =ᵐ[μ.restrict {ω | S.A ω = a}] μ[fun ω => h (a, S.W ω, S.X ω) | S.σ_AUX] := by set d : P.Ω → ℝ := fun ω => h (S.A ω, S.W ω, S.X ω) - h (a, S.W ω, S.X ω) have hdint : Integrable d μ := hhAInt.sub hhArmInt have hd_zero_on_arm : d =ᵐ[μ.restrict {ω | S.A ω = a}] 0 := by apply ae_restrict_of_forall_mem hs_meas intro ω hω have : S.A ω = a := hω simp [d, this] have hs_in_m : MeasurableSet[S.σ_AUX] {ω | S.A ω = a} := by refine ⟨Prod.fst ⁻¹' {a}, ?_, ?_⟩ · exact measurable_fst (measurableSet_singleton a) · ext ω; rfl have hind_zero : ({ω | S.A ω = a}).indicator d =ᵐ[μ] 0 := by simpa using Causalean.indicator_aeEq_of_aeEq_restrict hs_meas hd_zero_on_arm have hd_zero_cond : μ[d | S.σ_AUX] =ᵐ[μ.restrict {ω | S.A ω = a}] 0 := by have hindCE_zero : ({ω | S.A ω = a}).indicator (μ[d | S.σ_AUX]) =ᵐ[μ] 0 := Causalean.condExp_indicator_aeEq_zero hs_in_m hdint hind_zero have hindCE_zero' : ({ω | S.A ω = a}).indicator (μ[d | S.σ_AUX]) =ᵐ[μ] ({ω | S.A ω = a}).indicator (0 : P.Ω → ℝ) := by simpa using hindCE_zero simpa using Causalean.aeEq_restrict_of_indicator_aeEq hs_meas hindCE_zero' have hCE_dsub : μ[d | S.σ_AUX] =ᵐ[μ] μ[fun ω => h (S.A ω, S.W ω, S.X ω) | S.σ_AUX] - μ[fun ω => h (a, S.W ω, S.X ω) | S.σ_AUX] := MeasureTheory.condExp_sub (m := S.σ_AUX) hhAInt hhArmInt have hCE_dsub_restrict : μ[d | S.σ_AUX] =ᵐ[μ.restrict {ω | S.A ω = a}] μ[fun ω => h (S.A ω, S.W ω, S.X ω) | S.σ_AUX] - μ[fun ω => h (a, S.W ω, S.X ω) | S.σ_AUX] := ae_restrict_of_ae hCE_dsub have hdiff_zero : (μ[fun ω => h (S.A ω, S.W ω, S.X ω) | S.σ_AUX] - μ[fun ω => h (a, S.W ω, S.X ω) | S.σ_AUX]) =ᵐ[μ.restrict {ω | S.A ω = a}] 0 := hCE_dsub_restrict.symm.trans hd_zero_cond filter_upwards [hdiff_zero] with ω hω have : (μ[fun ω => h (S.A ω, S.W ω, S.X ω) | S.σ_AUX]) ω - (μ[fun ω => h (a, S.W ω, S.X ω) | S.σ_AUX]) ω = 0 := by simpa [Pi.sub_apply, Pi.zero_apply] using hω linarith -- Step 3: combine to get μ[Y | σ_AUX] =ᵐ[restrict {A=a}] μ[h(a,W,X) | σ_AUX]. have hBridge_AUX_arm : μ[S.Y | S.σ_AUX] =ᵐ[μ.restrict {ω | S.A ω = a}] μ[fun ω => h (S.A ω, S.W ω, S.X ω) | S.σ_AUX] := ae_restrict_of_ae hBridge_AUX have hY_h_AUX : μ[S.Y | S.σ_AUX] =ᵐ[μ.restrict {ω | S.A ω = a}] μ[fun ω => h (a, S.W ω, S.X ω) | S.σ_AUX] := Filter.EventuallyEq.trans hBridge_AUX_arm hCE_h_eq -- Step 4: apply tower property `condExp_condExp_of_le` with σ_AX ≤ σ_AUX -- to bring both sides down to σ_AX. -- μ[μ[Y | σ_AUX] | σ_AX] = μ[Y | σ_AX] globally (a.e.). Same for the h-side. have hAX_le_AUX : S.σ_AX ≤ S.σ_AUX := S.σ_AX_le_σ_AUX have hY_tower : μ[μ[S.Y | S.σ_AUX] | S.σ_AX] =ᵐ[μ] μ[S.Y | S.σ_AX] := MeasureTheory.condExp_condExp_of_le (m₁ := S.σ_AX) (m₂ := S.σ_AUX) hAX_le_AUX S.σ_AUX_le have hh_tower : μ[μ[fun ω => h (a, S.W ω, S.X ω) | S.σ_AUX] | S.σ_AX] =ᵐ[μ] μ[fun ω => h (a, S.W ω, S.X ω) | S.σ_AX] := MeasureTheory.condExp_condExp_of_le (m₁ := S.σ_AX) (m₂ := S.σ_AUX) hAX_le_AUX S.σ_AUX_le -- The σ_AUX-conditional expectations coincide a.e. on {A = a}; we lift this -- through the σ_AX tower. The set {A = a} is σ_AX-measurable, and applying -- `condExp_congr_ae` over the restricted measure converts the `{A=a}`-a.e. -- equality of σ_AUX-CE's to a `{A=a}`-a.e. equality of their σ_AX-CE's via -- `setIntegral_condExp` would be a heavy detour. Simpler: use the indicator -- trick at σ_AX level too. -- -- Step 4 (clean form): apply the indicator trick directly to bring the -- σ_AUX-equality on {A=a} to a σ_AX-equality on {A=a}. Set -- D := μ[Y | σ_AUX] - μ[h(a,W,X) | σ_AUX]. -- We have D =ᵐ[restrict {A=a}] 0. Hence indicator_{A=a} D =ᵐ[μ] 0, so -- E[indicator_{A=a} D | σ_AX] =ᵐ[μ] 0 -- = indicator_{A=a} · E[D | σ_AX] (since {A=a} ∈ σ_AX) -- Applying tower again: E[D | σ_AX] = μ[Y | σ_AX] - μ[h(a,W,X) | σ_AX] a.e. -- So indicator_{A=a} · (μ[Y | σ_AX] - μ[h(a,W,X) | σ_AX]) =ᵐ[μ] 0, -- which yields the desired restrict-{A=a} equality. set f1 : P.Ω → ℝ := μ[S.Y | S.σ_AUX] set f2 : P.Ω → ℝ := μ[fun ω => h (a, S.W ω, S.X ω) | S.σ_AUX] set D : P.Ω → ℝ := f1 - f2 have hf1_int : Integrable f1 μ := MeasureTheory.integrable_condExp have hf2_int : Integrable f2 μ := MeasureTheory.integrable_condExp have hD_int : Integrable D μ := hf1_int.sub hf2_int have hD_zero_on_arm : D =ᵐ[μ.restrict {ω | S.A ω = a}] 0 := by filter_upwards [hY_h_AUX] with ω hω simp [D, f1, f2, Pi.sub_apply, hω] have hs_in_AX : MeasurableSet[S.σ_AX] {ω | S.A ω = a} := by refine ⟨Prod.fst ⁻¹' {a}, ?_, ?_⟩ · exact measurable_fst (measurableSet_singleton a) · ext ω; rfl have hind_D_zero : ({ω | S.A ω = a}).indicator D =ᵐ[μ] 0 := by simpa using Causalean.indicator_aeEq_of_aeEq_restrict hs_meas hD_zero_on_arm have hD_zero_AX : μ[D | S.σ_AX] =ᵐ[μ.restrict {ω | S.A ω = a}] 0 := by have hindCE_zero : ({ω | S.A ω = a}).indicator (μ[D | S.σ_AX]) =ᵐ[μ] 0 := Causalean.condExp_indicator_aeEq_zero hs_in_AX hD_int hind_D_zero have hindCE_zero' : ({ω | S.A ω = a}).indicator (μ[D | S.σ_AX]) =ᵐ[μ] ({ω | S.A ω = a}).indicator (0 : P.Ω → ℝ) := by simpa using hindCE_zero simpa using Causalean.aeEq_restrict_of_indicator_aeEq hs_meas hindCE_zero' -- Decompose μ[D | σ_AX] = μ[f1 | σ_AX] - μ[f2 | σ_AX] and apply tower. have hCE_Dsub : μ[D | S.σ_AX] =ᵐ[μ] μ[f1 | S.σ_AX] - μ[f2 | S.σ_AX] := MeasureTheory.condExp_sub (m := S.σ_AX) hf1_int hf2_int have hf1_AX_eq : μ[f1 | S.σ_AX] =ᵐ[μ] μ[S.Y | S.σ_AX] := hY_tower have hf2_AX_eq : μ[f2 | S.σ_AX] =ᵐ[μ] μ[fun ω => h (a, S.W ω, S.X ω) | S.σ_AX] := hh_tower have hCE_Dsub_AX : μ[D | S.σ_AX] =ᵐ[μ] μ[S.Y | S.σ_AX] - μ[fun ω => h (a, S.W ω, S.X ω) | S.σ_AX] := by refine hCE_Dsub.trans ?_ filter_upwards [hf1_AX_eq, hf2_AX_eq] with ω h1 h2 simp [Pi.sub_apply, h1, h2] -- Combine with hD_zero_AX (over the restricted measure). have hCE_Dsub_AX_arm : μ[D | S.σ_AX] =ᵐ[μ.restrict {ω | S.A ω = a}] μ[S.Y | S.σ_AX] - μ[fun ω => h (a, S.W ω, S.X ω) | S.σ_AX] := ae_restrict_of_ae hCE_Dsub_AX have hdiff_zero_AX : (μ[S.Y | S.σ_AX] - μ[fun ω => h (a, S.W ω, S.X ω) | S.σ_AX]) =ᵐ[μ.restrict {ω | S.A ω = a}] 0 := Filter.EventuallyEq.trans (Filter.EventuallyEq.symm hCE_Dsub_AX_arm) hD_zero_AX filter_upwards [hdiff_zero_AX] with ω hω have : (μ[S.Y | S.σ_AX]) ω - (μ[fun ω => h (a, S.W ω, S.X ω) | S.σ_AX]) ω = 0 := by simpa [Pi.sub_apply, Pi.zero_apply] using hω linarith -
condExp_Y_eq_condExp_h_arm_AXlemma — In the W-proxy bundle, the observed conditional mean of the outcome equals the conditional mean of the bridge function on the matching treatment arm.hypothesesconclusionμ[S.Y | S.σ_AX] =ᵐ[μ.restrict {ω | S.A ω = a}] μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AX]Proof (Lean source)
lemma condExp_Y_eq_condExp_h_arm_AX (HA : POProximalSystem.WBasedAssumptions S μ) (a : Bool) (_hAY : S.Avar.v ≠ S.Yvar.v) : μ[S.Y | S.σ_AX] =ᵐ[μ.restrict {ω | S.A ω = a}] μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AX] := condExp_Y_eq_condExp_h_arm_AX_core (h := HA.h) a HA.integrable_Y HA.integrable_h (HA.integrable_h_arm a) HA.bridge -
setIntegral_mul_condExp_of_stronglyMeasurableLeftlemma — A sigma-measurable left factor can be pulled through conditional expectation inside a set integral over a measurable event.∀ {Ω : Type u_1} {m mΩ : MeasurableSpace Ω}, m ≤ mΩ → ∀ {μ : Measure Ω} [IsFiniteMeasure μ] {f g : Ω → ℝ}, StronglyMeasurable f → Integrable g μ → Integrable (f * g) μ → ∀ {s : Set Ω}, MeasurableSet s → ∫ (ω : Ω) in s, f ω * g ω ∂μ = ∫ (ω : Ω) in s, f ω * μ[g | m] ω ∂μProof (Lean source)
lemma setIntegral_mul_condExp_of_stronglyMeasurableLeft {Ω} {m mΩ : MeasurableSpace Ω} (hm : m ≤ mΩ) {μ : Measure Ω} [IsFiniteMeasure μ] {f g : Ω → ℝ} (hf_sm : StronglyMeasurable[m] f) (hg_int : Integrable g μ) (hfg_int : Integrable (f * g) μ) {s : Set Ω} (hs_m : MeasurableSet[m] s) : ∫ ω in s, f ω * g ω ∂μ = ∫ ω in s, f ω * (μ[g | m]) ω ∂μ := by -- Step 1: pull-out a.e. equality. have h_pull : (μ[f * g | m]) =ᵐ[μ] f * μ[g | m] := condExp_mul_of_stronglyMeasurable_left hf_sm hfg_int hg_int -- Step 2: setIntegral_condExp on the m-measurable set s. have h_setInt : ∫ ω in s, (μ[f * g | m]) ω ∂μ = ∫ ω in s, (f * g) ω ∂μ := setIntegral_condExp hm hfg_int hs_m -- Step 3: integral_congr_ae for the pull-out, restricted to s. have h_pull_restrict : (μ[f * g | m]) =ᵐ[μ.restrict s] (f * μ[g | m]) := ae_restrict_of_ae h_pull have h_congr : ∫ ω in s, (μ[f * g | m]) ω ∂μ = ∫ ω in s, (f * μ[g | m]) ω ∂μ := integral_congr_ae h_pull_restrict -- Combine. have h_eq := h_setInt.symm.trans h_congr -- h_eq : ∫_s (f*g) = ∫_s (f * μ[g|m]); rewrite Pi.mul_apply. simpa [Pi.mul_apply] using h_eq
CondExpQ 1 core · 0 supporting This file derives the conditional-expectation identity that connects the treatment bridge q to the observable stratum odds ratio. ★ condExp_q_eq_stratumOddsRatio_arm_AX
Conditional-expectation identities for treatment bridges
This file derives the conditional-expectation identity that connects the
treatment bridge q to the observable stratum odds ratio. The result is used by
the two-proxy partial-identification envelope chain to eliminate the latent
treatment bridge from the public bound.
lemma condExp_q_eq_stratumOddsRatio_arm_AX reviewed
⚑ flagged
Causalean.PO.POProximalSystem
q-collapse on the on-arm σ(A,X) (TwoProxy). Fix a treatment arm a and assume the two-proxy bridge assumption bundle, with the treatment and outcome variables distinct. Under the probability-ratio convention for the treatment-proxy bridge q encoded by likelihoodRatio_swapA_spec, restricted to the stratum {A = a}, the conditional expectation of q(Z, a, X) given the σ-algebra generated by treatment and covariates collapses to the σ(X)-measurable stratum odds ratio p(A≠a∣X)/p(A=a∣X):
Formal statement
hypotheses
conclusion
(μ[fun ω => HA.q (S.Z ω, a, S.X ω) | S.σ_AX])
=ᵐ[μ.restrict {ω | S.A ω = a}] S.stratumOddsRatio μ a
Proof (Lean source)
lemma condExp_q_eq_stratumOddsRatio_arm_AX
(HA : POProximalSystem.TwoProxyAssumptions S μ) (a : Bool)
(_hAY : S.Avar.v ≠ S.Yvar.v) :
(μ[fun ω => HA.q (S.Z ω, a, S.X ω) | S.σ_AX])
=ᵐ[μ.restrict {ω | S.A ω = a}]
S.stratumOddsRatio μ a := by
-- Notation.
set q' : P.Ω → ℝ := fun ω => HA.q (S.Z ω, a, S.X ω) with hq'_def
set L_a : P.Ω → ℝ := HA.likelihoodRatio_swapA a with hLa_def
set R : P.Ω → ℝ := S.stratumOddsRatio μ a with hR_def
set ind : P.Ω → ℝ := indicator {ω' | S.A ω' = a} (fun _ => (1:ℝ)) with hind_def
-- Basic measurability / integrability facts.
have hs_meas : MeasurableSet {ω : P.Ω | S.A ω = a} :=
S.measurable_A (measurableSet_singleton a)
have hs_in_AX : MeasurableSet[S.σ_AX] {ω | S.A ω = a} := by
refine ⟨Prod.fst ⁻¹' {a}, ?_, ?_⟩
· exact measurable_fst (measurableSet_singleton a)
· ext ω; rfl
have hs_in_AUX : MeasurableSet[S.σ_AUX] {ω | S.A ω = a} :=
S.σ_AX_le_σ_AUX _ hs_in_AX
have hq'_int : Integrable q' μ := HA.integrable_q a
have hLa_int : Integrable L_a μ := HA.integrable_likelihoodRatio_swapA a
have hLa_m_UX : Measurable[S.σ_UX] L_a := HA.measurable_likelihoodRatio_swapA a
-- ind is bounded by 1 and σ_AX-measurable (lifts to mΩ).
have hind_meas_AX : Measurable[S.σ_AX] ind := by
refine Measurable.indicator (m := S.σ_AX) measurable_const ?_
exact hs_in_AX
have hind_meas : Measurable ind := hind_meas_AX.mono S.σ_AX_le le_rfl
have hind_le : ∀ ω, ‖ind ω‖ ≤ 1 := by
intro ω; by_cases h : ω ∈ {ω' | S.A ω' = a}
· simp [ind, Set.indicator_of_mem h]
· simp [ind, Set.indicator_of_notMem h]
have hind_int : Integrable ind μ := by
refine (integrable_const (1 : ℝ)).mono' hind_meas.aestronglyMeasurable ?_
exact Filter.Eventually.of_forall (by intro ω; simpa using hind_le ω)
-- f := ind * q', g := ind * R.
set f : P.Ω → ℝ := fun ω => ind ω * q' ω with hf_def
set g : P.Ω → ℝ := fun ω => ind ω * R ω with hg_def
-- Integrability of f via boundedness of ind.
have hf_int : Integrable f μ := by
refine hq'_int.bdd_mul (c := 1) hind_meas.aestronglyMeasurable ?_
exact Filter.Eventually.of_forall hind_le
-- R is σ_X-measurable (hence σ_AX-meas, σ_AUX-meas).
have hR_meas_X : Measurable[S.σ_X] R := by
have := stronglyMeasurable_condExp (m := S.σ_X) (μ := μ)
(f := indicator {ω' | S.A ω' ≠ a} (fun _ => (1:ℝ)))
have h1 : Measurable[S.σ_X]
(μ[indicator {ω' | S.A ω' ≠ a} (fun _ => (1:ℝ)) | S.σ_X]) :=
this.measurable
have h2 : Measurable[S.σ_X]
(μ[indicator {ω' | S.A ω' = a} (fun _ => (1:ℝ)) | S.σ_X]) :=
stronglyMeasurable_condExp.measurable
exact h1.div h2
have hR_meas_AX : Measurable[S.σ_AX] R := hR_meas_X.mono S.σ_X_le_σ_AX le_rfl
have hR_meas_UX : Measurable[S.σ_UX] R := hR_meas_X.mono S.σ_X_le_σ_UX le_rfl
have hR_meas_AUX : Measurable[S.σ_AUX] R := hR_meas_X.mono S.σ_X_le_σ_AUX le_rfl
have hR_meas : Measurable R := hR_meas_X.mono S.σ_X_le le_rfl
-- Integrability of g: g equals ({A=a}).indicator R; combine with
-- `integrableOn_stratumOddsRatio_arm`.
have hR_armOn : IntegrableOn R {ω | S.A ω = a} μ :=
integrableOn_stratumOddsRatio_arm HA a
have hg_eq_indicator : g = ({ω | S.A ω = a}).indicator R := by
funext ω
by_cases h : ω ∈ {ω' | S.A ω' = a}
· simp [g, ind, Set.indicator_of_mem h]
· simp [g, ind, Set.indicator_of_notMem h]
have hg_int : Integrable g μ := by
rw [hg_eq_indicator]
exact hR_armOn.integrable_indicator hs_meas
-- AEStronglyMeasurable[σ_AX] g.
have hg_aesm_AX : AEStronglyMeasurable[S.σ_AX] g μ := by
refine (Measurable.stronglyMeasurable ?_).aestronglyMeasurable
exact hind_meas_AX.mul hR_meas_AX
-- σ-finite trim for σ_AX, σ_UX, σ_AUX.
haveI : IsFiniteMeasure (μ.trim S.σ_AX_le) := isFiniteMeasure_trim S.σ_AX_le
haveI : SigmaFinite (μ.trim S.σ_AX_le) := inferInstance
haveI : IsFiniteMeasure (μ.trim S.σ_UX_le) := isFiniteMeasure_trim S.σ_UX_le
haveI : SigmaFinite (μ.trim S.σ_UX_le) := inferInstance
haveI : IsFiniteMeasure (μ.trim S.σ_AUX_le) := isFiniteMeasure_trim S.σ_AUX_le
haveI : SigmaFinite (μ.trim S.σ_AUX_le) := inferInstance
haveI : IsFiniteMeasure (μ.trim S.σ_X_le) := isFiniteMeasure_trim S.σ_X_le
haveI : SigmaFinite (μ.trim S.σ_X_le) := inferInstance
-- ============================================================
-- Step B: g =ᵐ[μ] μ[f | σ_AX] via the uniqueness lemma.
-- ============================================================
have hg_eq_CE : g =ᵐ[μ] μ[f | S.σ_AX] := by
refine MeasureTheory.ae_eq_condExp_of_forall_setIntegral_eq S.σ_AX_le hf_int
(fun s _ _ => hg_int.integrableOn) ?_ hg_aesm_AX
-- Set-integral identity on σ_AX-measurable s with finite measure.
intro s hs_meas_AX _hμs_finite
-- Unpack s = S.AX ⁻¹' C.
have hs_meas_mΩ : MeasurableSet s := S.σ_AX_le _ hs_meas_AX
obtain ⟨C, hC_meas, hC_eq⟩ := hs_meas_AX
-- Define C_a := slice of C at a, and g_X := indicator C_a (S.X ·).
set C_a : Set γ_X := (fun x : γ_X => ((a, x) : Bool × γ_X)) ⁻¹' C with hCa_def
have hCa_meas : MeasurableSet C_a := by
refine (prodMk (measurable_const : Measurable (fun _ : γ_X => a))
measurable_id) hC_meas
set g_X : P.Ω → ℝ := fun ω => indicator C_a (fun _ => (1:ℝ)) (S.X ω)
with hgX_def
-- g_X is σ_X-measurable (and bounded by 1).
have hgX_meas_X : Measurable[S.σ_X] g_X := by
-- comap-form: indicator C_a (·1) ∘ S.X has σ_X-meas preimages.
have hbase : Measurable (indicator C_a (fun _ : γ_X => (1:ℝ))) :=
measurable_const.indicator hCa_meas
-- A function of S.X is σ_X-measurable.
intro t ht
refine ⟨Set.indicator C_a (fun _ : γ_X => (1:ℝ)) ⁻¹' t, hbase ht, ?_⟩
rfl
have hgX_meas : Measurable g_X := hgX_meas_X.mono S.σ_X_le le_rfl
have hgX_meas_AX : Measurable[S.σ_AX] g_X := hgX_meas_X.mono S.σ_X_le_σ_AX le_rfl
have hgX_meas_UX : Measurable[S.σ_UX] g_X := hgX_meas_X.mono S.σ_X_le_σ_UX le_rfl
have hgX_meas_AUX : Measurable[S.σ_AUX] g_X := hgX_meas_X.mono S.σ_X_le_σ_AUX le_rfl
have hgX_le : ∀ ω, ‖g_X ω‖ ≤ 1 := by
intro ω
by_cases h : S.X ω ∈ C_a
· simp [g_X, Set.indicator_of_mem h]
· simp [g_X, Set.indicator_of_notMem h]
have hgX_int : Integrable g_X μ := by
refine (integrable_const (1 : ℝ)).mono' hgX_meas.aestronglyMeasurable ?_
exact Filter.Eventually.of_forall (by intro ω; simpa using hgX_le ω)
-- The split identity: 1_s · ind = g_X · ind, pointwise.
have hSplit : ∀ ω, indicator s (fun _ => (1:ℝ)) ω * ind ω
= g_X ω * ind ω := by
intro ω
by_cases hAa : ω ∈ {ω' | S.A ω' = a}
· -- on {A=a}: ind = 1; LHS = 1_s ω; RHS = g_X ω.
have hindω : ind ω = 1 := by
simp [ind, Set.indicator_of_mem hAa]
have hAω : S.A ω = a := hAa
-- ω ∈ s ↔ S.AX ω ∈ C ↔ (a, S.X ω) ∈ C ↔ S.X ω ∈ C_a.
have hs_iff : ω ∈ s ↔ S.X ω ∈ C_a := by
rw [← hC_eq]; constructor
· intro h
change (S.A ω, S.X ω) ∈ C at h
rw [hAω] at h
exact h
· intro h
change (S.A ω, S.X ω) ∈ C
rw [hAω]; exact h
by_cases hsω : ω ∈ s
· have hCa : S.X ω ∈ C_a := hs_iff.mp hsω
simp [Set.indicator_of_mem hsω, Set.indicator_of_mem hCa, g_X, hindω]
· have hCa : S.X ω ∉ C_a := fun h => hsω (hs_iff.mpr h)
simp [Set.indicator_of_notMem hsω, Set.indicator_of_notMem hCa, g_X, hindω]
· -- off {A=a}: ind = 0, both sides zero.
have hindω : ind ω = 0 := by
simp [ind, Set.indicator_of_notMem hAa]
simp [hindω]
-- Express ∫_s f = ∫_{A=a} g_X * q' (using Pf has ind in it).
have h_f_split : ∫ ω in s, f ω ∂μ
= ∫ ω in {ω | S.A ω = a}, g_X ω * q' ω ∂μ := by
-- ∫_s f = ∫ 1_s · ind · q' (since f = ind · q')
-- = ∫ g_X · ind · q' (Split)
-- = ∫_{A=a} g_X · q'.
rw [← integral_indicator (μ := μ) hs_meas_mΩ,
← integral_indicator (μ := μ) hs_meas]
refine integral_congr_ae (Filter.Eventually.of_forall ?_)
intro ω
by_cases hsω : ω ∈ s
· -- ω ∈ s. f = ind · q'. We have hSplit ω.
have h1 : indicator s f ω = f ω := Set.indicator_of_mem hsω f
rw [h1]
by_cases hAa : ω ∈ {ω' | S.A ω' = a}
· have h2 : indicator {ω | S.A ω = a} (fun ω => g_X ω * q' ω) ω
= g_X ω * q' ω := Set.indicator_of_mem hAa _
rw [h2]
-- f ω = ind ω * q' ω, ind ω = 1 here.
have hindω : ind ω = 1 := by simp [ind, Set.indicator_of_mem hAa]
-- And 1_s ω = 1, so 1 * ind ω = g_X ω * ind ω → 1 = g_X ω
have hSplitω := hSplit ω
rw [Set.indicator_of_mem hsω, hindω, mul_one, mul_one] at hSplitω
simp [f, hindω, hSplitω]
· -- ω ∉ {A=a}: ind ω = 0, f ω = 0; RHS indicator off the set = 0.
have h2 : indicator {ω | S.A ω = a} (fun ω => g_X ω * q' ω) ω = 0 :=
Set.indicator_of_notMem hAa _
have hindω : ind ω = 0 := by simp [ind, Set.indicator_of_notMem hAa]
simp [f, hindω, h2]
· -- ω ∉ s.
rw [Set.indicator_of_notMem hsω]
by_cases hAa : ω ∈ {ω' | S.A ω' = a}
· -- ω ∉ s but ω ∈ {A=a}: by hs_iff, S.X ω ∉ C_a, so g_X ω = 0.
have hAω : S.A ω = a := hAa
have hs_iff : ω ∈ s ↔ S.X ω ∈ C_a := by
rw [← hC_eq]; constructor
· intro h
change (S.A ω, S.X ω) ∈ C at h
rw [hAω] at h; exact h
· intro h
change (S.A ω, S.X ω) ∈ C
rw [hAω]; exact h
have hCa_not : S.X ω ∉ C_a := fun h => hsω (hs_iff.mpr h)
have hgXω : g_X ω = 0 := by
simp [g_X, Set.indicator_of_notMem hCa_not]
have h2 : indicator {ω | S.A ω = a} (fun ω => g_X ω * q' ω) ω
= g_X ω * q' ω := Set.indicator_of_mem hAa _
rw [h2, hgXω, zero_mul]
· have h2 : indicator {ω | S.A ω = a} (fun ω => g_X ω * q' ω) ω = 0 :=
Set.indicator_of_notMem hAa _
rw [h2]
-- Same for g (replacing q' with R).
have h_g_split : ∫ ω in s, g ω ∂μ
= ∫ ω in {ω | S.A ω = a}, g_X ω * R ω ∂μ := by
rw [← integral_indicator (μ := μ) hs_meas_mΩ,
← integral_indicator (μ := μ) hs_meas]
refine integral_congr_ae (Filter.Eventually.of_forall ?_)
intro ω
by_cases hsω : ω ∈ s
· have h1 : indicator s g ω = g ω := Set.indicator_of_mem hsω g
rw [h1]
by_cases hAa : ω ∈ {ω' | S.A ω' = a}
· have h2 : indicator {ω | S.A ω = a} (fun ω => g_X ω * R ω) ω
= g_X ω * R ω := Set.indicator_of_mem hAa _
rw [h2]
have hindω : ind ω = 1 := by simp [ind, Set.indicator_of_mem hAa]
have hSplitω := hSplit ω
rw [Set.indicator_of_mem hsω, hindω, mul_one, mul_one] at hSplitω
simp [g, hindω, hSplitω]
· have h2 : indicator {ω | S.A ω = a} (fun ω => g_X ω * R ω) ω = 0 :=
Set.indicator_of_notMem hAa _
have hindω : ind ω = 0 := by simp [ind, Set.indicator_of_notMem hAa]
simp [g, hindω, h2]
· rw [Set.indicator_of_notMem hsω]
by_cases hAa : ω ∈ {ω' | S.A ω' = a}
· have hAω : S.A ω = a := hAa
have hs_iff : ω ∈ s ↔ S.X ω ∈ C_a := by
rw [← hC_eq]; constructor
· intro h
-- … truncated; follow the source link for the rest …