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
γ_X :
Type u_1
γ_Z :
Type u_2
γ_W :
Type u_3
γ_U :
Type u_4
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
γ_X :
Type u_1
γ_Z :
Type u_2
γ_W :
Type u_3
γ_U :
Type u_4
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
γ_X :
Type u_1
γ_Z :
Type u_2
γ_W :
Type u_3
γ_U :
Type u_4
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 · 12 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
For a proximal potential-outcome system, the joint treatment-and-covariate map assigns to each unit its factual binary treatment and covariate.
Definition (Lean source)
parameters
γ_X :
Type u_1
γ_Z :
Type u_2
γ_W :
Type u_3
γ_U :
Type u_4
def
given by
fun ω => (S.A ω, S.X ω)
def σ_AX reviewed
⚑ flagged
Causalean.PO.POProximalSystem
For a proximal potential-outcome system, the σ-algebra generated by factual treatment and covariate is the pullback to the sample space of their product σ-algebra.
Definition (Lean source)
parameters
γ_X :
Type u_1
γ_Z :
Type u_2
γ_W :
Type u_3
γ_U :
Type u_4
def
given by
comap S.AX inferInstance
def σ_X reviewed
⚑ flagged
Causalean.PO.POProximalSystem
For a proximal potential-outcome system, the σ-algebra generated by the factual covariate is the pullback to the sample space of the covariate's σ-algebra.
Definition (Lean source)
parameters
γ_X :
Type u_1
γ_Z :
Type u_2
γ_W :
Type u_3
γ_U :
Type u_4
def
given by
comap S.X inferInstance
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
hypotheses
γ_X :
Type u_1
γ_Z :
Type u_2
γ_W :
Type u_3
γ_U :
Type u_4
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
For a proximal potential-outcome system, a measure on its sample space, and a treatment level, the marginal potential-outcome mean is the integral of the outcome that each unit would have under that treatment level with respect to that measure.
Definition (Lean source)
parameters
γ_X :
Type u_1
γ_Z :
Type u_2
γ_W :
Type u_3
γ_U :
Type u_4
μ :
Measure P.Ω
a :
def
meanYofA S μ a :
ℝ
given by
∫ ω, S.YofA a ω ∂μ
def condMeanYofA reviewed
⚑ flagged
Causalean.PO.POProximalSystem
For a proximal potential-outcome system, a measure on its sample space, and a treatment level, the opposite-arm conditional potential-outcome mean is the integral of that level's potential outcome over units whose factual treatment differs from that level, divided by the measure of that stratum.
Definition (Lean source)
parameters
γ_X :
Type u_1
γ_Z :
Type u_2
γ_W :
Type u_3
γ_U :
Type u_4
μ :
Measure P.Ω
a :
def
condMeanYofA S μ a :
ℝ
given by
(μ {ω | S.A ω ≠ a}).toReal⁻¹ * ∫ ω in {ω | S.A ω ≠ a}, S.YofA a ω ∂μ
def ATE reviewed
⚑ flagged
Causalean.PO.POProximalSystem
For a proximal potential-outcome system and a measure on its sample space, the average treatment effect is the marginal mean potential outcome under treatment one minus that under treatment zero.
Definition (Lean source)
parameters
γ_X :
Type u_1
γ_Z :
Type u_2
γ_W :
Type u_3
γ_U :
Type u_4
μ :
Measure P.Ω
def
ATE S μ :
ℝ
def stratumOddsRatio reviewed
⚑ flagged
Causalean.PO.POProximalSystem
For a proximal potential-outcome system, a measure on its sample space, and a treatment level, the stratum odds-ratio function assigns each unit the conditional expected indicator of the opposite treatment arm given its covariates divided by the conditional expected indicator of its own arm given those covariates.
Definition (Lean source)
parameters
γ_X :
Type u_1
γ_Z :
Type u_2
γ_W :
Type u_3
γ_U :
Type u_4
μ :
Measure P.Ω
a :
def
stratumOddsRatio S μ a :
P.Ω → ℝ
def IsUpperEnvW reviewed
⚑ flagged
Causalean.PO.POProximalSystem
For a proximal potential-outcome system, a measure on its sample space, a treatment level, and a proposed upper-envelope function of treatment and covariates, the upper W-proxy envelope condition holds exactly when the function is measurable [step:1] and, for every measurable nonnegative test function of the outcome-side proxy and covariates whose unweighted and envelope-weighted versions are integrable, its integral over the opposite treatment arm is at most its stratum-odds-ratio- and envelope-weighted integral over the specified treatment arm [step:2].
Definition (Lean source)
parameters
γ_X :
Type u_1
γ_Z :
Type u_2
γ_W :
Type u_3
γ_U :
Type u_4
μ :
Measure P.Ω
a :
Uenv :
Bool × γ_X → ℝ
def
IsUpperEnvW S μ a Uenv :
Prop
given by
clause 1
Measurable Uenv
clause 2
φ :
γ_W × γ_X → ℝ
(∀ 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
For a proximal potential-outcome system, a measure on its sample space, a treatment level, and a proposed lower-envelope function of treatment and covariates, the lower W-proxy envelope condition holds exactly when the function is measurable [step:1] and, for every measurable nonnegative test function of the outcome-side proxy and covariates whose unweighted and envelope-weighted versions are integrable, its stratum-odds-ratio- and envelope-weighted integral over the specified treatment arm is at most its integral over the opposite treatment arm [step:2].
Definition (Lean source)
parameters
γ_X :
Type u_1
γ_Z :
Type u_2
γ_W :
Type u_3
γ_U :
Type u_4
μ :
Measure P.Ω
a :
Lenv :
Bool × γ_X → ℝ
def
IsLowerEnvW S μ a Lenv :
Prop
given by
clause 1
Measurable Lenv
clause 2
φ :
γ_W × γ_X → ℝ
(∀ 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
For a proximal potential-outcome system, a measure on its sample space, a treatment level, and a proposed upper-envelope function of treatment and covariates, the upper Z-proxy envelope condition holds exactly when the function is measurable [step:1] and, for almost every unit in the specified treatment arm, the conditional mean of the factual outcome given treatment, treatment-side proxy, and covariates does not exceed the envelope evaluated at that treatment and covariate [step:2].
Definition (Lean source)
parameters
γ_X :
Type u_1
γ_Z :
Type u_2
γ_W :
Type u_3
γ_U :
Type u_4
μ :
Measure P.Ω
a :
Uenv :
Bool × γ_X → ℝ
def
IsUpperEnvZ S μ a Uenv :
Prop
given by
clause 1
Measurable Uenv
clause 2
∀ᵐ ω ∂(μ.restrict {ω | S.A ω = a}), (μ[S.Y | S.σ_AZX]) ω ≤ Uenv (a, S.X ω)
def IsLowerEnvZ reviewed
⚑ flagged
Causalean.PO.POProximalSystem
For a proximal potential-outcome system, a measure on its sample space, a treatment level, and a proposed lower-envelope function of treatment and covariates, the lower Z-proxy envelope condition holds exactly when the function is measurable [step:1] and, for almost every unit in the specified treatment arm, the envelope evaluated at that treatment and covariate does not exceed the conditional mean of the factual outcome given treatment, treatment-side proxy, and covariates [step:2].
Definition (Lean source)
parameters
γ_X :
Type u_1
γ_Z :
Type u_2
γ_W :
Type u_3
γ_U :
Type u_4
μ :
Measure P.Ω
a :
Lenv :
Bool × γ_X → ℝ
def
IsLowerEnvZ S μ a Lenv :
Prop
given by
clause 1
Measurable Lenv
clause 2
∀ᵐ ω ∂(μ.restrict {ω | S.A ω = a}), Lenv (a, S.X ω) ≤ (μ[S.Y | S.σ_AZX]) ω
def IsUpperEnvWZ reviewed
⚑ flagged
Causalean.PO.POProximalSystem
For a proximal potential-outcome system, a measure on its sample space, a treatment level, and a proposed upper-envelope function of treatment and covariates, the upper joint W--Z envelope condition holds exactly when the function is measurable [step:1] and, for every pair of measurable nonnegative test functions of respectively the outcome-side and treatment-side proxies with all three displayed products integrable, the conditional expectation of their product given treatment and covariates is at most the envelope times the product of their conditional expectations, almost everywhere in the specified treatment arm [step:2].
Definition (Lean source)
parameters
γ_X :
Type u_1
γ_Z :
Type u_2
γ_W :
Type u_3
γ_U :
Type u_4
μ :
Measure P.Ω
a :
Uenv :
Bool × γ_X → ℝ
def
IsUpperEnvWZ S μ a Uenv :
Prop
given by
clause 1
Measurable Uenv
clause 2
φ_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
For a proximal potential-outcome system, a measure on its sample space, a treatment level, and a proposed lower-envelope function of treatment and covariates, the lower joint W--Z envelope condition holds exactly when the function is measurable [step:1] and, for every pair of measurable nonnegative test functions of respectively the outcome-side and treatment-side proxies with all three displayed products integrable, the envelope times the product of their conditional expectations given treatment and covariates is at most the conditional expectation of their product, almost everywhere in the specified treatment arm [step:2].
Definition (Lean source)
parameters
γ_X :
Type u_1
γ_Z :
Type u_2
γ_W :
Type u_3
γ_U :
Type u_4
μ :
Measure P.Ω
a :
Lenv :
Bool × γ_X → ℝ
def
IsLowerEnvWZ S μ a Lenv :
Prop
given by
clause 1
Measurable Lenv
clause 2
φ_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])
12 supporting declarations (lemmas, instances)
-
measurable_AXlemma — The treatment-covariate tuple map is measurable.hypothesesγ_X :sharedType u_1γ_Z :sharedType u_2γ_W :sharedType u_3γ_U :sharedType u_4conclusionMeasurable S.AXProof (Lean source)
@[fun_prop] 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.hypothesesγ_X :sharedType u_1γ_Z :sharedType u_2γ_W :sharedType u_3γ_U :sharedType u_4conclusionS.σ_AX ≤ (inferInstance : MeasurableSpace P.Ω)Proof (Lean source)
lemma σ_AX_le : S.σ_AX ≤ (inferInstance : MeasurableSpace P.Ω) := S.measurable_AX.comap_le -
measurable_X_σ_Xlemma — The covariate is measurable with respect to the σ-algebra it generates.hypothesesγ_X :sharedType u_1γ_Z :sharedType u_2γ_W :sharedType u_3γ_U :sharedType u_4conclusionMeasurable[S.σ_X] S.XProof (Lean source)
@[fun_prop] lemma measurable_X_σ_X : Measurable[S.σ_X] S.X := fun _ ht => ⟨_, ht, rfl⟩ -
measurable_A_σ_AXlemma — The treatment is measurable with respect to the σ-algebra generated by treatment and covariate, being the first coordinate of that tuple.hypothesesγ_X :sharedType u_1γ_Z :sharedType u_2γ_W :sharedType u_3γ_U :sharedType u_4conclusionMeasurable[S.σ_AX] S.AProof (Lean source)
@[fun_prop] lemma measurable_A_σ_AX : Measurable[S.σ_AX] S.A := by intro t ht refine ⟨Prod.fst ⁻¹' t, measurable_fst ht, ?_⟩ ext ω; rfl -
measurable_X_σ_AXlemma — The covariate is measurable with respect to the σ-algebra generated by treatment and covariate, being the second coordinate of that tuple.hypothesesγ_X :sharedType u_1γ_Z :sharedType u_2γ_W :sharedType u_3γ_U :sharedType u_4conclusionMeasurable[S.σ_AX] S.XProof (Lean source)
@[fun_prop] lemma measurable_X_σ_AX : Measurable[S.σ_AX] S.X := by intro t ht refine ⟨Prod.snd ⁻¹' t, measurable_snd ht, ?_⟩ ext ω; rfl -
σ_X_le_σ_AXlemma — σ_X is coarser than σ_AX: X factors through (A, X) via the second projection.hypothesesγ_X :sharedType u_1γ_Z :sharedType u_2γ_W :sharedType u_3γ_U :sharedType u_4conclusionS.σ_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.hypothesesγ_X :sharedType u_1γ_Z :sharedType u_2γ_W :sharedType u_3γ_U :sharedType u_4conclusionS.σ_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).hypothesesγ_X :sharedType u_1γ_Z :sharedType u_2γ_W :sharedType u_3γ_U :sharedType u_4conclusionS.σ_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.hypothesesγ_X :sharedType u_1γ_Z :sharedType u_2γ_W :sharedType u_3γ_U :sharedType u_4conclusionS.σ_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).hypothesesγ_X :sharedType u_1γ_Z :sharedType u_2γ_W :sharedType u_3γ_U :sharedType u_4conclusionS.σ_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.hypothesesγ_X :sharedType u_1γ_Z :sharedType u_2γ_W :sharedType u_3γ_U :sharedType u_4conclusionS.σ_X ≤ S.σ_AUXProof (Lean source)
lemma σ_X_le_σ_AUX : S.σ_X ≤ S.σ_AUX := le_trans S.σ_X_le_σ_AX S.σ_AX_le_σ_AUX -
condMeanYofA_eqlemma — The conditional potential outcome mean of an arm on the opposite-arm stratum is the integral of that arm's potential outcome over the stratum where treatment differs from the arm, divided by the mass of that stratum.hypothesesγ_X :sharedType u_1γ_Z :sharedType u_2γ_W :sharedType u_3γ_U :sharedType u_4μ :Measure P.Ωa :conclusionS.condMeanYofA μ a = (μ {ω | S.A ω ≠ a}).toReal⁻¹ * ∫ ω in {ω | S.A ω ≠ a}, S.YofA a ω ∂μProof (Lean source)
@[causal_defs_simps] lemma condMeanYofA_eq (μ : Measure P.Ω) (a : Bool) : S.condMeanYofA μ a = (μ {ω | S.A ω ≠ a}).toReal⁻¹ * ∫ ω in {ω | S.A ω ≠ a}, S.YofA a ω ∂μ := rfl
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
γ_X :
Type u_1
γ_Z :
Type u_2
γ_W :
Type u_3
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
γ_X :
Type u_1
γ_Z :
Type u_2
γ_W :
Type u_3
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
γ_X :
Type u_1
γ_Z :
Type u_2
γ_W :
Type u_3
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
γ_X :
Type u_1
γ_Z :
Type u_2
γ_W :
Type u_3
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
γ_X :
Type u_1
γ_Z :
Type u_2
γ_W :
Type u_3
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
γ_X :
Type u_1
γ_Z :
Type u_2
γ_W :
Type u_3
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]) ω) μ
conclusion
conclusion 1
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
γ_X :
Type u_1
γ_Z :
Type u_2
γ_W :
Type u_3
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
conclusion 1
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
γ_X :
Type u_1
γ_Z :
Type u_2
γ_W :
Type u_3
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
conclusion 1
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 …