PO.ID.Partial.Proxy
Partial identification with proxy variables: sensitivity of bounds to proxy quality.
Helpers 4 core · 6 supporting · 4 submodules This file gathers the shared algebra and conditioning facts used by proximal partial-identification bounds, covering marginalization, bridge substitution, and proxy-collapse arguments. ZBased 3 core · 1 supporting · 1 submodule This file proves the Z-only proximal partial-identification bounds for off-arm and marginal counterfactual means.
Assumptions 3 core · 0 supporting Three weakened assumption bundles, one per partial-identification theorem of Ghassami-Shpitser-Tchetgen Tchetgen (2024): * WBasedAssumptions — outcome-confounding-proxy bounds (Theorem 1).
Proximal partial-identification assumption bundles
Three weakened assumption bundles, one per partial-identification theorem of Ghassami-Shpitser-Tchetgen Tchetgen (2024):
* WBasedAssumptions — outcome-confounding-proxy bounds (Theorem 1).
* ZBasedAssumptions — treatment-confounding-proxy bounds (Theorem 2).
* TwoProxyAssumptions — two conditionally independent invalid proxies
(Theorem 3).
All three weaken the exact-identification bundle
POProximalSystem.Assumptions by dropping the completeness condition (and,
for the W- and Z-only cases, dropping the unused proxy's assumptions).
The bridge function h (W side) and bridge function q (Z side) are bundled
as fields, exactly as in the exact-ID bundle. The treatment-side bridge q
satisfies E[q(Z, A, X) | A, X, U] = p(U | ¬A, X) / p(U | A, X). In the
general standard-Borel setting the right-hand side is a Radon-Nikodym
derivative whose existence is non-trivial; we package it as a user-supplied
measurable function likelihoodRatio_swapA together with its defining
relation.
structure WBasedAssumptions reviewed
⚑ flagged
Causalean.PO.POProximalSystem
Assumption bundle for the W-proxy partial-identification theorem (Ghassami-Shpitser-Tchetgen Tchetgen 2024, Thm 1).
Definition (Lean source)
parameters
S :
POProximalSystem P γ_X γ_Z γ_W γ_U
μ :
Measure P.Ω := P.μ
fields
Consistency axiom for the ambient PO system.
consistency :
POSystem.Consistency P
Latent exchangeability: Y(a) ⟂ A | (U, X) for each treatment level.
latent_exch :
∀ a : Bool, CondIndepFun S.σ_UX S.σ_UX_le (S.YofA a) S.A μ
Outcome-proxy assumption: W ⟂ A | (U, X).
proxy_WA :
CondIndepFun S.σ_UX S.σ_UX_le S.W S.A μ
Outcome bridge function `h : Bool × γ_W × γ_X → ℝ`.
h :
Bool × γ_W × γ_X → ℝ
`h` is measurable.
measurable_h :
`h` is pointwise non-negative. This is the paper's Assumption 2, which
*posits the existence* of a non-negative outcome bridge `h`. (It is not a
consequence of `Y ≥ 0`: even when `Y ⊆ [0, ∞)`, a bridge solving the integral
equation need not itself be non-negative, so this is assumed, not derived.)
h_nonneg :
∀ x, 0 ≤ h x
Latent bridge equation: `E[Y - h(A, W, X) | σ(A, U, X)] = 0` a.s.
bridge :
(μ[fun ω => S.Y ω - h (S.A ω, S.W ω, S.X ω) | S.σ_AUX]) =ᵐ[μ] 0
`h(A, W, X)` is integrable.
integrable_h :
Integrable (fun ω => h (S.A ω, S.W ω, S.X ω)) μ
For each `a`, `h(a, W, X)` is integrable (used by the upper-envelope step).
integrable_h_arm :
∀ a : Bool, Integrable (fun ω => h (a, S.W ω, S.X ω)) μ
`Y` is integrable.
integrable_Y :
Integrable S.Y μ
Each `Y(a)` is integrable.
integrable_YofA :
∀ a : Bool, Integrable (S.YofA a) μ
Essential lower bound on `Y` (paper: `Y ⊆ [0, +∞)`, generalised).
Y_bdd_below :
∃ M : ℝ, ∀ᵐ ω ∂μ, M ≤ S.Y ω
Essential upper bound on `Y` used by the trivial-bound clamp. This finite
bound is a formal strengthening of the paper's displayed nonnegative-support
convention, which writes the upper clamp with `sup Y`; the theorem here uses
a real-valued essential upper bound instead of an extended-real top element.
Y_bdd_above :
∃ M : ℝ, ∀ᵐ ω ∂μ, S.Y ω ≤ M
Strong overlap: for each arm `a`, `P(A = a | U, X) > 0` a.e., expressed
as: every σ_UX-measurable set that meets `{A = a}` in a null set is itself null.
Required for lifting single-arm a.e.-equalities to global a.e.-equalities.
overlap_strong :
structure ZBasedAssumptions reviewed
⚑ flagged
Causalean.PO.POProximalSystem
Assumption bundle for the Z-proxy partial-identification theorem (Thm 2). Drops proxy_WAZ, completeness, and W-related fields.
Definition (Lean source)
parameters
S :
POProximalSystem P γ_X γ_Z γ_W γ_U
μ :
Measure P.Ω := P.μ
fields
Consistency axiom for the ambient PO system.
consistency :
POSystem.Consistency P
Latent exchangeability: Y(a) ⟂ A | (U, X) for each treatment level.
latent_exch :
∀ a : Bool, CondIndepFun S.σ_UX S.σ_UX_le (S.YofA a) S.A μ
Treatment-proxy assumption: Z ⟂ Y | (A, U, X).
proxy_YZ :
CondIndepFun S.σ_AUX S.σ_AUX_le S.Y S.Z μ
Treatment-side bridge function `q : γ_Z × Bool × γ_X → ℝ`.
q :
γ_Z × Bool × γ_X → ℝ
`q` is measurable.
measurable_q :
`q` is non-negative (paper Assumption 5).
q_nonneg :
∀ x, 0 ≤ q x
Probability-ratio `p(¬a | U, X) / p(a | U, X)`, σ_UX-measurable,
supplied by the user (see structure docstring).
likelihoodRatio_swapA :
Bool → P.Ω → ℝ
measurable_likelihoodRatio_swapA :
∀ a, Measurable[S.σ_UX] (likelihoodRatio_swapA a)
Defining change-of-measure equation
`E[𝟙{A=a} | σ_UX] · likelihoodRatio_swapA a =ᵐ E[𝟙{A=¬a} | σ_UX]`.
On the support of `E[𝟙{A=a} | σ_UX]`, this gives
`likelihoodRatio_swapA a = p(¬a | U, X) / p(a | U, X)`.
likelihoodRatio_swapA_spec :
`likelihoodRatio_swapA a` is integrable. Paper Assumption 3 (strict
overlap) does not produce a uniform bound on `L`, so finiteness of its
expectation is surfaced as a separate explicit assumption.
integrable_likelihoodRatio_swapA :
∀ a : Bool, Integrable (likelihoodRatio_swapA a) μ
Product `μ[Y(a) | σ_UX] · L` is integrable. The bundle does not
give Y or `μ[Y(a)|σ_UX]` boundedness in the Z-only theorem (Remark 5),
so L¹·L¹ closure is not automatic; we surface it explicitly.
integrable_condExpYofA_mul_L :
∀ a : Bool, Integrable (fun ω => (μ[S.YofA a | S.σ_UX]) ω * likelihoodRatio_swapA a ω) μ
Product `μ[Y | σ_AZX] · q(Z, a, X)` is integrable. Required by the
σ_AZX-conditional envelope step inside the bridge-substitution chain
(Theorem 2). The bundle does not give Y or `μ[Y|σ_AZX]` boundedness
(Remark 5 forbids a Y-clamp), so L¹·L¹ closure is not automatic; we
surface it explicitly per the paper's "all integrals are finite"
convention.
integrable_condExpY_mul_q :
∀ a : Bool, Integrable (fun ω => (μ[S.Y | S.σ_AZX]) ω * q (S.Z ω, a, S.X ω)) μ
Product `Y · q(Z, a, X)` is integrable. Required by the
bridge-substitution arm chain (Theorem 2): we factor
`μ[Y · q | σ_AUX] = μ[Y|σ_AUX] · μ[q|σ_AUX]` under proxy_YZ and tower
back to `∫_s Y · q dμ`, both of which need this L¹ closure. The bundle
does not give Y boundedness (Remark 5 forbids a Y-clamp), so L¹·L¹
closure is not automatic; we surface it explicitly per the paper's
"all integrals are finite" convention.
integrable_Y_mul_q :
∀ a : Bool, Integrable (fun ω => S.Y ω * q (S.Z ω, a, S.X ω)) μ
Treatment-side bridge equation:
`E[q(Z, a, X) | σ(A, U, X)] = likelihoodRatio_swapA a` a.s. on `{A = a}`.
bridge_q :
∀ a : Bool,
(μ[fun ω => q (S.Z ω, a, S.X ω) | S.σ_AUX])
=ᵐ[μ.restrict {ω | S.A ω = a}] likelihoodRatio_swapA a
For each `a`, `q(Z, a, X)` is integrable.
integrable_q :
∀ a : Bool, Integrable (fun ω => q (S.Z ω, a, S.X ω)) μ
`Y` is integrable.
integrable_Y :
Integrable S.Y μ
Each `Y(a)` is integrable.
integrable_YofA :
∀ a : Bool, Integrable (S.YofA a) μ
Strong overlap: `p(A = a | U, X) > 0` (paper Assumption 3 positivity).
Same condition as `WBasedAssumptions.overlap_strong`.
overlap_strong :
structure TwoProxyAssumptions reviewed
⚑ flagged
Causalean.PO.POProximalSystem
Assumption bundle for the two-proxy partial-identification theorem (Thm 3). Both proxies W and Z are present, but the strong exclusion restrictions W ⟂ A | (U, X) and Y ⟂ Z | (A, U, X) may FAIL — that is the "invalid proxy" angle. The only proxy-side conditional independence required is proxy_WZ_indep : W ⟂ Z | (A, X, U) (paper Assumption 6); in particular, no W ⟂ A | (U, X) requirement is bundled. Both bridge functions h and q are kept as fields, with their latent-side defining equations.
Definition (Lean source)
parameters
S :
POProximalSystem P γ_X γ_Z γ_W γ_U
μ :
Measure P.Ω := P.μ
fields
Consistency axiom for the ambient PO system.
consistency :
POSystem.Consistency P
Latent exchangeability: Y(a) ⟂ A | (U, X) for each treatment level.
latent_exch :
∀ a : Bool, CondIndepFun S.σ_UX S.σ_UX_le (S.YofA a) S.A μ
Conditional independence of the two proxies given `(A, U, X)`
(paper Assumption 6).
proxy_WZ_indep :
CondIndepFun S.σ_AUX S.σ_AUX_le S.W S.Z μ
Outcome-side bridge function.
h :
Bool × γ_W × γ_X → ℝ
`h` is measurable.
measurable_h :
`h` is pointwise non-negative. This is the paper's Assumption 2, which
*posits the existence* of a non-negative outcome bridge `h`. (It is not a
consequence of `Y ≥ 0`: even when `Y ⊆ [0, ∞)`, a bridge solving the integral
equation need not itself be non-negative, so this is assumed, not derived.)
h_nonneg :
∀ x, 0 ≤ h x
Outcome bridge equation `E[Y - h(A,W,X) | σ(A,U,X)] = 0`.
bridge_h :
(μ[fun ω => S.Y ω - h (S.A ω, S.W ω, S.X ω) | S.σ_AUX]) =ᵐ[μ] 0
`h(A, W, X)` is integrable.
integrable_h :
Integrable (fun ω => h (S.A ω, S.W ω, S.X ω)) μ
For each treatment arm `a`, `h(a, W, X)` is integrable.
integrable_h_arm :
∀ a : Bool, Integrable (fun ω => h (a, S.W ω, S.X ω)) μ
Treatment-side bridge function.
q :
γ_Z × Bool × γ_X → ℝ
`q` is measurable.
measurable_q :
`q` is non-negative (paper Assumption 5).
q_nonneg :
∀ x, 0 ≤ q x
Treatment-stratum likelihood ratio (see `ZBasedAssumptions` for spec).
likelihoodRatio_swapA :
Bool → P.Ω → ℝ
measurable_likelihoodRatio_swapA :
∀ a, Measurable[S.σ_UX] (likelihoodRatio_swapA a)
Defining change-of-measure equation for the probability-ratio convention:
`E[𝟙{A=a} | σ_UX] · likelihoodRatio_swapA a =ᵐ E[𝟙{A≠a} | σ_UX]`.
likelihoodRatio_swapA_spec :
`L` is integrable. Paper Assumption 3 does not yield a uniform bound.
integrable_likelihoodRatio_swapA :
∀ a : Bool, Integrable (likelihoodRatio_swapA a) μ
Product `μ[Y(a) | σ_UX] · L` is integrable (used in arm-swap step).
integrable_condExpYofA_mul_L :
∀ a : Bool, Integrable (fun ω => (μ[S.YofA a | S.σ_UX]) ω * likelihoodRatio_swapA a ω) μ
Treatment-side bridge equation:
`E[q(Z, a, X) | σ(A, U, X)] = likelihoodRatio_swapA a` a.s. on `{A = a}`.
bridge_q :
∀ a : Bool,
(μ[fun ω => q (S.Z ω, a, S.X ω) | S.σ_AUX])
=ᵐ[μ.restrict {ω | S.A ω = a}] likelihoodRatio_swapA a
For each `a`, `q(Z, a, X)` is integrable.
integrable_q :
∀ a : Bool, Integrable (fun ω => q (S.Z ω, a, S.X ω)) μ
Product `h(a, W, X) · q(Z, a, X)` is integrable. Required by the
bridge-substitution identity and the envelope chain (separate L¹ for `h`
and `q` does not imply L¹ for the product).
integrable_hq_arm :
∀ a : Bool, Integrable (fun ω => h (a, S.W ω, S.X ω) * q (S.Z ω, a, S.X ω)) μ
`Y` is integrable.
integrable_Y :
Integrable S.Y μ
Each `Y(a)` is integrable.
integrable_YofA :
∀ a : Bool, Integrable (S.YofA a) μ
Essential lower bound on `Y`.
Y_bdd_below :
∃ M : ℝ, ∀ᵐ ω ∂μ, M ≤ S.Y ω
Essential upper bound on `Y`. This finite bound is a formal strengthening
of the paper's displayed nonnegative-support assumption plus the formal
`sup Y` clamp; the theorem here exposes a real-valued essential upper bound.
Y_bdd_above :
∃ M : ℝ, ∀ᵐ ω ∂μ, S.Y ω ≤ M
Strong overlap: same condition as `WBasedAssumptions.overlap_strong`.
overlap_strong :
Setup 14 core · 8 supporting Reuses the POProximalSystem data structure from Causalean/PO/ID/Exact/Proximal/Setup.lean (six POVars: X, A, Z, W, Y, U) and adds: * The (A, X) and (X) tuple maps and σ-algebras (σ_AX, σ_X) used as conditioning targets i ★ σ_X_le
Proximal partial identification — data layer
Reuses the POProximalSystem data structure from
Causalean/PO/ID/Exact/Proximal/Setup.lean (six POVars: X, A, Z, W, Y, U)
and adds:
* The (A, X) and (X) tuple maps and σ-algebras (σ_AX, σ_X) used as
conditioning targets in the partial-identification proofs.
* Target parameters meanYofA (E[Y(a)]) and condMeanYofA (E[Y(a) | A = ¬a]).
* The σ_X-measurable stratumOddsRatio (p(A=¬a|X) / p(A=a|X)) used to
normalise stratum-conditional integrals across the two arms.
* Three abstract upper/lower envelope predicates (IsUpperEnvW/IsLowerEnvW,
IsUpperEnvZ/IsLowerEnvZ, IsUpperEnvWZ/IsLowerEnvWZ), one per
partial-identification theorem (Ghassami-Shpitser-Tchetgen Tchetgen 2024,
Thms 1, 2, 3). Each envelope is the operational integrated form of the
paper's min_w / max_w proxy-density-ratio bound.
No assumption bundles live here — see Assumptions.lean.
def AX reviewed
⚑ flagged
Causalean.PO.POProximalSystem
(A, X) : P.Ω → Bool × γ_X.
Definition (Lean source)
noncomputable def AX : P.Ω → Bool × γ_X := fun ω => (S.A ω, S.X ω)
def σ_AX reviewed
⚑ flagged
Causalean.PO.POProximalSystem
σ-algebra generated by (A, X).
Definition (Lean source)
def σ_X reviewed
⚑ flagged
Causalean.PO.POProximalSystem
σ-algebra generated by X alone.
Definition (Lean source)
lemma σ_X_le reviewed
⚑ flagged
Causalean.PO.POProximalSystem
The σ-algebra generated by the covariates is a sub-σ-algebra of the ambient measurable space.
Formal statement
conclusion
S.σ_X ≤ (inferInstance : MeasurableSpace P.Ω)
Proof (Lean source)
lemma σ_X_le : S.σ_X ≤ (inferInstance : MeasurableSpace P.Ω) :=
S.measurable_X.comap_le
def meanYofA reviewed
⚑ flagged
Causalean.PO.POProximalSystem
Marginal potential outcome mean E[Y(a)] = ∫ Y(a) dμ.
def condMeanYofA reviewed
⚑ flagged
Causalean.PO.POProximalSystem
Conditional potential outcome mean E[Y(a) | A = ¬a]. Defined as (μ {A ≠ a})⁻¹ · ∫_{A ≠ a} Y(a) dμ.
Definition (Lean source)
noncomputable def condMeanYofA (μ : Measure P.Ω) (a : Bool) : ℝ :=
(μ {ω | S.A ω ≠ a}).toReal⁻¹ * ∫ ω in {ω | S.A ω ≠ a}, S.YofA a ω ∂μ
def ATE reviewed
⚑ flagged
Causalean.PO.POProximalSystem
ATE in this proximal system: E[Y(1)] - E[Y(0)].
def stratumOddsRatio reviewed
⚑ flagged
Causalean.PO.POProximalSystem
The σ_X-measurable function ω ↦ E[𝟙{A ≠ a} | X](ω) / E[𝟙{A = a} | X](ω), which equals p(A = ¬a | X) / p(A = a | X) in the discrete case. Used to re-normalise integrals against μ.restrict {A = a} to the {A ≠ a} arm.
Definition (Lean source)
noncomputable def stratumOddsRatio (μ : Measure P.Ω) (a : Bool) : P.Ω → ℝ :=
fun ω =>
(μ[indicator {ω' | S.A ω' ≠ a} (fun _ => (1:ℝ)) | S.σ_X]) ω /
(μ[indicator {ω' | S.A ω' = a} (fun _ => (1:ℝ)) | S.σ_X]) ω
def IsUpperEnvW reviewed
⚑ flagged
Causalean.PO.POProximalSystem
Upper envelope for the W-proxy density ratio p(W | A = ¬a, X) / p(W | A = a, X) under treatment level a.
Definition (Lean source)
def IsUpperEnvW (μ : Measure P.Ω) (a : Bool) (Uenv : Bool × γ_X → ℝ) : Prop :=
Measurable Uenv ∧
∀ (φ : γ_W × γ_X → ℝ), Measurable φ → (∀ x, 0 ≤ φ x) →
Integrable (fun ω => φ (S.W ω, S.X ω)) μ →
Integrable
(fun ω => S.stratumOddsRatio μ a ω * Uenv (a, S.X ω) * φ (S.W ω, S.X ω)) μ →
∫ ω in {ω | S.A ω ≠ a}, φ (S.W ω, S.X ω) ∂μ
≤ ∫ ω in {ω | S.A ω = a},
S.stratumOddsRatio μ a ω * Uenv (a, S.X ω) * φ (S.W ω, S.X ω) ∂μ
def IsLowerEnvW reviewed
⚑ flagged
Causalean.PO.POProximalSystem
Lower envelope for the W-proxy density ratio. Mirror of IsUpperEnvW with the inequality reversed, including integrability of the weighted left-hand side.
Definition (Lean source)
def IsLowerEnvW (μ : Measure P.Ω) (a : Bool) (Lenv : Bool × γ_X → ℝ) : Prop :=
Measurable Lenv ∧
∀ (φ : γ_W × γ_X → ℝ), Measurable φ → (∀ x, 0 ≤ φ x) →
Integrable (fun ω => φ (S.W ω, S.X ω)) μ →
Integrable
(fun ω => S.stratumOddsRatio μ a ω * Lenv (a, S.X ω) * φ (S.W ω, S.X ω)) μ →
∫ ω in {ω | S.A ω = a},
S.stratumOddsRatio μ a ω * Lenv (a, S.X ω) * φ (S.W ω, S.X ω) ∂μ
≤ ∫ ω in {ω | S.A ω ≠ a}, φ (S.W ω, S.X ω) ∂μ
def IsUpperEnvZ reviewed
⚑ flagged
Causalean.PO.POProximalSystem
Upper envelope for E[Y | Z, X, A = a] under treatment level a. A σ_X-measurable function Uenv(a, X) such that, μ-a.e. on {A = a}, (μ[Y | σ_AZX]) ≤ Uenv(a, X). The paper's max_z E[Y | z, X, A = a] is the canonical (sharp) instance.
Definition (Lean source)
def IsUpperEnvZ (μ : Measure P.Ω) (a : Bool) (Uenv : Bool × γ_X → ℝ) : Prop :=
Measurable Uenv ∧
∀ᵐ ω ∂(μ.restrict {ω | S.A ω = a}),
(μ[S.Y | S.σ_AZX]) ω ≤ Uenv (a, S.X ω)
def IsLowerEnvZ reviewed
⚑ flagged
Causalean.PO.POProximalSystem
Lower envelope for E[Y | Z, X, A = a]. Mirror of IsUpperEnvZ.
Definition (Lean source)
def IsLowerEnvZ (μ : Measure P.Ω) (a : Bool) (Lenv : Bool × γ_X → ℝ) : Prop :=
Measurable Lenv ∧
∀ᵐ ω ∂(μ.restrict {ω | S.A ω = a}),
Lenv (a, S.X ω) ≤ (μ[S.Y | S.σ_AZX]) ω
def IsUpperEnvWZ reviewed
⚑ flagged
Causalean.PO.POProximalSystem
Upper envelope for the same-arm joint-vs-product W-Z density ratio under treatment level a: ρ(w, z, x) := p(w, z | A = a, x) / (p(w | A = a, x) · p(z | A = a, x)).
Definition (Lean source)
def IsUpperEnvWZ (μ : Measure P.Ω) (a : Bool) (Uenv : Bool × γ_X → ℝ) : Prop :=
Measurable Uenv ∧
∀ (φ_W : γ_W × γ_X → ℝ) (φ_Z : γ_Z × γ_X → ℝ),
Measurable φ_W → Measurable φ_Z →
(∀ x, 0 ≤ φ_W x) → (∀ x, 0 ≤ φ_Z x) →
Integrable (fun ω => φ_W (S.W ω, S.X ω) * φ_Z (S.Z ω, S.X ω)) μ →
Integrable (fun ω => φ_W (S.W ω, S.X ω)) μ →
Integrable (fun ω => φ_Z (S.Z ω, S.X ω)) μ →
(μ[fun ω => φ_W (S.W ω, S.X ω) * φ_Z (S.Z ω, S.X ω) | S.σ_AX])
≤ᵐ[μ.restrict {ω | S.A ω = a}]
fun ω => Uenv (a, S.X ω) *
((μ[fun ω' => φ_W (S.W ω', S.X ω') | S.σ_AX]) ω)
* ((μ[fun ω' => φ_Z (S.Z ω', S.X ω') | S.σ_AX]) ω)
def IsLowerEnvWZ reviewed
⚑ flagged
Causalean.PO.POProximalSystem
Lower envelope for the same-arm joint-vs-product W-Z density ratio. Mirror of IsUpperEnvWZ with the inequality reversed: the canonical sharp choice is Lenv(a, x) = inf_{w, z} ρ(w, z, x).
Definition (Lean source)
def IsLowerEnvWZ (μ : Measure P.Ω) (a : Bool) (Lenv : Bool × γ_X → ℝ) : Prop :=
Measurable Lenv ∧
∀ (φ_W : γ_W × γ_X → ℝ) (φ_Z : γ_Z × γ_X → ℝ),
Measurable φ_W → Measurable φ_Z →
(∀ x, 0 ≤ φ_W x) → (∀ x, 0 ≤ φ_Z x) →
Integrable (fun ω => φ_W (S.W ω, S.X ω) * φ_Z (S.Z ω, S.X ω)) μ →
Integrable (fun ω => φ_W (S.W ω, S.X ω)) μ →
Integrable (fun ω => φ_Z (S.Z ω, S.X ω)) μ →
(fun ω => Lenv (a, S.X ω) *
((μ[fun ω' => φ_W (S.W ω', S.X ω') | S.σ_AX]) ω)
* ((μ[fun ω' => φ_Z (S.Z ω', S.X ω') | S.σ_AX]) ω))
≤ᵐ[μ.restrict {ω | S.A ω = a}]
(μ[fun ω => φ_W (S.W ω, S.X ω) * φ_Z (S.Z ω, S.X ω) | S.σ_AX])
8 supporting declarations (lemmas, instances)
-
measurable_AXlemma — The treatment-covariate tuple map is measurable.conclusionMeasurable S.AXProof (Lean source)
lemma measurable_AX : Measurable S.AX := prodMk S.measurable_A S.measurable_X -
σ_AX_lelemma — The sigma-algebra generated by treatment and covariates is a sub-sigma-algebra of the ambient measurable space.conclusionS.σ_AX ≤ (inferInstance : MeasurableSpace P.Ω)Proof (Lean source)
lemma σ_AX_le : S.σ_AX ≤ (inferInstance : MeasurableSpace P.Ω) := S.measurable_AX.comap_le -
σ_X_le_σ_AXlemma — σ_X is coarser than σ_AX: X factors through (A, X) via the second projection.conclusionS.σ_X ≤ S.σ_AXProof (Lean source)
lemma σ_X_le_σ_AX : S.σ_X ≤ S.σ_AX := by -- X = snd ∘ (A, X). So comap X ≤ comap (A, X). have hX_eq : S.X = (fun p : Bool × γ_X => p.2) ∘ S.AX := by funext ω; rfl intro s hs obtain ⟨t, ht_meas, ht_eq⟩ := hs refine ⟨(fun p : Bool × γ_X => p.2) ⁻¹' t, measurable_snd ht_meas, ?_⟩ rw [← ht_eq, hX_eq]; rfl -
σ_X_le_σ_UXlemma — σ_X ≤ σ_UX, since X factors through (U, X) via the second projection.conclusionS.σ_X ≤ S.σ_UXProof (Lean source)
lemma σ_X_le_σ_UX : S.σ_X ≤ S.σ_UX := by intro s hs obtain ⟨t, ht_meas, ht_eq⟩ := hs refine ⟨(fun p : γ_U × γ_X => p.2) ⁻¹' t, measurable_snd ht_meas, ?_⟩ rw [← ht_eq]; rfl -
σ_AZX_le_σ_AZUXlemma — σ_AZX ≤ σ_AZUX, since (A, Z, X) factors through (A, Z, U, X).conclusionS.σ_AZX ≤ S.σ_AZUXProof (Lean source)
lemma σ_AZX_le_σ_AZUX : S.σ_AZX ≤ S.σ_AZUX := by intro s hs obtain ⟨t, ht_meas, ht_eq⟩ := hs refine ⟨(fun p : Bool × γ_Z × γ_U × γ_X => (p.1, p.2.1, p.2.2.2)) ⁻¹' t, ?_, ?_⟩ · refine prodMk measurable_fst (prodMk ?_ ?_) ht_meas · exact measurable_fst.comp measurable_snd · exact measurable_snd.comp (measurable_snd.comp measurable_snd) · rw [← ht_eq]; rfl -
σ_AUX_le_σ_AZUXlemma — The sigma-algebra on treatment, unobserved confounder, and covariates is coarser than the sigma-algebra that also includes the Z proxy.conclusionS.σ_AUX ≤ S.σ_AZUXProof (Lean source)
lemma σ_AUX_le_σ_AZUX : S.σ_AUX ≤ S.σ_AZUX := by intro s hs obtain ⟨t, ht_meas, ht_eq⟩ := hs refine ⟨(fun p : Bool × γ_Z × γ_U × γ_X => (p.1, p.2.2.1, p.2.2.2)) ⁻¹' t, ?_, ?_⟩ · refine prodMk measurable_fst (prodMk ?_ ?_) ht_meas · exact measurable_fst.comp (measurable_snd.comp measurable_snd) · exact measurable_snd.comp (measurable_snd.comp measurable_snd) · rw [← ht_eq]; rfl -
σ_AX_le_σ_AUXlemma — σ_AX is coarser than σ_AUX, since (A, X) factors through (A, U, X) via the projection (a, u, x) ↦ (a, x).conclusionS.σ_AX ≤ S.σ_AUXProof (Lean source)
lemma σ_AX_le_σ_AUX : S.σ_AX ≤ S.σ_AUX := by -- The map S.AX = (A, X) factors as (proj) ∘ S.AUX where proj (a,u,x) = (a,x). -- So σ_AX = comap S.AX = comap (proj ∘ S.AUX) ≤ comap S.AUX = σ_AUX. have hAX_eq : S.AX = (fun p : Bool × γ_U × γ_X => (p.1, p.2.2)) ∘ S.AUX := by funext ω; rfl have hproj_meas : Measurable (fun p : Bool × γ_U × γ_X => (p.1, p.2.2)) := prodMk measurable_fst (measurable_snd.comp measurable_snd) -- Now show comap S.AX ≤ comap S.AUX directly. intro s hs obtain ⟨t, ht_meas, ht_eq⟩ := hs refine ⟨(fun p : Bool × γ_U × γ_X => (p.1, p.2.2)) ⁻¹' t, hproj_meas ht_meas, ?_⟩ rw [← ht_eq, hAX_eq] rfl -
σ_X_le_σ_AUXlemma — σ_X ≤ σ_AUX, by composition σ_X ≤ σ_AX ≤ σ_AUX.conclusionS.σ_X ≤ S.σ_AUXProof (Lean source)
lemma σ_X_le_σ_AUX : S.σ_X ≤ S.σ_AUX := le_trans S.σ_X_le_σ_AX S.σ_AX_le_σ_AUX
IntervalForm 5 core · 0 supporting This file converts the scalar two-sided proximal proxy bounds into Set.Icc membership statements. ★ condMeanYofA_W_mem_Icc★ meanYofA_W_mem_Icc★ condMeanYofA_Z_mem_Icc★ meanYofA_Z_mem_Icc★ condMeanYofA_WZ_mem_Icc
Closed-interval forms of proximal proxy bounds
This file converts the scalar two-sided proximal proxy bounds into Set.Icc
membership statements. The W-based, Z-based, and two-proxy source theorems keep
their original hypotheses, while this layer adapts them to the common
partial-identification interval vocabulary.
theorem condMeanYofA_W_mem_Icc reviewed
⚑ flagged
Causalean.PO.POProximalSystem
Set.Icc form of Theorem 1 (condMeanYofA_W_bounds). Fix a treatment arm a and assume the W-only proximal bridge assumption bundle, with the treatment and outcome variables distinct; let Lenv, Uenv be lower and upper envelope functions bounding the W-proxy density ratio, with the off-arm stratum of positive mass and the envelope-weighted bridge moments integrable. Then the conditional target E[Y(a) ∣ A ≠ a] lies in the closed interval spanned by the essential Y-bounds and the W-proxy envelope clamps, the Set.Icc membership restatement of the scalar sandwich bound condMeanYofA_W_bounds.
Formal statement
hypotheses
HA :
POProximalSystem.WBasedAssumptions S μ
a :
hAY :
S.Avar.v ≠ S.Yvar.v
Lenv Uenv :
Bool × γ_X → ℝ
hL :
S.IsLowerEnvW μ a Lenv
hU :
S.IsUpperEnvW μ a Uenv
hμpos :
0 < (μ {ω | S.A ω ≠ a}).toReal
hU_int_h :
Integrable (fun ω => S.stratumOddsRatio μ a ω * Uenv (a, S.X ω) * HA.h (a, S.W ω, S.X ω)) μ
hL_int_h :
Integrable (fun ω => S.stratumOddsRatio μ a ω * Lenv (a, S.X ω) * HA.h (a, S.W ω, S.X ω)) μ
conclusion
S.condMeanYofA μ a ∈ Icc (max (choose HA.Y_bdd_below) ((μ {ω | S.A ω ≠ a}).toReal⁻¹ * ∫ ω in {ω | S.A ω = a}, S.stratumOddsRatio μ a ω * Lenv (a, S.X ω) * (μ[S.Y | S.σ_AX]) ω ∂μ)) (min (choose HA.Y_bdd_above) ((μ {ω | S.A ω ≠ a}).toReal⁻¹ * ∫ ω in {ω | S.A ω = a}, S.stratumOddsRatio μ a ω * Uenv (a, S.X ω) * (μ[S.Y | S.σ_AX]) ω ∂μ))
Proof (Lean source)
theorem condMeanYofA_W_mem_Icc
(HA : POProximalSystem.WBasedAssumptions S μ) (a : Bool)
(hAY : S.Avar.v ≠ S.Yvar.v)
(Lenv Uenv : Bool × γ_X → ℝ)
(hL : S.IsLowerEnvW μ a Lenv) (hU : S.IsUpperEnvW μ a Uenv)
(hμpos : 0 < (μ {ω | S.A ω ≠ a}).toReal)
(hU_int_h : Integrable
(fun ω => S.stratumOddsRatio μ a ω * Uenv (a, S.X ω) *
HA.h (a, S.W ω, S.X ω)) μ)
(hL_int_h : Integrable
(fun ω => S.stratumOddsRatio μ a ω * Lenv (a, S.X ω) *
HA.h (a, S.W ω, S.X ω)) μ) :
S.condMeanYofA μ a ∈ Icc
(max (choose HA.Y_bdd_below)
((μ {ω | S.A ω ≠ a}).toReal⁻¹ *
∫ ω in {ω | S.A ω = a},
S.stratumOddsRatio μ a ω * Lenv (a, S.X ω) * (μ[S.Y | S.σ_AX]) ω ∂μ))
(min (choose HA.Y_bdd_above)
((μ {ω | S.A ω ≠ a}).toReal⁻¹ *
∫ ω in {ω | S.A ω = a},
S.stratumOddsRatio μ a ω * Uenv (a, S.X ω) * (μ[S.Y | S.σ_AX]) ω ∂μ)) := by
have h := condMeanYofA_W_bounds HA a hAY Lenv Uenv hL hU hμpos hU_int_h hL_int_h
exact mem_Icc_of_sandwich h.1 h.2
theorem meanYofA_W_mem_Icc reviewed
⚑ flagged
Causalean.PO.POProximalSystem
Set.Icc form of Corollary 1 (meanYofA_W_bounds). Fix a treatment arm a and assume the W-only proximal bridge assumption bundle, with the treatment and outcome variables distinct; let Lenv, Uenv be lower and upper envelope functions bounding the W-proxy density ratio, and assume the envelope-weighted bridge moments and the envelope-weighted observed conditional means are integrable. Then the marginal target E[Y(a)] lies in the closed interval spanned by the W-proxy marginal lower and upper clamps, the Set.Icc membership restatement of the scalar sandwich bound meanYofA_W_bounds.
Formal statement
hypotheses
HA :
POProximalSystem.WBasedAssumptions S μ
a :
hAY :
S.Avar.v ≠ S.Yvar.v
Lenv Uenv :
Bool × γ_X → ℝ
hL :
S.IsLowerEnvW μ a Lenv
hU :
S.IsUpperEnvW μ a Uenv
hU_int_h :
Integrable (fun ω => S.stratumOddsRatio μ a ω * Uenv (a, S.X ω) * HA.h (a, S.W ω, S.X ω)) μ
hL_int_h :
Integrable (fun ω => S.stratumOddsRatio μ a ω * Lenv (a, S.X ω) * HA.h (a, S.W ω, S.X ω)) μ
hU_int_Y :
Integrable (fun ω => S.stratumOddsRatio μ a ω * Uenv (a, S.X ω) * (μ[S.Y | S.σ_AX]) ω) μ
hL_int_Y :
Integrable (fun ω => S.stratumOddsRatio μ a ω * Lenv (a, S.X ω) * (μ[S.Y | S.σ_AX]) ω) μ
conclusion
S.meanYofA μ a ∈ Icc (max (choose HA.Y_bdd_below * (μ {ω | S.A ω ≠ a}).toReal) (∫ ω in {ω | S.A ω = a}, S.stratumOddsRatio μ a ω * Lenv (a, S.X ω) * (μ[S.Y | S.σ_AX]) ω ∂μ) + (∫ ω in {ω | S.A ω = a}, S.Y ω ∂μ)) (min (choose HA.Y_bdd_above * (μ {ω | S.A ω ≠ a}).toReal) (∫ ω in {ω | S.A ω = a}, S.stratumOddsRatio μ a ω * Uenv (a, S.X ω) * (μ[S.Y | S.σ_AX]) ω ∂μ) + (∫ ω in {ω | S.A ω = a}, S.Y ω ∂μ))
Proof (Lean source)
theorem meanYofA_W_mem_Icc
(HA : POProximalSystem.WBasedAssumptions S μ) (a : Bool)
(hAY : S.Avar.v ≠ S.Yvar.v)
(Lenv Uenv : Bool × γ_X → ℝ)
(hL : S.IsLowerEnvW μ a Lenv) (hU : S.IsUpperEnvW μ a Uenv)
(hU_int_h : Integrable
(fun ω => S.stratumOddsRatio μ a ω * Uenv (a, S.X ω) *
HA.h (a, S.W ω, S.X ω)) μ)
(hL_int_h : Integrable
(fun ω => S.stratumOddsRatio μ a ω * Lenv (a, S.X ω) *
HA.h (a, S.W ω, S.X ω)) μ)
(hU_int_Y : Integrable
(fun ω => S.stratumOddsRatio μ a ω * Uenv (a, S.X ω) *
(μ[S.Y | S.σ_AX]) ω) μ)
(hL_int_Y : Integrable
(fun ω => S.stratumOddsRatio μ a ω * Lenv (a, S.X ω) *
(μ[S.Y | S.σ_AX]) ω) μ) :
S.meanYofA μ a ∈ Icc
(max (choose HA.Y_bdd_below * (μ {ω | S.A ω ≠ a}).toReal)
(∫ ω in {ω | S.A ω = a},
S.stratumOddsRatio μ a ω * Lenv (a, S.X ω) * (μ[S.Y | S.σ_AX]) ω ∂μ)
+ (∫ ω in {ω | S.A ω = a}, S.Y ω ∂μ))
(min (choose HA.Y_bdd_above * (μ {ω | S.A ω ≠ a}).toReal)
(∫ ω in {ω | S.A ω = a},
S.stratumOddsRatio μ a ω * Uenv (a, S.X ω) * (μ[S.Y | S.σ_AX]) ω ∂μ)
+ (∫ ω in {ω | S.A ω = a}, S.Y ω ∂μ)) := by
have h := meanYofA_W_bounds HA a hAY Lenv Uenv hL hU
hU_int_h hL_int_h hU_int_Y hL_int_Y
exact mem_Icc_of_sandwich h.1 h.2
theorem condMeanYofA_Z_mem_Icc reviewed
⚑ flagged
Causalean.PO.POProximalSystem
Set.Icc form of Theorem 2 (condMeanYofA_Z_bounds). Fix a treatment arm a and assume the Z-only proximal bridge assumption bundle, with the treatment and outcome variables distinct; let Lenv, Uenv be lower and upper envelope functions bounding the σ(A,Z,X)-conditional mean of the outcome on the on-arm stratum, assumed integrable, with the envelope weighted by the treatment-proxy bridge and the envelope weighted by the likelihood-ratio arm-swap factor both integrable, and the off-arm stratum of positive mass. Then the conditional target E[Y(a) ∣ A ≠ a] lies in the closed interval spanned by the normalised on-arm integrals of Lenv and Uenv, the Set.Icc membership restatement of the scalar sandwich bound condMeanYofA_Z_bounds.
Formal statement
hypotheses
HA :
POProximalSystem.ZBasedAssumptions S μ
a :
hAY :
S.Avar.v ≠ S.Yvar.v
Lenv Uenv :
Bool × γ_X → ℝ
hL :
S.IsLowerEnvZ μ a Lenv
hU :
S.IsUpperEnvZ μ a Uenv
hLInt :
Integrable (fun ω => Lenv (a, S.X ω)) μ
hUInt :
Integrable (fun ω => Uenv (a, S.X ω)) μ
hL_q :
Integrable (fun ω => Lenv (a, S.X ω) * HA.q (S.Z ω, a, S.X ω)) μ
hU_q :
Integrable (fun ω => Uenv (a, S.X ω) * HA.q (S.Z ω, a, S.X ω)) μ
hL_L :
Integrable (fun ω => Lenv (a, S.X ω) * HA.likelihoodRatio_swapA a ω) μ
hU_L :
Integrable (fun ω => Uenv (a, S.X ω) * HA.likelihoodRatio_swapA a ω) μ
hμpos :
0 < (μ {ω | S.A ω ≠ a}).toReal
conclusion
S.condMeanYofA μ a ∈ Icc ((μ {ω | S.A ω ≠ a}).toReal⁻¹ * ∫ ω in {ω | S.A ω ≠ a}, Lenv (a, S.X ω) ∂μ) ((μ {ω | S.A ω ≠ a}).toReal⁻¹ * ∫ ω in {ω | S.A ω ≠ a}, Uenv (a, S.X ω) ∂μ)
Proof (Lean source)
theorem condMeanYofA_Z_mem_Icc
(HA : POProximalSystem.ZBasedAssumptions S μ) (a : Bool)
(hAY : S.Avar.v ≠ S.Yvar.v)
(Lenv Uenv : Bool × γ_X → ℝ)
(hL : S.IsLowerEnvZ μ a Lenv) (hU : S.IsUpperEnvZ μ a Uenv)
(hLInt : Integrable (fun ω => Lenv (a, S.X ω)) μ)
(hUInt : Integrable (fun ω => Uenv (a, S.X ω)) μ)
(hL_q :
Integrable (fun ω => Lenv (a, S.X ω) * HA.q (S.Z ω, a, S.X ω)) μ)
(hU_q :
Integrable (fun ω => Uenv (a, S.X ω) * HA.q (S.Z ω, a, S.X ω)) μ)
(hL_L :
Integrable (fun ω => Lenv (a, S.X ω) * HA.likelihoodRatio_swapA a ω) μ)
(hU_L :
Integrable (fun ω => Uenv (a, S.X ω) * HA.likelihoodRatio_swapA a ω) μ)
(hμpos : 0 < (μ {ω | S.A ω ≠ a}).toReal) :
S.condMeanYofA μ a ∈ Icc
((μ {ω | S.A ω ≠ a}).toReal⁻¹ * ∫ ω in {ω | S.A ω ≠ a}, Lenv (a, S.X ω) ∂μ)
((μ {ω | S.A ω ≠ a}).toReal⁻¹ * ∫ ω in {ω | S.A ω ≠ a}, Uenv (a, S.X ω) ∂μ) := by
have h := condMeanYofA_Z_bounds HA a hAY Lenv Uenv hL hU
hLInt hUInt hL_q hU_q hL_L hU_L hμpos
exact mem_Icc_of_sandwich h.1 h.2
theorem meanYofA_Z_mem_Icc reviewed
⚑ flagged
Causalean.PO.POProximalSystem
Set.Icc form of Corollary 2 (meanYofA_Z_bounds). Fix a treatment arm a and assume the Z-only proximal bridge assumption bundle, with the treatment and outcome variables distinct; let Lenv, Uenv be lower and upper envelope functions bounding the σ(A,Z,X)-conditional mean of the outcome on the on-arm stratum, assumed integrable, with the envelope weighted by the treatment-proxy bridge and the envelope weighted by the likelihood-ratio arm-swap factor both integrable. Then the marginal target E[Y(a)] lies in the closed interval spanned by the Z-proxy marginal envelope integrals, the Set.Icc membership restatement of the scalar sandwich bound meanYofA_Z_bounds.
Formal statement
hypotheses
HA :
POProximalSystem.ZBasedAssumptions S μ
a :
hAY :
S.Avar.v ≠ S.Yvar.v
Lenv Uenv :
Bool × γ_X → ℝ
hL :
S.IsLowerEnvZ μ a Lenv
hU :
S.IsUpperEnvZ μ a Uenv
hLInt :
Integrable (fun ω => Lenv (a, S.X ω)) μ
hUInt :
Integrable (fun ω => Uenv (a, S.X ω)) μ
hL_q :
Integrable (fun ω => Lenv (a, S.X ω) * HA.q (S.Z ω, a, S.X ω)) μ
hU_q :
Integrable (fun ω => Uenv (a, S.X ω) * HA.q (S.Z ω, a, S.X ω)) μ
hL_L :
Integrable (fun ω => Lenv (a, S.X ω) * HA.likelihoodRatio_swapA a ω) μ
hU_L :
Integrable (fun ω => Uenv (a, S.X ω) * HA.likelihoodRatio_swapA a ω) μ
conclusion
S.meanYofA μ a ∈ Icc ((∫ ω in {ω | S.A ω ≠ a}, Lenv (a, S.X ω) ∂μ) + (∫ ω in {ω | S.A ω = a}, S.Y ω ∂μ)) ((∫ ω in {ω | S.A ω ≠ a}, Uenv (a, S.X ω) ∂μ) + (∫ ω in {ω | S.A ω = a}, S.Y ω ∂μ))
Proof (Lean source)
theorem meanYofA_Z_mem_Icc
(HA : POProximalSystem.ZBasedAssumptions S μ) (a : Bool)
(hAY : S.Avar.v ≠ S.Yvar.v)
(Lenv Uenv : Bool × γ_X → ℝ)
(hL : S.IsLowerEnvZ μ a Lenv) (hU : S.IsUpperEnvZ μ a Uenv)
(hLInt : Integrable (fun ω => Lenv (a, S.X ω)) μ)
(hUInt : Integrable (fun ω => Uenv (a, S.X ω)) μ)
(hL_q :
Integrable (fun ω => Lenv (a, S.X ω) * HA.q (S.Z ω, a, S.X ω)) μ)
(hU_q :
Integrable (fun ω => Uenv (a, S.X ω) * HA.q (S.Z ω, a, S.X ω)) μ)
(hL_L :
Integrable (fun ω => Lenv (a, S.X ω) * HA.likelihoodRatio_swapA a ω) μ)
(hU_L :
Integrable (fun ω => Uenv (a, S.X ω) * HA.likelihoodRatio_swapA a ω) μ) :
S.meanYofA μ a ∈ Icc
((∫ ω in {ω | S.A ω ≠ a}, Lenv (a, S.X ω) ∂μ)
+ (∫ ω in {ω | S.A ω = a}, S.Y ω ∂μ))
((∫ ω in {ω | S.A ω ≠ a}, Uenv (a, S.X ω) ∂μ)
+ (∫ ω in {ω | S.A ω = a}, S.Y ω ∂μ)) := by
have h := meanYofA_Z_bounds HA a hAY Lenv Uenv hL hU
hLInt hUInt hL_q hU_q hL_L hU_L
exact mem_Icc_of_sandwich h.1 h.2
theorem condMeanYofA_WZ_mem_Icc reviewed
⚑ flagged
Causalean.PO.POProximalSystem
Set.Icc form of Theorem 3 (condMeanYofA_WZ_bounds). Fix a treatment arm a and assume the two-proxy bridge assumption bundle, with the treatment and outcome variables distinct; let Lenv, Uenv be lower and upper envelope functions bounding the same-arm joint-versus-product W-Z density ratio, with the off-arm stratum of positive mass and the envelope-weighted product of the two conditional bridge means integrable. Then the conditional target E[Y(a) ∣ A ≠ a] lies in the closed interval spanned by the essential Y-bounds and the joint-WZ envelope clamps, the Set.Icc membership restatement of the scalar sandwich bound condMeanYofA_WZ_bounds.
Formal statement
hypotheses
HA :
POProximalSystem.TwoProxyAssumptions S μ
a :
hAY :
S.Avar.v ≠ S.Yvar.v
Lenv Uenv :
Bool × γ_X → ℝ
hL :
S.IsLowerEnvWZ μ a Lenv
hU :
S.IsUpperEnvWZ μ a Uenv
hμpos :
0 < (μ {ω | S.A ω ≠ a}).toReal
hU_envInt :
Integrable (fun ω => Uenv (a, S.X ω) * (μ[fun ω' => HA.h (a, S.W ω', S.X ω') | S.σ_AX]) ω * (μ[fun ω' => HA.q (S.Z ω', a, S.X ω') | S.σ_AX]) ω) μ
hL_envInt :
Integrable (fun ω => Lenv (a, S.X ω) * (μ[fun ω' => HA.h (a, S.W ω', S.X ω') | S.σ_AX]) ω * (μ[fun ω' => HA.q (S.Z ω', a, S.X ω') | S.σ_AX]) ω) μ
conclusion
S.condMeanYofA μ a ∈ Icc (max (choose HA.Y_bdd_below) ((μ {ω | S.A ω ≠ a}).toReal⁻¹ * ∫ ω in {ω | S.A ω = a}, S.stratumOddsRatio μ a ω * Lenv (a, S.X ω) * (μ[S.Y | S.σ_AX]) ω ∂μ)) (min (choose HA.Y_bdd_above) ((μ {ω | S.A ω ≠ a}).toReal⁻¹ * ∫ ω in {ω | S.A ω = a}, S.stratumOddsRatio μ a ω * Uenv (a, S.X ω) * (μ[S.Y | S.σ_AX]) ω ∂μ))
Proof (Lean source)
theorem condMeanYofA_WZ_mem_Icc
(HA : POProximalSystem.TwoProxyAssumptions S μ) (a : Bool)
(hAY : S.Avar.v ≠ S.Yvar.v)
(Lenv Uenv : Bool × γ_X → ℝ)
(hL : S.IsLowerEnvWZ μ a Lenv) (hU : S.IsUpperEnvWZ μ a Uenv)
(hμpos : 0 < (μ {ω | S.A ω ≠ a}).toReal)
(hU_envInt : Integrable (fun ω =>
Uenv (a, S.X ω)
* (μ[fun ω' => HA.h (a, S.W ω', S.X ω') | S.σ_AX]) ω
* (μ[fun ω' => HA.q (S.Z ω', a, S.X ω') | S.σ_AX]) ω) μ)
(hL_envInt : Integrable (fun ω =>
Lenv (a, S.X ω)
* (μ[fun ω' => HA.h (a, S.W ω', S.X ω') | S.σ_AX]) ω
* (μ[fun ω' => HA.q (S.Z ω', a, S.X ω') | S.σ_AX]) ω) μ) :
S.condMeanYofA μ a ∈ Icc
(max (choose HA.Y_bdd_below)
((μ {ω | S.A ω ≠ a}).toReal⁻¹ *
∫ ω in {ω | S.A ω = a},
S.stratumOddsRatio μ a ω * Lenv (a, S.X ω) * (μ[S.Y | S.σ_AX]) ω ∂μ))
(min (choose HA.Y_bdd_above)
((μ {ω | S.A ω ≠ a}).toReal⁻¹ *
∫ ω in {ω | S.A ω = a},
S.stratumOddsRatio μ a ω * Uenv (a, S.X ω) * (μ[S.Y | S.σ_AX]) ω ∂μ)) := by
have h := condMeanYofA_WZ_bounds HA a hAY Lenv Uenv hL hU hμpos
hU_envInt hL_envInt
exact mem_Icc_of_sandwich h.1 h.2
TwoProxy 1 core · 0 supporting This file proves the two-proxy proximal partial-identification sandwich for the off-arm counterfactual mean. ★ condMeanYofA_WZ_bounds
Two-proxy proximal partial-identification bounds
This file proves the two-proxy proximal partial-identification sandwich for the
off-arm counterfactual mean. The bridge-substitution identity
condIntYofA_eq_hq_armSwap_twoProxy moves the target to the observed treatment
arm; the joint W-Z envelope predicates IsLowerEnvWZ and IsUpperEnvWZ then
bound the bridge product by observable conditional means and stratum odds
ratios.
The main declaration is condMeanYofA_WZ_bounds, the Theorem 3 bound for
condMeanYofA. Its public statement contains only observable objects:
stratumOddsRatio, the envelope functions, and μ[Y | σ_AX]; the latent
bridges h and q are eliminated by the conditional-expectation collapse
lemmas.
theorem condMeanYofA_WZ_bounds reviewed
⚑ flagged
Causalean.PO.POProximalSystem
Theorem 3 (Ghassami-Shpitser-Tchetgen Tchetgen 2024, two-proxy partial identification). Fix a treatment arm a and assume the two-proxy assumption bundle — consistency, latent exchangeability, conditional independence of the proxies W and Z given treatment and covariates, the outcome and treatment-proxy bridges, and essential bounds on Y — together with the treatment and outcome variables being distinct; let Lenv, Uenv be lower and upper envelope functions bounding the same-arm joint-versus-product density ratio of the two proxies, with the off-arm stratum of positive mass and the envelope-weighted product of the outcome- and treatment-proxy conditional bridge means integrable. Then the conditional target E[Y(a) ∣ A ≠ a] is sandwiched between the essential Y-bounds and the integrated envelope bound, expressed entirely through observable quantities — the stratum odds ratio, the envelope functions, and the observed conditional mean of Y.
Formal statement
hypotheses
HA :
POProximalSystem.TwoProxyAssumptions S μ
a :
hAY :
S.Avar.v ≠ S.Yvar.v
Lenv Uenv :
Bool × γ_X → ℝ
hL :
S.IsLowerEnvWZ μ a Lenv
hU :
S.IsUpperEnvWZ μ a Uenv
hμpos :
0 < (μ {ω | S.A ω ≠ a}).toReal
Phase B integrability hypotheses (per project decision): the paper assumes implicit boundedness of the envelope and odds-ratio, which would make these L¹. We surface them as hypotheses here.
hU_envInt :
Integrable (fun ω => Uenv (a, S.X ω) * (μ[fun ω' => HA.h (a, S.W ω', S.X ω') | S.σ_AX]) ω * (μ[fun ω' => HA.q (S.Z ω', a, S.X ω') | S.σ_AX]) ω) μ
hL_envInt :
Integrable (fun ω => Lenv (a, S.X ω) * (μ[fun ω' => HA.h (a, S.W ω', S.X ω') | S.σ_AX]) ω * (μ[fun ω' => HA.q (S.Z ω', a, S.X ω') | S.σ_AX]) ω) μ
Proof (Lean source)
theorem condMeanYofA_WZ_bounds
(HA : POProximalSystem.TwoProxyAssumptions S μ) (a : Bool)
(hAY : S.Avar.v ≠ S.Yvar.v)
(Lenv Uenv : Bool × γ_X → ℝ)
(hL : S.IsLowerEnvWZ μ a Lenv) (hU : S.IsUpperEnvWZ μ a Uenv)
(hμpos : 0 < (μ {ω | S.A ω ≠ a}).toReal)
-- Phase B integrability hypotheses (per project decision):
-- the paper assumes implicit boundedness of the envelope and odds-ratio,
-- which would make these L¹. We surface them as hypotheses here.
(hU_envInt : Integrable (fun ω =>
Uenv (a, S.X ω)
* (μ[fun ω' => HA.h (a, S.W ω', S.X ω') | S.σ_AX]) ω
* (μ[fun ω' => HA.q (S.Z ω', a, S.X ω') | S.σ_AX]) ω) μ)
(hL_envInt : Integrable (fun ω =>
Lenv (a, S.X ω)
* (μ[fun ω' => HA.h (a, S.W ω', S.X ω') | S.σ_AX]) ω
* (μ[fun ω' => HA.q (S.Z ω', a, S.X ω') | S.σ_AX]) ω) μ) :
max (Classical.choose HA.Y_bdd_below)
((μ {ω | S.A ω ≠ a}).toReal⁻¹ *
∫ ω in {ω | S.A ω = a},
S.stratumOddsRatio μ a ω * Lenv (a, S.X ω) * (μ[S.Y | S.σ_AX]) ω ∂μ)
≤ S.condMeanYofA μ a
∧ S.condMeanYofA μ a ≤
min (Classical.choose HA.Y_bdd_above)
((μ {ω | S.A ω ≠ a}).toReal⁻¹ *
∫ ω in {ω | S.A ω = a},
S.stratumOddsRatio μ a ω * Uenv (a, S.X ω) * (μ[S.Y | S.σ_AX]) ω ∂μ)
:= by
-- Notation.
set s' : Set P.Ω := {ω | S.A ω ≠ a} with hs'_def
set s : Set P.Ω := {ω | S.A ω = a} with hs_def
set p : ℝ := (μ s').toReal with hp_def
-- Bridge identity (same-arm form, prob-ratio q convention — no stratumOddsRatio):
-- ∫_{A≠a} Y(a) dμ = ∫_{A=a} h(a,W,X) · q(Z,a,X) dμ.
have hBridge : (∫ ω in s', S.YofA a ω ∂μ)
= ∫ ω in s, HA.h (a, S.W ω, S.X ω) * HA.q (S.Z ω, a, S.X ω) ∂μ :=
POProximalSystem.condIntYofA_eq_hq_armSwap_twoProxy HA a hAY
have hp_inv_nn : 0 ≤ p⁻¹ := le_of_lt (inv_pos.mpr hμpos)
-- Trivial clamps via essential Y bounds (independent of the envelope chain).
have hU_triv : S.condMeanYofA μ a ≤ Classical.choose HA.Y_bdd_above := by
set M : ℝ := Classical.choose HA.Y_bdd_above with hM_def
have hM : ∀ᵐ ω ∂μ, S.Y ω ≤ M := Classical.choose_spec HA.Y_bdd_above
have hYa : ∀ᵐ ω ∂μ, S.YofA a ω ≤ M :=
POProximalSystem.YofA_essbound_above HA.consistency (HA.latent_exch a) hAY
(HA.overlap_strong a) hM
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 hYaInt : Integrable (S.YofA a) μ := HA.integrable_YofA a
have h_le : (∫ ω in s', S.YofA a ω ∂μ) ≤ ∫ _ in s', M ∂μ := by
refine setIntegral_mono_ae ?_ ?_ hYa
· exact hYaInt.integrableOn
· exact integrableOn_const
have h_const : (∫ _ in s', M ∂μ) = M * p := by
rw [setIntegral_const]
simp [hp_def, MeasureTheory.measureReal_def, mul_comm]
have h_int_le : (∫ ω in s', S.YofA a ω ∂μ) ≤ M * p := h_le.trans_eq h_const
have hgoal : p⁻¹ * (∫ ω in s', S.YofA a ω ∂μ) ≤ p⁻¹ * (M * p) :=
mul_le_mul_of_nonneg_left h_int_le hp_inv_nn
have hp_ne : p ≠ 0 := ne_of_gt hμpos
have h_eq : p⁻¹ * (M * p) = M := by field_simp
rw [h_eq] at hgoal
unfold POProximalSystem.condMeanYofA
exact hgoal
have hL_triv : Classical.choose HA.Y_bdd_below ≤ S.condMeanYofA μ a := by
set M : ℝ := Classical.choose HA.Y_bdd_below with hM_def
have hM : ∀ᵐ ω ∂μ, M ≤ S.Y ω := Classical.choose_spec HA.Y_bdd_below
have hYa : ∀ᵐ ω ∂μ, M ≤ S.YofA a ω :=
POProximalSystem.YofA_essbound_below HA.consistency (HA.latent_exch a) hAY
(HA.overlap_strong a) hM
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 hYaInt : Integrable (S.YofA a) μ := HA.integrable_YofA a
have h_le : (∫ _ in s', M ∂μ) ≤ ∫ ω in s', S.YofA a ω ∂μ := by
refine setIntegral_mono_ae ?_ ?_ hYa
· exact integrableOn_const
· exact hYaInt.integrableOn
have h_const : (∫ _ in s', M ∂μ) = M * p := by
rw [setIntegral_const]
simp [hp_def, MeasureTheory.measureReal_def, mul_comm]
have h_int_le : M * p ≤ (∫ ω in s', S.YofA a ω ∂μ) := h_const ▸ h_le
have hgoal : p⁻¹ * (M * p) ≤ p⁻¹ * (∫ ω in s', S.YofA a ω ∂μ) :=
mul_le_mul_of_nonneg_left h_int_le hp_inv_nn
have hp_ne : p ≠ 0 := ne_of_gt hμpos
have h_eq : p⁻¹ * (M * p) = M := by field_simp
rw [h_eq] at hgoal
unfold POProximalSystem.condMeanYofA
exact hgoal
-- ============================================================
-- ENVELOPE CHAIN (same-arm; no fiber transport)
--
-- After the same-arm bridge identity ∫_{A≠a} Y(a) dμ = ∫_{A=a} h·q dμ,
-- both sides of the envelope chain live on `{A = a}`. Internal chain
-- (one direction shown):
--
-- ∫_{A=a} h(a,W,X) · q(Z,a,X) dμ
-- = ∫_{A=a} μ[h · q | σ_AX] dμ (σ_AX pull-out)
-- ≤ ∫_{A=a} Uenv(a,X) · μ[h|σ_AX] · μ[q|σ_AX] dμ (hU.2)
-- = ∫_{A=a} Uenv(a,X) · μ[Y|σ_AX] · stratumOddsRatio dμ
-- (helpers: μ[h|σ_AX]→μ[Y|σ_AX],
-- μ[q|σ_AX]→stratumOddsRatio
-- on `restrict {A=a}`)
-- = ∫_{A=a} stratumOddsRatio · Uenv(a,X) · μ[Y|σ_AX] dμ.
--
-- The σ_AX-pull-out step is identical to the W-only case in `WBased.lean`.
-- The two collapses use existing helpers:
-- `condExp_Y_eq_condExp_h_arm_AX` and
-- `condExp_q_eq_stratumOddsRatio_arm_AX`.
-- ============================================================
-- Notation for the bridge factors and their measurability.
set φW : γ_W × γ_X → ℝ := fun p => HA.h (a, p.1, p.2) with hφW_def
set φZ : γ_Z × γ_X → ℝ := fun p => HA.q (p.1, a, p.2) with hφZ_def
have hφW_meas : Measurable φW := by
have : Measurable (fun p : γ_W × γ_X => (a, p.1, p.2)) :=
prodMk measurable_const
(prodMk measurable_fst measurable_snd)
exact HA.measurable_h.comp this
have hφZ_meas : Measurable φZ := by
have : Measurable (fun p : γ_Z × γ_X => (p.1, a, p.2)) :=
prodMk measurable_fst
(prodMk measurable_const measurable_snd)
exact HA.measurable_q.comp this
have hφW_nn : ∀ x, 0 ≤ φW x := fun _ => HA.h_nonneg _
have hφZ_nn : ∀ x, 0 ≤ φZ x := fun _ => HA.q_nonneg _
-- Integrabilities for the envelope predicate.
have hφW_int : Integrable (fun ω => φW (S.W ω, S.X ω)) μ :=
HA.integrable_h_arm a
have hφZ_int : Integrable (fun ω => φZ (S.Z ω, S.X ω)) μ :=
HA.integrable_q a
have hφWZ_int : Integrable
(fun ω => φW (S.W ω, S.X ω) * φZ (S.Z ω, S.X ω)) μ :=
HA.integrable_hq_arm a
-- σ_AX-measurability of {A = a}.
have hs_meas : MeasurableSet s := S.measurable_A (measurableSet_singleton a)
have hs_in_AX : MeasurableSet[S.σ_AX] s := by
refine ⟨Prod.fst ⁻¹' {a}, ?_, ?_⟩
· exact measurable_fst (measurableSet_singleton a)
· ext ω; simp [s, POProximalSystem.AX]
-- Collapse identities.
have hCollapse_h :
μ[S.Y | S.σ_AX] =ᵐ[μ.restrict s]
μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AX] :=
POProximalSystem.condExp_Y_eq_condExp_h_arm_AX_twoProxy HA a hAY
have hCollapse_q :
(μ[fun ω => HA.q (S.Z ω, a, S.X ω) | S.σ_AX])
=ᵐ[μ.restrict s] S.stratumOddsRatio μ a :=
POProximalSystem.condExp_q_eq_stratumOddsRatio_arm_AX HA a hAY
-- Step (ii): σ_AX pull-out.
have hPull : ∫ ω in s,
HA.h (a, S.W ω, S.X ω) * HA.q (S.Z ω, a, S.X ω) ∂μ
= ∫ ω in s,
(μ[fun ω => φW (S.W ω, S.X ω) * φZ (S.Z ω, S.X ω) | S.σ_AX]) ω ∂μ := by
have h_setInt :
∫ ω in s,
(μ[fun ω => φW (S.W ω, S.X ω) * φZ (S.Z ω, S.X ω) | S.σ_AX]) ω ∂μ
= ∫ ω in s, φW (S.W ω, S.X ω) * φZ (S.Z ω, S.X ω) ∂μ :=
setIntegral_condExp S.σ_AX_le hφWZ_int hs_in_AX
simp only [φW, φZ] at h_setInt ⊢
exact h_setInt.symm
-- Step (iii): apply hU.2 envelope and integrate.
have hEnvAE := hU.2 φW φZ hφW_meas hφZ_meas hφW_nn hφZ_nn hφWZ_int hφW_int hφZ_int
-- The envelope-bound integrand on the rhs.
have hEnvBound_int : IntegrableOn
(fun ω => Uenv (a, S.X ω)
* (μ[fun ω' => φW (S.W ω', S.X ω') | S.σ_AX]) ω
* (μ[fun ω' => φZ (S.Z ω', S.X ω') | S.σ_AX]) ω) s μ := by
simp only [φW, φZ]
exact hU_envInt.integrableOn
have hCondMul_int : IntegrableOn
(fun ω => (μ[fun ω => φW (S.W ω, S.X ω) * φZ (S.Z ω, S.X ω) | S.σ_AX]) ω) s μ :=
integrable_condExp.integrableOn
-- setIntegral_mono_ae over {A = a}.
have hMono :
∫ ω in s, (μ[fun ω => φW (S.W ω, S.X ω) * φZ (S.Z ω, S.X ω) | S.σ_AX]) ω ∂μ
≤ ∫ ω in s,
Uenv (a, S.X ω)
* (μ[fun ω' => φW (S.W ω', S.X ω') | S.σ_AX]) ω
* (μ[fun ω' => φZ (S.Z ω', S.X ω') | S.σ_AX]) ω ∂μ :=
setIntegral_mono_ae_restrict hCondMul_int hEnvBound_int hEnvAE
-- Step (iv)+(v): collapse h → Y and q → stratumOddsRatio on {A=a}, and rearrange.
have hRewrite :
∫ ω in s,
Uenv (a, S.X ω)
* (μ[fun ω' => φW (S.W ω', S.X ω') | S.σ_AX]) ω
* (μ[fun ω' => φZ (S.Z ω', S.X ω') | S.σ_AX]) ω ∂μ
= ∫ ω in s,
S.stratumOddsRatio μ a ω * Uenv (a, S.X ω) * (μ[S.Y | S.σ_AX]) ω ∂μ := by
refine integral_congr_ae ?_
filter_upwards [hCollapse_h, hCollapse_q] with ω hh hq
simp only [φW, φZ] at *
rw [hh, hq]; ring
-- Assemble.
have hU_arm : (∫ ω in s', S.YofA a ω ∂μ)
≤ ∫ ω in s,
S.stratumOddsRatio μ a ω * Uenv (a, S.X ω)
* (μ[S.Y | S.σ_AX]) ω ∂μ := by
rw [hBridge, hPull]
exact hMono.trans (le_of_eq hRewrite)
-- ----- LOWER -----
have hEnvAE_L := hL.2 φW φZ hφW_meas hφZ_meas hφW_nn hφZ_nn hφWZ_int hφW_int hφZ_int
have hEnvBound_L_int : IntegrableOn
(fun ω => Lenv (a, S.X ω)
* (μ[fun ω' => φW (S.W ω', S.X ω') | S.σ_AX]) ω
* (μ[fun ω' => φZ (S.Z ω', S.X ω') | S.σ_AX]) ω) s μ := by
simp only [φW, φZ]
exact hL_envInt.integrableOn
have hMono_L :
∫ ω in s,
-- … truncated; follow the source link for the rest …
WBased 2 core · 0 supporting This file proves the W-only proximal partial-identification bounds of Ghassami-Shpitser-Tchetgen Tchetgen for a potential-outcome system with an outcome-inducing proxy W. ★ condMeanYofA_W_bounds★ meanYofA_W_bounds
W-based proximal partial-identification bounds
This file proves the W-only proximal partial-identification bounds of
Ghassami-Shpitser-Tchetgen Tchetgen for a potential-outcome system with an
outcome-inducing proxy W. The outcome bridge rewrites the off-arm target
E[Y(a) | A != a] as a bridge moment, and the W-density-ratio envelope
predicates IsLowerEnvW and IsUpperEnvW turn that moment into observable
integrals over the on-arm stratum.
Main declarations:
* condMeanYofA_W_bounds is the conditional Theorem 1 sandwich for
condMeanYofA, combining the envelope bounds with the trivial essential
bounds on Y.
* meanYofA_W_bounds is the marginal Corollary 1 sandwich for meanYofA,
obtained by adding the consistency-identified {A = a} contribution.
theorem condMeanYofA_W_bounds reviewed
⚑ flagged
Causalean.PO.POProximalSystem
Theorem 1 (Ghassami-Shpitser-Tchetgen Tchetgen 2024, W-only partial identification). Fix a treatment arm a and assume the W-only assumption bundle — consistency, latent exchangeability, independence of the proxy W from treatment given the latent confounder and covariates, the outcome bridge, and essential bounds on Y — together with the treatment and outcome variables being distinct; let Lenv, Uenv be lower and upper envelope functions bounding the W-proxy density ratio, with the off-arm stratum of positive mass and the envelope-weighted bridge moments integrable. Then the conditional target E[Y(a) ∣ A ≠ a] lies between the trivial essential-Y bound and the integrated envelope bound on each side.
Formal statement
hypotheses
HA :
POProximalSystem.WBasedAssumptions S μ
a :
hAY :
S.Avar.v ≠ S.Yvar.v
Lenv Uenv :
Bool × γ_X → ℝ
hL :
S.IsLowerEnvW μ a Lenv
hU :
S.IsUpperEnvW μ a Uenv
hμpos :
0 < (μ {ω | S.A ω ≠ a}).toReal
hU_int_h :
Integrable (fun ω => S.stratumOddsRatio μ a ω * Uenv (a, S.X ω) * HA.h (a, S.W ω, S.X ω)) μ
hL_int_h :
Integrable (fun ω => S.stratumOddsRatio μ a ω * Lenv (a, S.X ω) * HA.h (a, S.W ω, S.X ω)) μ
Proof (Lean source)
theorem condMeanYofA_W_bounds
(HA : POProximalSystem.WBasedAssumptions S μ) (a : Bool)
(hAY : S.Avar.v ≠ S.Yvar.v)
(Lenv Uenv : Bool × γ_X → ℝ)
(hL : S.IsLowerEnvW μ a Lenv) (hU : S.IsUpperEnvW μ a Uenv)
(hμpos : 0 < (μ {ω | S.A ω ≠ a}).toReal)
(hU_int_h : Integrable
(fun ω => S.stratumOddsRatio μ a ω * Uenv (a, S.X ω) *
HA.h (a, S.W ω, S.X ω)) μ)
(hL_int_h : Integrable
(fun ω => S.stratumOddsRatio μ a ω * Lenv (a, S.X ω) *
HA.h (a, S.W ω, S.X ω)) μ) :
max (Classical.choose HA.Y_bdd_below)
((μ {ω | S.A ω ≠ a}).toReal⁻¹ *
∫ ω in {ω | S.A ω = a},
S.stratumOddsRatio μ a ω * Lenv (a, S.X ω) * (μ[S.Y | S.σ_AX]) ω ∂μ)
≤ S.condMeanYofA μ a
∧ S.condMeanYofA μ a ≤
min (Classical.choose HA.Y_bdd_above)
((μ {ω | S.A ω ≠ a}).toReal⁻¹ *
∫ ω in {ω | S.A ω = a},
S.stratumOddsRatio μ a ω * Uenv (a, S.X ω) * (μ[S.Y | S.σ_AX]) ω ∂μ)
:= by
-- Notation.
set s' : Set P.Ω := {ω | S.A ω ≠ a} with hs'_def
set s : Set P.Ω := {ω | S.A ω = a} with hs_def
set p : ℝ := (μ s').toReal with hp_def
-- φ : the bridge integrand viewed as a function of (W, X).
let φ : γ_W × γ_X → ℝ := fun wx => HA.h (a, wx.1, wx.2)
-- Measurability of φ.
have h_meas_φ : Measurable φ := by
have hp : Measurable (fun wx : γ_W × γ_X => (a, wx.1, wx.2)) := by
refine Measurable.prodMk measurable_const ?_
exact Measurable.prodMk measurable_fst measurable_snd
exact HA.measurable_h.comp hp
-- Integrability of `ω ↦ φ (W ω, X ω) = h(a, W ω, X ω)`.
have h_int_φ : Integrable (fun ω => φ (S.W ω, S.X ω)) μ := HA.integrable_h_arm a
-- Bridge substitution: ∫_{A≠a} Y(a) dμ = ∫_{A≠a} h(a, W, X) dμ.
have hBridge : (∫ ω in s', S.YofA a ω ∂μ)
= (∫ ω in s', HA.h (a, S.W ω, S.X ω) ∂μ) :=
POProximalSystem.condIntYofA_eq_h_arm HA a hAY
-- ============================================================
-- UPPER BOUND
-- ============================================================
-- Step U1: nonnegativity of φ. The paper assumes Y ≥ 0 ⇒ h ≥ 0. The
-- WBased bundle does not bundle nonnegativity of `h`; this is the same
-- gap as in `TwoProxy.lean`.
have h_nonneg_φ : ∀ x, 0 ≤ φ x := by
intro x; exact HA.h_nonneg _
-- Step U2: apply the upper envelope predicate to φ.
have hU_int : ∫ ω in s', φ (S.W ω, S.X ω) ∂μ
≤ ∫ ω in s,
S.stratumOddsRatio μ a ω * Uenv (a, S.X ω) * φ (S.W ω, S.X ω) ∂μ :=
hU.2 φ h_meas_φ h_nonneg_φ h_int_φ hU_int_h
-- Step U3: chain bridge + envelope to bound ∫_{A≠a} Y(a).
have hU_arm : (∫ ω in s', S.YofA a ω ∂μ)
≤ ∫ ω in s,
S.stratumOddsRatio μ a ω * Uenv (a, S.X ω) * HA.h (a, S.W ω, S.X ω) ∂μ := by
rw [hBridge]; exact hU_int
-- Step U4: divide by μ(s').toReal to get a bound on `condMeanYofA`.
have hp_inv_nn : 0 ≤ p⁻¹ := le_of_lt (inv_pos.mpr hμpos)
-- Collapse: rewrite the integral on {A=a} with `h(a,W,X)` factor as
-- the same integral with `μ[Y | σ_AX]` factor. Strategy:
-- (i) σ_AX-measurable factor `f := stratumOddsRatio · Uenv(a,X)`
-- pulls into the conditional expectation:
-- μ[f · h(a,W,X) | σ_AX] =ᵐ f · μ[h(a,W,X) | σ_AX].
-- (ii) `setIntegral_condExp` on σ_AX-meas set s = {A=a} gives
-- ∫_s f · h(a,W,X) dμ = ∫_s μ[f · h(a,W,X) | σ_AX] dμ.
-- (iii) Combine: ∫_s f · h(a,W,X) dμ = ∫_s f · μ[h(a,W,X) | σ_AX] dμ.
-- (iv) Collapse helper on s: μ[h(a,W,X)|σ_AX] =ᵐ μ[Y|σ_AX] on `restrict s`.
-- (v) Hence ∫_s f · μ[h(a,W,X) | σ_AX] dμ = ∫_s f · μ[Y | σ_AX] dμ
-- (`integral_congr_ae`).
have hs_meas : MeasurableSet s := S.measurable_A (measurableSet_singleton a)
have hs_in_AX : MeasurableSet[S.σ_AX] s := by
refine ⟨Prod.fst ⁻¹' {a}, ?_, ?_⟩
· exact measurable_fst (measurableSet_singleton a)
· ext ω; simp [s, POProximalSystem.AX]
have hCollapse :
μ[S.Y | S.σ_AX] =ᵐ[μ.restrict s]
μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AX] :=
POProximalSystem.condExp_Y_eq_condExp_h_arm_AX HA a hAY
-- σ_X / σ_AX strong-measurability of the envelope-and-X factor.
have hX_σX : Measurable[S.σ_X] S.X := Measurable.of_comap_le le_rfl
have hUenv_σX : Measurable[S.σ_X] (fun ω => Uenv (a, S.X ω)) := by
have hU_meas : Measurable Uenv := hU.1
have hpair : Measurable[S.σ_X] (fun ω => (a, S.X ω)) :=
Measurable.prodMk measurable_const hX_σX
exact hU_meas.comp hpair
have hLenv_σX : Measurable[S.σ_X] (fun ω => Lenv (a, S.X ω)) := by
have hL_meas : Measurable Lenv := hL.1
have hpair : Measurable[S.σ_X] (fun ω => (a, S.X ω)) :=
Measurable.prodMk measurable_const hX_σX
exact hL_meas.comp hpair
have hSOR_σX : StronglyMeasurable[S.σ_X] (S.stratumOddsRatio μ a) := by
unfold POProximalSystem.stratumOddsRatio
refine ((stronglyMeasurable_condExp.measurable).div
(stronglyMeasurable_condExp.measurable)).stronglyMeasurable
have hUenv_σAX : Measurable[S.σ_AX] (fun ω => Uenv (a, S.X ω)) :=
hUenv_σX.mono S.σ_X_le_σ_AX le_rfl
have hLenv_σAX : Measurable[S.σ_AX] (fun ω => Lenv (a, S.X ω)) :=
hLenv_σX.mono S.σ_X_le_σ_AX le_rfl
have hSOR_σAX : StronglyMeasurable[S.σ_AX] (S.stratumOddsRatio μ a) :=
hSOR_σX.mono S.σ_X_le_σ_AX
have hfU_sm : StronglyMeasurable[S.σ_AX]
(fun ω => S.stratumOddsRatio μ a ω * Uenv (a, S.X ω)) :=
hSOR_σAX.mul hUenv_σAX.stronglyMeasurable
have hfL_sm : StronglyMeasurable[S.σ_AX]
(fun ω => S.stratumOddsRatio μ a ω * Lenv (a, S.X ω)) :=
hSOR_σAX.mul hLenv_σAX.stronglyMeasurable
have hh_int : Integrable (fun ω => HA.h (a, S.W ω, S.X ω)) μ :=
HA.integrable_h_arm a
-- L1 + collapse: replace `h(a,W,X)` with `μ[Y|σ_AX]` on the {A=a} integral.
have hU_collapse : (∫ ω in s,
S.stratumOddsRatio μ a ω * Uenv (a, S.X ω) * HA.h (a, S.W ω, S.X ω) ∂μ)
= ∫ ω in s,
S.stratumOddsRatio μ a ω * Uenv (a, S.X ω) * (μ[S.Y | S.σ_AX]) ω ∂μ := by
have h1 :=
setIntegral_mul_condExp_of_stronglyMeasurableLeft S.σ_AX_le hfU_sm
hh_int hU_int_h hs_in_AX
have h_ae : (fun ω => S.stratumOddsRatio μ a ω * Uenv (a, S.X ω)
* (μ[fun ω' => HA.h (a, S.W ω', S.X ω')|S.σ_AX]) ω)
=ᵐ[μ.restrict s]
(fun ω => S.stratumOddsRatio μ a ω * Uenv (a, S.X ω)
* (μ[S.Y | S.σ_AX]) ω) := by
filter_upwards [hCollapse] with ω hω
simp [hω]
exact h1.trans (integral_congr_ae h_ae)
have hL_collapse : (∫ ω in s,
S.stratumOddsRatio μ a ω * Lenv (a, S.X ω) * HA.h (a, S.W ω, S.X ω) ∂μ)
= ∫ ω in s,
S.stratumOddsRatio μ a ω * Lenv (a, S.X ω) * (μ[S.Y | S.σ_AX]) ω ∂μ := by
have h1 :=
setIntegral_mul_condExp_of_stronglyMeasurableLeft S.σ_AX_le hfL_sm
hh_int hL_int_h hs_in_AX
have h_ae : (fun ω => S.stratumOddsRatio μ a ω * Lenv (a, S.X ω)
* (μ[fun ω' => HA.h (a, S.W ω', S.X ω')|S.σ_AX]) ω)
=ᵐ[μ.restrict s]
(fun ω => S.stratumOddsRatio μ a ω * Lenv (a, S.X ω)
* (μ[S.Y | S.σ_AX]) ω) := by
filter_upwards [hCollapse] with ω hω
simp [hω]
exact h1.trans (integral_congr_ae h_ae)
-- Step U5 (collapse the {A=a} integral): replace `h(a,W,X)` with `μ[Y|σ_AX]`.
have hU_cond : S.condMeanYofA μ a
≤ p⁻¹ *
∫ ω in s,
S.stratumOddsRatio μ a ω * Uenv (a, S.X ω) * (μ[S.Y | S.σ_AX]) ω ∂μ := by
have hgoal := mul_le_mul_of_nonneg_left hU_arm hp_inv_nn
rw [hU_collapse] at hgoal
unfold POProximalSystem.condMeanYofA
exact hgoal
-- Step U5: trivial upper clamp via Y_bdd_above. Needs `Y(a) ≤ essup Y` a.e.
have hU_triv : S.condMeanYofA μ a ≤ Classical.choose HA.Y_bdd_above := by
set M : ℝ := Classical.choose HA.Y_bdd_above with hM_def
have hM : ∀ᵐ ω ∂μ, S.Y ω ≤ M := Classical.choose_spec HA.Y_bdd_above
have hYa : ∀ᵐ ω ∂μ, S.YofA a ω ≤ M :=
POProximalSystem.YofA_essbound_above HA.consistency (HA.latent_exch a) hAY
(HA.overlap_strong a) hM
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 hYaInt : Integrable (S.YofA a) μ := HA.integrable_YofA a
have h_le : (∫ ω in s', S.YofA a ω ∂μ) ≤ ∫ _ in s', M ∂μ := by
refine setIntegral_mono_ae ?_ ?_ hYa
· exact hYaInt.integrableOn
· exact integrableOn_const
have h_const : (∫ _ in s', M ∂μ) = M * p := by
rw [setIntegral_const]
simp [hp_def, MeasureTheory.measureReal_def, mul_comm]
have h_int_le : (∫ ω in s', S.YofA a ω ∂μ) ≤ M * p := h_le.trans_eq h_const
have hgoal : p⁻¹ * (∫ ω in s', S.YofA a ω ∂μ) ≤ p⁻¹ * (M * p) :=
mul_le_mul_of_nonneg_left h_int_le hp_inv_nn
have hp_ne : p ≠ 0 := ne_of_gt hμpos
have h_eq : p⁻¹ * (M * p) = M := by field_simp
rw [h_eq] at hgoal
unfold POProximalSystem.condMeanYofA
exact hgoal
-- ============================================================
-- LOWER BOUND (mirror of upper)
-- ============================================================
have hL_int : ∫ ω in s,
S.stratumOddsRatio μ a ω * Lenv (a, S.X ω) * φ (S.W ω, S.X ω) ∂μ
≤ ∫ ω in s', φ (S.W ω, S.X ω) ∂μ :=
hL.2 φ h_meas_φ h_nonneg_φ h_int_φ hL_int_h
have hL_arm : (∫ ω in s,
S.stratumOddsRatio μ a ω * Lenv (a, S.X ω) * HA.h (a, S.W ω, S.X ω) ∂μ)
≤ (∫ ω in s', S.YofA a ω ∂μ) := by
rw [hBridge]; exact hL_int
have hL_cond : p⁻¹ *
∫ ω in s,
S.stratumOddsRatio μ a ω * Lenv (a, S.X ω) * (μ[S.Y | S.σ_AX]) ω ∂μ
≤ S.condMeanYofA μ a := by
have hgoal := mul_le_mul_of_nonneg_left hL_arm hp_inv_nn
rw [hL_collapse] at hgoal
unfold POProximalSystem.condMeanYofA
exact hgoal
have hL_triv : Classical.choose HA.Y_bdd_below ≤ S.condMeanYofA μ a := by
set M : ℝ := Classical.choose HA.Y_bdd_below with hM_def
have hM : ∀ᵐ ω ∂μ, M ≤ S.Y ω := Classical.choose_spec HA.Y_bdd_below
have hYa : ∀ᵐ ω ∂μ, M ≤ S.YofA a ω :=
POProximalSystem.YofA_essbound_below HA.consistency (HA.latent_exch a) hAY
(HA.overlap_strong a) hM
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 hYaInt : Integrable (S.YofA a) μ := HA.integrable_YofA a
have h_le : (∫ _ in s', M ∂μ) ≤ ∫ ω in s', S.YofA a ω ∂μ := by
refine setIntegral_mono_ae ?_ ?_ hYa
· exact integrableOn_const
· exact hYaInt.integrableOn
have h_const : (∫ _ in s', M ∂μ) = M * p := by
rw [setIntegral_const]
simp [hp_def, MeasureTheory.measureReal_def, mul_comm]
have h_int_le : M * p ≤ (∫ ω in s', S.YofA a ω ∂μ) := h_const ▸ h_le
have hgoal : p⁻¹ * (M * p) ≤ p⁻¹ * (∫ ω in s', S.YofA a ω ∂μ) :=
mul_le_mul_of_nonneg_left h_int_le hp_inv_nn
have hp_ne : p ≠ 0 := ne_of_gt hμpos
have h_eq : p⁻¹ * (M * p) = M := by field_simp
rw [h_eq] at hgoal
unfold POProximalSystem.condMeanYofA
exact hgoal
-- ============================================================
-- … truncated; follow the source link for the rest …
theorem meanYofA_W_bounds reviewed
⚑ flagged
Causalean.PO.POProximalSystem
Corollary 1 (Ghassami-Shpitser-Tchetgen Tchetgen 2024, W-only marginal version). Fix a treatment arm a and assume the W-only assumption bundle, with the treatment and outcome variables distinct; let Lenv, Uenv be lower and upper envelope functions bounding the W-proxy density ratio, and assume the envelope-weighted bridge moments and the envelope-weighted observed conditional means are integrable. Then the marginal target E[Y(a)] lies between a trivial clamp and an envelope clamp on each side, plus the point-identified on-arm contribution.
Formal statement
hypotheses
HA :
POProximalSystem.WBasedAssumptions S μ
a :
hAY :
S.Avar.v ≠ S.Yvar.v
Lenv Uenv :
Bool × γ_X → ℝ
hL :
S.IsLowerEnvW μ a Lenv
hU :
S.IsUpperEnvW μ a Uenv
hU_int_h :
Integrable (fun ω => S.stratumOddsRatio μ a ω * Uenv (a, S.X ω) * HA.h (a, S.W ω, S.X ω)) μ
hL_int_h :
Integrable (fun ω => S.stratumOddsRatio μ a ω * Lenv (a, S.X ω) * HA.h (a, S.W ω, S.X ω)) μ
hU_int_Y :
Integrable (fun ω => S.stratumOddsRatio μ a ω * Uenv (a, S.X ω) * (μ[S.Y | S.σ_AX]) ω) μ
hL_int_Y :
Integrable (fun ω => S.stratumOddsRatio μ a ω * Lenv (a, S.X ω) * (μ[S.Y | S.σ_AX]) ω) μ
conclusion
max (choose HA.Y_bdd_below * (μ {ω | S.A ω ≠ a}).toReal) (∫ ω in {ω | S.A ω = a}, S.stratumOddsRatio μ a ω * Lenv (a, S.X ω) * (μ[S.Y | S.σ_AX]) ω ∂μ)
+ (∫ ω in {ω | S.A ω = a}, S.Y ω ∂μ)
≤ S.meanYofA μ a ∧
S.meanYofA μ a
≤ min (choose HA.Y_bdd_above * (μ {ω | S.A ω ≠ a}).toReal) (∫ ω in {ω | S.A ω = a}, S.stratumOddsRatio μ a ω * Uenv (a, S.X ω) * (μ[S.Y | S.σ_AX]) ω ∂μ)
+ (∫ ω in {ω | S.A ω = a}, S.Y ω ∂μ)
Proof (Lean source)
theorem meanYofA_W_bounds
(HA : POProximalSystem.WBasedAssumptions S μ) (a : Bool)
(hAY : S.Avar.v ≠ S.Yvar.v)
(Lenv Uenv : Bool × γ_X → ℝ)
(hL : S.IsLowerEnvW μ a Lenv) (hU : S.IsUpperEnvW μ a Uenv)
(hU_int_h : Integrable
(fun ω => S.stratumOddsRatio μ a ω * Uenv (a, S.X ω) *
HA.h (a, S.W ω, S.X ω)) μ)
(hL_int_h : Integrable
(fun ω => S.stratumOddsRatio μ a ω * Lenv (a, S.X ω) *
HA.h (a, S.W ω, S.X ω)) μ)
(hU_int_Y : Integrable
(fun ω => S.stratumOddsRatio μ a ω * Uenv (a, S.X ω) *
(μ[S.Y | S.σ_AX]) ω) μ)
(hL_int_Y : Integrable
(fun ω => S.stratumOddsRatio μ a ω * Lenv (a, S.X ω) *
(μ[S.Y | S.σ_AX]) ω) μ) :
max (Classical.choose HA.Y_bdd_below * (μ {ω | S.A ω ≠ a}).toReal)
(∫ ω in {ω | S.A ω = a},
S.stratumOddsRatio μ a ω * Lenv (a, S.X ω) * (μ[S.Y | S.σ_AX]) ω ∂μ)
+ (∫ ω in {ω | S.A ω = a}, S.Y ω ∂μ)
≤ S.meanYofA μ a
∧ S.meanYofA μ a ≤
min (Classical.choose HA.Y_bdd_above * (μ {ω | S.A ω ≠ a}).toReal)
(∫ ω in {ω | S.A ω = a},
S.stratumOddsRatio μ a ω * Uenv (a, S.X ω) * (μ[S.Y | S.σ_AX]) ω ∂μ)
+ (∫ ω in {ω | S.A ω = a}, S.Y ω ∂μ) := by
-- Notation.
set s' : Set P.Ω := {ω | S.A ω ≠ a} with hs'_def
set s : Set P.Ω := {ω | S.A ω = a} with hs_def
set p : ℝ := (μ s').toReal with hp_def
-- φ : the bridge integrand viewed as a function of (W, X).
let φ : γ_W × γ_X → ℝ := fun wx => HA.h (a, wx.1, wx.2)
have h_meas_φ : Measurable φ := by
have hp : Measurable (fun wx : γ_W × γ_X => (a, wx.1, wx.2)) := by
refine Measurable.prodMk measurable_const ?_
exact Measurable.prodMk measurable_fst measurable_snd
exact HA.measurable_h.comp hp
have h_int_φ : Integrable (fun ω => φ (S.W ω, S.X ω)) μ := HA.integrable_h_arm a
-- Bridge nonnegativity (paper: Y ≥ 0 ⇒ h ≥ 0).
have h_nonneg_φ : ∀ x, 0 ≤ φ x := by
intro x; exact HA.h_nonneg _
-- Bridge substitution: ∫_{A≠a} Y(a) dμ = ∫_{A≠a} h(a, W, X) dμ.
have hBridge : (∫ ω in s', S.YofA a ω ∂μ)
= (∫ ω in s', HA.h (a, S.W ω, S.X ω) ∂μ) :=
POProximalSystem.condIntYofA_eq_h_arm HA a hAY
-- Marginalisation identity: meanYofA = ∫_{A≠a} Y(a) + ∫_{A=a} Y.
have hsplit : S.meanYofA μ a
= (∫ ω in s', S.YofA a ω ∂μ) + (∫ ω in s, S.Y ω ∂μ) :=
POProximalSystem.meanYofA_eq_strata (S := S) (μ := μ)
HA.consistency a hAY (HA.integrable_YofA a)
-- {A ≠ a} is measurable.
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
-- ============================================================
-- TRIVIAL CLAMPS via essential Y bounds on the off-arm stratum.
-- ============================================================
have hU_triv_arm : (∫ ω in s', S.YofA a ω ∂μ)
≤ Classical.choose HA.Y_bdd_above * p := by
set M : ℝ := Classical.choose HA.Y_bdd_above with hM_def
have hM : ∀ᵐ ω ∂μ, S.Y ω ≤ M := Classical.choose_spec HA.Y_bdd_above
have hYa : ∀ᵐ ω ∂μ, S.YofA a ω ≤ M :=
POProximalSystem.YofA_essbound_above HA.consistency (HA.latent_exch a) hAY
(HA.overlap_strong a) hM
have hYaInt : Integrable (S.YofA a) μ := HA.integrable_YofA a
have h_le : (∫ ω in s', S.YofA a ω ∂μ) ≤ ∫ _ in s', M ∂μ := by
refine setIntegral_mono_ae ?_ ?_ hYa
· exact hYaInt.integrableOn
· exact integrableOn_const
have h_const : (∫ _ in s', M ∂μ) = M * p := by
rw [setIntegral_const]
simp [hp_def, MeasureTheory.measureReal_def, mul_comm]
exact h_le.trans_eq h_const
have hL_triv_arm : Classical.choose HA.Y_bdd_below * p
≤ (∫ ω in s', S.YofA a ω ∂μ) := by
set M : ℝ := Classical.choose HA.Y_bdd_below with hM_def
have hM : ∀ᵐ ω ∂μ, M ≤ S.Y ω := Classical.choose_spec HA.Y_bdd_below
have hYa : ∀ᵐ ω ∂μ, M ≤ S.YofA a ω :=
POProximalSystem.YofA_essbound_below HA.consistency (HA.latent_exch a) hAY
(HA.overlap_strong a) hM
have hYaInt : Integrable (S.YofA a) μ := HA.integrable_YofA a
have h_le : (∫ _ in s', M ∂μ) ≤ ∫ ω in s', S.YofA a ω ∂μ := by
refine setIntegral_mono_ae ?_ ?_ hYa
· exact integrableOn_const
· exact hYaInt.integrableOn
have h_const : (∫ _ in s', M ∂μ) = M * p := by
rw [setIntegral_const]
simp [hp_def, MeasureTheory.measureReal_def, mul_comm]
exact h_const ▸ h_le
-- ============================================================
-- ENVELOPE CLAMPS via IsUpperEnvW / IsLowerEnvW + bridge + collapse.
-- ============================================================
have hU_int : ∫ ω in s', φ (S.W ω, S.X ω) ∂μ
≤ ∫ ω in s,
S.stratumOddsRatio μ a ω * Uenv (a, S.X ω) * φ (S.W ω, S.X ω) ∂μ :=
hU.2 φ h_meas_φ h_nonneg_φ h_int_φ hU_int_h
have hL_int : ∫ ω in s,
S.stratumOddsRatio μ a ω * Lenv (a, S.X ω) * φ (S.W ω, S.X ω) ∂μ
≤ ∫ ω in s', φ (S.W ω, S.X ω) ∂μ :=
hL.2 φ h_meas_φ h_nonneg_φ h_int_φ hL_int_h
have hU_arm_h : (∫ ω in s', S.YofA a ω ∂μ)
≤ ∫ ω in s,
S.stratumOddsRatio μ a ω * Uenv (a, S.X ω) * HA.h (a, S.W ω, S.X ω) ∂μ := by
rw [hBridge]; exact hU_int
have hL_arm_h : (∫ ω in s,
S.stratumOddsRatio μ a ω * Lenv (a, S.X ω) * HA.h (a, S.W ω, S.X ω) ∂μ)
≤ (∫ ω in s', S.YofA a ω ∂μ) := by
rw [hBridge]; exact hL_int
-- Collapse step: replace `h(a,W,X)` factor with `μ[Y | σ_AX]` on `{A=a}`.
-- σ_AX-pull-out lemma `∫_s f · g dμ = ∫_s f · μ[g | σ_AX] dμ` for
-- σ_AX-measurable f and integrable g, combined with
-- `condExp_Y_eq_condExp_h_arm_AX`.
-- σ_AX-measurable set s = {A = a}.
have hs_meas : MeasurableSet s := S.measurable_A (measurableSet_singleton a)
have hs_in_AX : MeasurableSet[S.σ_AX] s := by
refine ⟨Prod.fst ⁻¹' {a}, ?_, ?_⟩
· exact measurable_fst (measurableSet_singleton a)
· ext ω; simp [s, POProximalSystem.AX]
-- Collapse identity (proved in `Helpers/Common.lean`).
have hCollapse :
μ[S.Y | S.σ_AX] =ᵐ[μ.restrict s]
μ[fun ω => HA.h (a, S.W ω, S.X ω) | S.σ_AX] :=
POProximalSystem.condExp_Y_eq_condExp_h_arm_AX HA a hAY
-- σ_X-strong-measurability of the Uenv-and-X factor (then lifted to σ_AX).
have hX_σX : Measurable[S.σ_X] S.X := Measurable.of_comap_le le_rfl
have hUenv_σX : Measurable[S.σ_X] (fun ω => Uenv (a, S.X ω)) := by
have hU_meas : Measurable Uenv := hU.1
have hpair : Measurable[S.σ_X] (fun ω => (a, S.X ω)) :=
Measurable.prodMk measurable_const hX_σX
exact hU_meas.comp hpair
have hLenv_σX : Measurable[S.σ_X] (fun ω => Lenv (a, S.X ω)) := by
have hL_meas : Measurable Lenv := hL.1
have hpair : Measurable[S.σ_X] (fun ω => (a, S.X ω)) :=
Measurable.prodMk measurable_const hX_σX
exact hL_meas.comp hpair
-- stratumOddsRatio is σ_X-strong-measurable (quotient of two σ_X condExps).
have hSOR_σX : StronglyMeasurable[S.σ_X] (S.stratumOddsRatio μ a) := by
unfold POProximalSystem.stratumOddsRatio
-- ℝ has no `ContinuousDiv` instance, so go via `Measurable.div`.
refine ((stronglyMeasurable_condExp.measurable).div
(stronglyMeasurable_condExp.measurable)).stronglyMeasurable
have hUenv_σAX : Measurable[S.σ_AX] (fun ω => Uenv (a, S.X ω)) :=
hUenv_σX.mono S.σ_X_le_σ_AX le_rfl
have hLenv_σAX : Measurable[S.σ_AX] (fun ω => Lenv (a, S.X ω)) :=
hLenv_σX.mono S.σ_X_le_σ_AX le_rfl
have hSOR_σAX : StronglyMeasurable[S.σ_AX] (S.stratumOddsRatio μ a) :=
hSOR_σX.mono S.σ_X_le_σ_AX
-- Build σ_AX-strong-measurability of f := stratumOddsRatio · Uenv(a,X).
have hfU_sm : StronglyMeasurable[S.σ_AX]
(fun ω => S.stratumOddsRatio μ a ω * Uenv (a, S.X ω)) :=
hSOR_σAX.mul hUenv_σAX.stronglyMeasurable
have hfL_sm : StronglyMeasurable[S.σ_AX]
(fun ω => S.stratumOddsRatio μ a ω * Lenv (a, S.X ω)) :=
hSOR_σAX.mul hLenv_σAX.stronglyMeasurable
-- Integrability of g₁ = h(a, W, X) (from the bundle).
have hh_int : Integrable (fun ω => HA.h (a, S.W ω, S.X ω)) μ :=
HA.integrable_h_arm a
-- Integrability of g₂ = μ[Y | σ_AX] (always integrable).
have hcondY_int : Integrable (fun ω => (μ[S.Y | S.σ_AX]) ω) μ :=
integrable_condExp
-- Caller-supplied integrability (paper's implicit "all integrals finite"
-- convention; not bundled in `WBasedAssumptions` because `Uenv`/`Lenv` are
-- theorem-level parameters). Repackage to the L1 lemma's `(f * g)` shape.
have hfU_h_int : Integrable
((fun ω => S.stratumOddsRatio μ a ω * Uenv (a, S.X ω)) *
(fun ω => HA.h (a, S.W ω, S.X ω))) μ := by
exact hU_int_h
have hfU_condY_int : Integrable
((fun ω => S.stratumOddsRatio μ a ω * Uenv (a, S.X ω)) *
(fun ω => (μ[S.Y | S.σ_AX]) ω)) μ := by
exact hU_int_Y
have hfL_h_int : Integrable
((fun ω => S.stratumOddsRatio μ a ω * Lenv (a, S.X ω)) *
(fun ω => HA.h (a, S.W ω, S.X ω))) μ := by
exact hL_int_h
have hfL_condY_int : Integrable
((fun ω => S.stratumOddsRatio μ a ω * Lenv (a, S.X ω)) *
(fun ω => (μ[S.Y | S.σ_AX]) ω)) μ := by
exact hL_int_Y
-- Apply L1 (twice on each side) and then `condExp_Y_eq_condExp_h_arm_AX`.
have hU_collapse : (∫ ω in s,
S.stratumOddsRatio μ a ω * Uenv (a, S.X ω) * HA.h (a, S.W ω, S.X ω) ∂μ)
= ∫ ω in s,
S.stratumOddsRatio μ a ω * Uenv (a, S.X ω) * (μ[S.Y | S.σ_AX]) ω ∂μ := by
-- L1 on g = h(a,W,X): ∫_s f·g = ∫_s f · μ[g|σ_AX]
have h1 :=
setIntegral_mul_condExp_of_stronglyMeasurableLeft S.σ_AX_le hfU_sm
hh_int hfU_h_int hs_in_AX
-- L1 on g' = μ[Y|σ_AX]: ∫_s f·μ[Y|σ_AX] = ∫_s f · μ[μ[Y|σ_AX]|σ_AX] = ∫_s f · μ[Y|σ_AX]
-- so we use it the other direction; we need only h1 plus a `congr_ae` on s
-- to swap μ[h|σ_AX] → μ[Y|σ_AX] using the collapse.
have h_ae : (fun ω => S.stratumOddsRatio μ a ω * Uenv (a, S.X ω)
* (μ[fun ω' => HA.h (a, S.W ω', S.X ω')|S.σ_AX]) ω)
=ᵐ[μ.restrict s]
(fun ω => S.stratumOddsRatio μ a ω * Uenv (a, S.X ω)
* (μ[S.Y | S.σ_AX]) ω) := by
filter_upwards [hCollapse] with ω hω
simp [hω]
have h2 := integral_congr_ae h_ae
-- h1 : ∫_s f * h = ∫_s f * μ[h|σ_AX]
-- h2 : ∫_s f * μ[h|σ_AX] = ∫_s f * μ[Y|σ_AX]
exact h1.trans h2
have hL_collapse : (∫ ω in s,
S.stratumOddsRatio μ a ω * Lenv (a, S.X ω) * HA.h (a, S.W ω, S.X ω) ∂μ)
= ∫ ω in s,
S.stratumOddsRatio μ a ω * Lenv (a, S.X ω) * (μ[S.Y | S.σ_AX]) ω ∂μ := by
have h1 :=
setIntegral_mul_condExp_of_stronglyMeasurableLeft S.σ_AX_le hfL_sm
hh_int hfL_h_int hs_in_AX
have h_ae : (fun ω => S.stratumOddsRatio μ a ω * Lenv (a, S.X ω)
* (μ[fun ω' => HA.h (a, S.W ω', S.X ω')|S.σ_AX]) ω)
=ᵐ[μ.restrict s]
(fun ω => S.stratumOddsRatio μ a ω * Lenv (a, S.X ω)
* (μ[S.Y | S.σ_AX]) ω) := by
filter_upwards [hCollapse] with ω hω
simp [hω]
have h2 := integral_congr_ae h_ae
exact h1.trans h2
have hU_arm : (∫ ω in s', S.YofA a ω ∂μ)
-- … truncated; follow the source link for the rest …