PO.ID.Partial.Proxy
Partial identification with proxy variables: sensitivity of bounds to proxy quality.
Helpers 6 core · 6 supporting · 4 submodules The identities that move an unobservable off-arm counterfactual integral onto observable quantities in the proximal bounds. 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 for abstract proximal envelope bounds inspired by Ghassami, Zhang, Shpitser, and Tchetgen Tchetgen (arXiv:2304.04374v4, 2026): * WBasedAssumptions — outcome-confounding-proxy envelope bo
Proximal partial-identification assumption bundles
Three weakened assumption bundles for abstract proximal envelope bounds inspired by Ghassami, Zhang, Shpitser, and Tchetgen Tchetgen (arXiv:2304.04374v4, 2026):
* WBasedAssumptions — outcome-confounding-proxy envelope bounds.
* ZBasedAssumptions — treatment-confounding-proxy envelope bounds.
* TwoProxyAssumptions — two conditionally independent invalid proxies
with joint envelope bounds.
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. The code uses a propensity-odds convention:
E[q(Z,a,X) | A,U,X] = p(A ≠ a | U,X) / p(A = a | U,X) on the arm {A=a}.
The user supplies this ratio as likelihoodRatio_swapA through an operational
conditional-expectation identity. The paper's latent-density-ratio convention
differs by the covariate-level stratumOddsRatio; no Radon–Nikodym conversion
theorem is formalized here.
structure WBasedAssumptions reviewed
⚑ flagged
Causalean.PO.POProximalSystem
Assumption bundle for the abstract W-proxy envelope bounds, inspired by Ghassami, Zhang, Shpitser, and Tchetgen Tchetgen (arXiv:2304.04374v4, 2026).
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 abstract Z-proxy envelope bounds. It 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
in the Z-envelope chain. 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: 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 abstract two-proxy envelope bound. 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
proximal bound family. They directly assume the operational integral or
conditional-expectation inequalities consumed by the downstream proofs;
no density-ratio extremum or sharpness result is formalized here.
No assumption bundles live here — see Assumptions.lean.
def AX reviewed
⚑ flagged
Causalean.PO.POProximalSystem
The joint treatment-and-covariate map of a proximal potential-outcome system assigns 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
The σ-algebra generated by factual treatment and the covariate in a proximal potential-outcome system is the pullback of their product σ-algebra to the sample space.
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
The σ-algebra generated by the factual covariate in a proximal potential-outcome system is the pullback of the covariate's σ-algebra to the sample space.
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
The marginal potential-outcome mean for a proximal potential-outcome system, a population measure, and a treatment arm averages the outcome each unit would have under that arm.
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
The opposite-arm conditional potential-outcome mean for a proximal potential-outcome system, a population measure, and a treatment arm averages that arm's potential outcome among units whose factual treatment differs from it.
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
The average treatment effect for a proximal potential-outcome system under a population measure 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
The stratum odds-ratio function for a proximal potential-outcome system, a population measure, and a treatment arm divides the conditional probability of the opposite arm by that of the specified arm at each covariate value.
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
The upper operational W-proxy envelope condition for a proximal system, a population measure, a treatment arm, and an envelope depending on treatment and covariates requires the envelope to be measurable and every admissible nonnegative proxy test function to satisfy the stated opposite-arm versus weighted on-arm integral inequality.
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
The lower operational W-proxy envelope condition for a proximal system, a population measure, a treatment arm, and an envelope depending on treatment and covariates requires the envelope to be measurable and every admissible nonnegative proxy test function to satisfy the stated weighted on-arm versus opposite-arm integral inequality.
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
The upper Z-proxy conditional-mean envelope condition for a proximal system, a population measure, a treatment arm, and an envelope depending on treatment and covariates requires the envelope to be measurable and the conditional outcome mean given treatment, the treatment-side proxy, and covariates to lie below it almost everywhere in that arm.
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
The lower Z-proxy conditional-mean envelope condition for a proximal system, a population measure, a treatment arm, and an envelope depending on treatment and covariates requires the envelope to be measurable and the conditional outcome mean given treatment, the treatment-side proxy, and covariates to lie above it almost everywhere in that arm.
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
The upper operational joint-proxy envelope condition for a proximal system, a population measure, a treatment arm, and an envelope depending on treatment and covariates requires the envelope to be measurable and every admissible pair of nonnegative proxy test functions to satisfy the stated conditional product inequality almost everywhere in that arm.
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
The lower operational joint-proxy envelope condition for a proximal system, a population measure, a treatment arm, and an envelope depending on treatment and covariates requires the envelope to be measurable and every admissible pair of nonnegative proxy test functions to satisfy the reverse conditional product inequality almost everywhere in that arm.
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 3 core · 2 supporting This file converts the scalar two-sided proximal proxy bounds into Set.Icc membership statements. ★ condMeanYofA_W_mem_Icc★ condMeanYofA_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
Closed-interval form of the conditional W-envelope bound. The opposite-arm conditional counterfactual mean belongs to the interval spanned by chosen outcome-bound witnesses and operational W-envelope clamps. This restates the scalar sandwich under the W-only bridge assumptions, distinct treatment and outcome variables, a treatment arm and lower and upper envelope functions, the two operational envelope comparisons, positive opposite-arm mass, and integrable envelope-weighted bridge moments.
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 condMeanYofA_Z_mem_Icc reviewed
⚑ flagged
Causalean.PO.POProximalSystem
Closed-interval form of the conditional Z-envelope bound. The opposite-arm conditional counterfactual mean belongs to the interval spanned by normalized integrals of lower and upper outcome envelopes. This restates the scalar sandwich under the Z-only bridge assumptions, distinct treatment and outcome variables, a treatment arm and lower and upper envelope functions, the two on-arm conditional-mean envelope comparisons, integrable envelopes, integrability after weighting by the treatment bridge, integrability after weighting by the arm-swap factor, and positive opposite-arm mass.
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 condMeanYofA_WZ_mem_Icc reviewed
⚑ flagged
Causalean.PO.POProximalSystem
Closed-interval form of the two-proxy envelope bound. The opposite-arm conditional counterfactual mean belongs to the interval spanned by chosen outcome-bound witnesses and operational joint-proxy envelope clamps. This restates the scalar sandwich under the two-proxy bridge assumptions, distinct treatment and outcome variables, a treatment arm and lower and upper envelope functions, the two operational joint-proxy comparisons, positive opposite-arm mass, and integrability of both envelope-weighted conditional bridge products.
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
2 supporting declarations (lemmas, instances)
-
meanYofA_W_mem_Icctheorem — Closed-interval form of the marginal W-envelope bound. The marginal counterfactual mean belongs to the interval spanned by the lower and upper operational W-envelope clamps. This restates the scalar sandwich under the W-only bridge assumptions, distinct treatment and outcome variables, a treatment arm and lower and upper envelope functions, the two operational envelope comparisons, integrable envelope-weighted bridge moments, and integrable envelope-weighted observed conditional means.hypothesesγ_X :sharedType u_1γ_Z :sharedType u_2γ_W :sharedType u_3HA :POProximalSystem.WBasedAssumptions S μa :hAY :S.Avar.v ≠ S.Yvar.vLenv Uenv :Bool × γ_X → ℝhL :S.IsLowerEnvW μ a LenvhU :S.IsUpperEnvW μ a UenvhU_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]) ω) μconclusionS.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 -
meanYofA_Z_mem_Icctheorem — Closed-interval form of the marginal Z-envelope bound. The marginal counterfactual mean belongs to the interval spanned by lower and upper Z-proxy envelope integrals. This restates the scalar sandwich under the Z-only bridge assumptions, distinct treatment and outcome variables, a treatment arm and lower and upper envelope functions, the two on-arm conditional-mean envelope comparisons, integrable envelopes, integrability after weighting by the treatment bridge, and integrability after weighting by the arm-swap factor.hypothesesγ_X :sharedType u_1γ_Z :sharedType u_2γ_W :sharedType u_3HA :POProximalSystem.ZBasedAssumptions S μa :hAY :S.Avar.v ≠ S.Yvar.vLenv Uenv :Bool × γ_X → ℝhL :S.IsLowerEnvZ μ a LenvhU :S.IsUpperEnvZ μ a UenvhLInt :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 ω) μconclusionS.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
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, an abstract envelope 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
Abstract two-proxy envelope consequence. The conditional counterfactual mean among units in the opposite treatment arm lies between chosen outcome-bound witnesses and operational joint-proxy envelope bounds expressed through observable quantities. The result uses the two-proxy bridge assumptions, distinct treatment and outcome variables, a treatment arm and lower and upper envelope functions, the lower and upper operational joint-proxy comparisons, positive mass for the opposite arm, and integrability of the two envelope-weighted products of conditional bridge means.
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
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
-- 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,
Lenv (a, S.X ω)
* (μ[fun ω' => φW (S.W ω', S.X ω') | S.σ_AX]) ω
* (μ[fun ω' => φZ (S.Z ω', S.X ω') | S.σ_AX]) ω ∂μ
-- … truncated; follow the source link for the rest …
WBased 2 core · 0 supporting This file proves abstract W-only proximal envelope consequences 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 abstract W-only proximal envelope consequences 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 operational W-envelope
predicates IsLowerEnvW and IsUpperEnvW turn that moment into observable
integrals over the on-arm stratum.
Main declarations:
* condMeanYofA_W_bounds is the conditional envelope sandwich for
condMeanYofA, combining envelope bounds with chosen essential-bound
witnesses for Y.
* meanYofA_W_bounds is the marginal sandwich for meanYofA,
obtained by adding the consistency-identified {A = a} contribution.
theorem condMeanYofA_W_bounds reviewed
⚑ flagged
Causalean.PO.POProximalSystem
Abstract W-envelope consequence. The conditional counterfactual mean among units in the opposite treatment arm lies between a chosen outcome-bound witness and an operational W-envelope bound on each side. The result uses the W-only bridge assumptions, distinct treatment and outcome variables, a treatment arm and lower and upper envelope functions, the two operational envelope comparisons, positive mass for the opposite arm, and integrability of the two envelope-weighted bridge moments.
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: use the bundled pointwise nonnegativity of the bridge.
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
-- σ_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: clamp by the chosen a.e. upper-bound witness.
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
-- ============================================================
-- ASSEMBLE
-- ============================================================
refine ⟨?_, ?_⟩
· -- max (chosen lower bound) (envelope lower) ≤ condMeanYofA
exact max_le hL_triv hL_cond
-- … truncated; follow the source link for the rest …
theorem meanYofA_W_bounds reviewed
⚑ flagged
Causalean.PO.POProximalSystem
Marginal abstract W-envelope consequence. The marginal counterfactual mean lies between a chosen outcome-bound clamp and an operational W-envelope clamp on each side, after adding the identified contribution from the observed arm. The result uses the W-only bridge assumptions, distinct treatment and outcome variables, a treatment arm and lower and upper envelope functions, the two operational envelope comparisons, integrability of the envelope-weighted bridge moments, and integrability of the envelope-weighted observed conditional means.
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
-- Use the bundle's assumed pointwise nonnegativity of the bridge.
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
-- σ_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
-- … truncated; follow the source link for the rest …