PO.ID.Partial.Manski
Manski worst-case and monotonicity-based bounds on treatment effects under bounded outcomes.
Setup 18 core · 5 supporting This file defines the data layer for Manski bounds with a discrete instrument, a binary treatment, and a real-valued outcome. ★ POManskiIVSystem★ measurable_YofD
Manski IV Setup
This file defines the data layer for Manski bounds with a discrete instrument, a binary treatment, and a real-valued outcome. It provides the potential outcomes, factual variables, instrument support, target average treatment effect, and the four observable bound functionals used by the Manski identification arguments.
Assumption bundles are kept in the companion assumptions file.
structure POManskiIVSystem reviewed
⚑ flagged
Causalean.PO
The Manski IV data layer records a discrete instrument, a binary treatment, and a real outcome inside a potential-outcome system.
Definition (Lean source)
parameters
P :
α :
fields
Z :
P.V
D :
P.V
Y :
P.V
hZ :
P.X Z ≃ᵐ α
hDbool :
P.X D ≃ᵐ Bool
hYreal :
P.X Y ≃ᵐ ℝ
hZD :
Z ≠ D
hZY :
Z ≠ Y
hDY :
D ≠ Y
def zVar reviewed
⚑ flagged
Causalean.PO.POManskiIVSystem
Instrument packaged as a POVar valued in α.
Definition (Lean source)
def zVar : POVar P α := ⟨S.Z, S.hZ⟩
def dVar reviewed
⚑ flagged
Causalean.PO.POManskiIVSystem
Treatment packaged as a POVar valued in Bool.
def yVar reviewed
⚑ flagged
Causalean.PO.POManskiIVSystem
Outcome packaged as a POVar valued in ℝ.
Definition (Lean source)
def yVar : POVar P ℝ := ⟨S.Y, S.hYreal⟩
def YofD reviewed
⚑ flagged
Causalean.PO.POManskiIVSystem
Counterfactual outcome under treatment arm d.
Definition (Lean source)
noncomputable def YofD (d : Bool) : P.Ω → ℝ := S.yVar.cfUnder S.dVar d
def factualZ reviewed
⚑ flagged
Causalean.PO.POManskiIVSystem
Factual instrument.
Definition (Lean source)
noncomputable def factualZ : P.Ω → α := S.zVar.factual
def factualD reviewed
⚑ flagged
Causalean.PO.POManskiIVSystem
Factual treatment.
Definition (Lean source)
noncomputable def factualD : P.Ω → Bool := S.dVar.factual
def factualY reviewed
⚑ flagged
Causalean.PO.POManskiIVSystem
Factual outcome.
Definition (Lean source)
noncomputable def factualY : P.Ω → ℝ := S.yVar.factual
def zEvent reviewed
⚑ flagged
Causalean.PO.POManskiIVSystem
The event {Z = z}.
Definition (Lean source)
def zEvent (z : α) : Set P.Ω := S.zVar.event z
def dEvent reviewed
⚑ flagged
Causalean.PO.POManskiIVSystem
The event {D = d}.
lemma measurable_YofD reviewed
⚑ flagged
Causalean.PO.POManskiIVSystem
For a fixed treatment arm d, the counterfactual outcome Y(d) is measurable.
Formal statement
Proof (Lean source)
lemma measurable_YofD (d : Bool) : Measurable (S.YofD d) :=
S.yVar.measurable_cfUnder S.dVar d
def ATE reviewed
⚑ flagged
Causalean.PO.POManskiIVSystem
Average treatment effect E[Y(1) - Y(0)].
def support reviewed
⚑ flagged
Causalean.PO.POManskiIVSystem
Support of the instrument: {z | μ(Z = z) ≠ 0}.
Definition (Lean source)
def support : Set α := {z | P.μ (S.zEvent z) ≠ 0}
def boundArm reviewed
⚑ flagged
Causalean.PO.POManskiIVSystem
The unified arm-bound functional averages the observed outcome on arm d and the supplied outcome floor or ceiling on the opposite arm within instrument stratum z.
Definition (Lean source)
noncomputable def boundArm (d : Bool) (c : ℝ) (z : α) : ℝ :=
eventCondExp P.μ (S.zEvent z)
(fun ω => S.factualY ω * S.dVar.indicator d ω
+ c * S.dVar.indicator (!d) ω)
def lowerBound1 reviewed
⚑ flagged
Causalean.PO.POManskiIVSystem
The lower observable bound for the treated potential-outcome mean in instrument stratum z uses the outcome floor on untreated units.
Definition (Lean source)
noncomputable def lowerBound1 (lo : ℝ) (z : α) : ℝ := S.boundArm true lo z
def upperBound1 reviewed
⚑ flagged
Causalean.PO.POManskiIVSystem
The upper observable bound for the treated potential-outcome mean in instrument stratum z uses the outcome ceiling on untreated units.
Definition (Lean source)
noncomputable def upperBound1 (hi : ℝ) (z : α) : ℝ := S.boundArm true hi z
def lowerBound0 reviewed
⚑ flagged
Causalean.PO.POManskiIVSystem
The lower observable bound for the control potential-outcome mean in instrument stratum z uses the outcome floor on treated units.
Definition (Lean source)
noncomputable def lowerBound0 (lo : ℝ) (z : α) : ℝ := S.boundArm false lo z
def upperBound0 reviewed
⚑ flagged
Causalean.PO.POManskiIVSystem
The upper observable bound for the control potential-outcome mean in instrument stratum z uses the outcome ceiling on treated units.
Definition (Lean source)
noncomputable def upperBound0 (hi : ℝ) (z : α) : ℝ := S.boundArm false hi z
5 supporting declarations (lemmas, instances)
-
measurable_factualZlemma — Factual instrument is measurable.conclusionMeasurable S.factualZProof (Lean source)
lemma measurable_factualZ : Measurable S.factualZ := S.zVar.measurable_factual -
measurable_factualDlemma — Factual treatment is measurable.conclusionMeasurable S.factualDProof (Lean source)
lemma measurable_factualD : Measurable S.factualD := S.dVar.measurable_factual -
measurable_factualYlemma — Factual outcome is measurable.conclusionMeasurable S.factualYProof (Lean source)
lemma measurable_factualY : Measurable S.factualY := S.yVar.measurable_factual -
measurableSet_zEventlemma — Each instrument stratum event is measurable.Proof (Lean source)
lemma measurableSet_zEvent (z : α) : MeasurableSet (S.zEvent z) := S.zVar.measurableSet_event _ (measurableSet_singleton _) -
measurableSet_dEventlemma — Each treatment arm event is measurable.Proof (Lean source)
lemma measurableSet_dEvent (d : Bool) : MeasurableSet (S.dEvent d) := S.dVar.measurableSet_event _ (measurableSet_singleton _)
Assumptions 6 core · 2 supporting This file states the assumption bundles for Manski bounds with a discrete instrument. ★ bounded
Manski Assumptions
This file states the assumption bundles for Manski bounds with a discrete instrument. The baseline assumptions impose consistency, bounded potential outcomes, and integrability, while separate shape restrictions encode mean independence, monotone treatment response, monotone treatment selection, and monotone instrumental variables.
The assumptions are separated from the data layer so later bound theorems can combine them independently.
structure BaseAssumptions reviewed
⚑ flagged
Causalean.PO.POManskiIVSystem
Discrete-IV ATE-bound baseline assumptions -- common part of def:po-iv-manski-assumptions.
Definition (Lean source)
parameters
S :
POManskiIVSystem P α
fields
consistency :
P.Consistency
lo :
ℝ
hi :
ℝ
hle :
lo ≤ hi
integrable_Y1 :
Integrable (S.YofD true) P.μ
integrable_Y0 :
Integrable (S.YofD false) P.μ
lemma bounded reviewed
⚑ flagged
Causalean.PO.POManskiIVSystem.BaseAssumptions
Given the baseline Manski assumptions bundle, which fixes bounds lo ≤ hi and asserts that both potential outcomes Y(1) and Y(0) lie a.s. in [lo, hi], the potential outcome Y(d) lies almost surely between lo and hi, uniformly for either treatment arm d — the binary-folded form of the two separate range assumptions.
Formal statement
hypotheses
hA :
S.BaseAssumptions
d :
conclusion
∀ᵐ ω ∂P.μ, hA.lo ≤ S.YofD d ω ∧ S.YofD d ω ≤ hA.hi
structure MeanIndep reviewed
⚑ flagged
Causalean.PO.POManskiIVSystem
Mean independence of the potential outcomes from the instrument. Stated directly on eventCondExp — matches def:po-iv-manski-assumptions letter-for-letter and avoids the stronger joint independence used in LATE.
Definition (Lean source)
structure MTR reviewed
⚑ flagged
Causalean.PO.POManskiIVSystem
Monotone treatment response -- prop:po-iv-mtr, item 1. Y(0) ≤ Y(1) almost surely.
Definition (Lean source)
structure MTS reviewed
⚑ flagged
Causalean.PO.POManskiIVSystem
Monotone treatment selection -- prop:po-iv-mts.
Definition (Lean source)
structure MIV reviewed
⚑ flagged
Causalean.PO.POManskiIVSystem
Monotone instrumental variable -- prop:po-iv-miv.
Definition (Lean source)
parameters
S :
POManskiIVSystem P α
fields
inst :
monotone :
∀ (d : Bool) (z z' : α)
if
z ∈ S.support
and
z' ∈ S.support
and
@le α inst.toLE z z'
then
eventCondExp P.μ (S.zEvent z) (S.YofD d) ≤ eventCondExp P.μ (S.zEvent z') (S.YofD d)
2 supporting declarations (lemmas, instances)
-
integrable_YofDlemma — Binary-folded form of integrable_Y1 / integrable_Y0.Proof (Lean source)
lemma integrable_YofD (hA : S.BaseAssumptions) (d : Bool) : Integrable (S.YofD d) P.μ := by cases d · exact hA.integrable_Y0 · exact hA.integrable_Y1 -
integrable_factualYlemma — The factual outcome Y is integrable. Derived from arm integrability via consistency (factualY = Σ_d Y(d)·1{D=d} a.e.), so it need not be assumed separately.Proof (Lean source)
lemma integrable_factualY (hA : S.BaseAssumptions) : Integrable S.factualY P.μ := by have hY1_ind : Integrable (fun ω => S.YofD true ω * S.dVar.indicator true ω) P.μ := S.dVar.integrable_mul_indicator true (measurableSet_singleton true) hA.integrable_Y1 have hY0_ind : Integrable (fun ω => S.YofD false ω * S.dVar.indicator false ω) P.μ := S.dVar.integrable_mul_indicator false (measurableSet_singleton false) hA.integrable_Y0 refine (hY1_ind.add hY0_ind).congr ?_ filter_upwards with ω have htrue := congr_fun (POVar.factual_mul_indicator_eq_cfUnder_mul_indicator_fn hA.consistency S.yVar S.dVar true (Ne.symm S.hDY)) ω have hfalse := congr_fun (POVar.factual_mul_indicator_eq_cfUnder_mul_indicator_fn hA.consistency S.yVar S.dVar false (Ne.symm S.hDY)) ω have htrue' : S.YofD true ω * S.dVar.indicator true ω = S.factualY ω * S.dVar.indicator true ω := by simpa [POManskiIVSystem.YofD, POManskiIVSystem.factualY] using htrue.symm have hfalse' : S.YofD false ω * S.dVar.indicator false ω = S.factualY ω * S.dVar.indicator false ω := by simpa [POManskiIVSystem.YofD, POManskiIVSystem.factualY] using hfalse.symm have hsum := S.dVar.indicator_add_indicator_not ω calc S.YofD true ω * S.dVar.indicator true ω + S.YofD false ω * S.dVar.indicator false ω = S.factualY ω * S.dVar.indicator true ω + S.factualY ω * S.dVar.indicator false ω := by rw [htrue', hfalse'] _ = S.factualY ω * (S.dVar.indicator true ω + S.dVar.indicator false ω) := by ring _ = S.factualY ω := by rw [hsum, mul_one]
MIV 5 core · 8 supporting This file proves envelope bounds for treatment-arm conditional means under the monotone instrumental variable assumption. ★ miv_bounds_ATE
Manski bounds under monotone instrumental variables
This file proves envelope bounds for treatment-arm conditional means under the monotone instrumental variable assumption. The stratum-level Manski bounds are combined with monotonicity in the instrument and then integrated to obtain the corresponding ATE bounds.
It defines the lower and upper monotone-instrument envelopes mLower1,
mUpper1, mLower0, and mUpper0, proves their conditional and integrated
arm-wise bounds, and concludes with miv_bounds_ATE.
def mLower1 reviewed
⚑ flagged
Causalean.PO.POManskiIVSystem
Lower envelope for arm d = 1: sSup { L_{1,u} | u ∈ supp, u ≤ z }.
Definition (Lean source)
noncomputable def mLower1 (hA : S.BaseAssumptions) [LinearOrder α] (z : α) : ℝ :=
sSup {val : ℝ | ∃ u ∈ S.support, u ≤ z ∧ val = S.lowerBound1 hA.lo u}
def mUpper1 reviewed
⚑ flagged
Causalean.PO.POManskiIVSystem
Upper envelope for arm d = 1: sInf { U_{1,u} | u ∈ supp, z ≤ u }.
Definition (Lean source)
noncomputable def mUpper1 (hA : S.BaseAssumptions) [LinearOrder α] (z : α) : ℝ :=
sInf {val : ℝ | ∃ u ∈ S.support, z ≤ u ∧ val = S.upperBound1 hA.hi u}
def mLower0 reviewed
⚑ flagged
Causalean.PO.POManskiIVSystem
Lower envelope for arm d = 0: sSup { L_{0,u} | u ∈ supp, u ≤ z }.
Definition (Lean source)
noncomputable def mLower0 (hA : S.BaseAssumptions) [LinearOrder α] (z : α) : ℝ :=
sSup {val : ℝ | ∃ u ∈ S.support, u ≤ z ∧ val = S.lowerBound0 hA.lo u}
def mUpper0 reviewed
⚑ flagged
Causalean.PO.POManskiIVSystem
Upper envelope for arm d = 0: sInf { U_{0,u} | u ∈ supp, z ≤ u }.
Definition (Lean source)
noncomputable def mUpper0 (hA : S.BaseAssumptions) [LinearOrder α] (z : α) : ℝ :=
sInf {val : ℝ | ∃ u ∈ S.support, z ≤ u ∧ val = S.upperBound0 hA.hi u}
theorem miv_bounds_ATE reviewed
⚑ flagged
Causalean.PO.POManskiIVSystem
MIV ATE envelope bounds (prop:po-iv-miv, integrated form). Under the baseline Manski assumptions and a monotone instrumental variable — the conditional mean of each potential outcome is nondecreasing in the instrument value across its support, the average treatment effect is sandwiched between the integrated lower-envelope contrast ∫ (mLower1(Z) − mUpper0(Z)) and the integrated upper-envelope contrast ∫ (mUpper1(Z) − mLower0(Z)).
Formal statement
Proof (Lean source)
theorem miv_bounds_ATE [IsFiniteMeasure P.μ] [Fintype α]
(hA : S.BaseAssumptions) (hMIV : S.MIV) :
letI := hMIV.inst
(∫ ω, S.mLower1 hA (S.factualZ ω) - S.mUpper0 hA (S.factualZ ω) ∂P.μ)
≤ S.ATE
∧ S.ATE ≤
(∫ ω, S.mUpper1 hA (S.factualZ ω) - S.mLower0 hA (S.factualZ ω) ∂P.μ) := by
letI := hMIV.inst
-- Integrability of the envelope composites (bounded on a Fintype support).
have hmeas_mL1 : Measurable (S.mLower1 hA) := measurable_of_finite _
have hmeas_mU1 : Measurable (S.mUpper1 hA) := measurable_of_finite _
have hmeas_mL0 : Measurable (S.mLower0 hA) := measurable_of_finite _
have hmeas_mU0 : Measurable (S.mUpper0 hA) := measurable_of_finite _
have hint_mL1 : Integrable (fun ω => S.mLower1 hA (S.factualZ ω)) P.μ := by
refine MeasureTheory.Integrable.of_bound
(hmeas_mL1.comp S.measurable_factualZ).aestronglyMeasurable
(∑ z : α, |S.mLower1 hA z|) (Filter.Eventually.of_forall (fun ω => ?_))
have : |S.mLower1 hA (S.factualZ ω)| ≤ ∑ z : α, |S.mLower1 hA z| :=
Finset.single_le_sum (f := fun z => |S.mLower1 hA z|)
(fun _ _ => abs_nonneg _) (Finset.mem_univ _)
simpa using this
have hint_mU1 : Integrable (fun ω => S.mUpper1 hA (S.factualZ ω)) P.μ := by
refine MeasureTheory.Integrable.of_bound
(hmeas_mU1.comp S.measurable_factualZ).aestronglyMeasurable
(∑ z : α, |S.mUpper1 hA z|) (Filter.Eventually.of_forall (fun ω => ?_))
have : |S.mUpper1 hA (S.factualZ ω)| ≤ ∑ z : α, |S.mUpper1 hA z| :=
Finset.single_le_sum (f := fun z => |S.mUpper1 hA z|)
(fun _ _ => abs_nonneg _) (Finset.mem_univ _)
simpa using this
have hint_mL0 : Integrable (fun ω => S.mLower0 hA (S.factualZ ω)) P.μ := by
refine MeasureTheory.Integrable.of_bound
(hmeas_mL0.comp S.measurable_factualZ).aestronglyMeasurable
(∑ z : α, |S.mLower0 hA z|) (Filter.Eventually.of_forall (fun ω => ?_))
have : |S.mLower0 hA (S.factualZ ω)| ≤ ∑ z : α, |S.mLower0 hA z| :=
Finset.single_le_sum (f := fun z => |S.mLower0 hA z|)
(fun _ _ => abs_nonneg _) (Finset.mem_univ _)
simpa using this
have hint_mU0 : Integrable (fun ω => S.mUpper0 hA (S.factualZ ω)) P.μ := by
refine MeasureTheory.Integrable.of_bound
(hmeas_mU0.comp S.measurable_factualZ).aestronglyMeasurable
(∑ z : α, |S.mUpper0 hA z|) (Filter.Eventually.of_forall (fun ω => ?_))
have : |S.mUpper0 hA (S.factualZ ω)| ≤ ∑ z : α, |S.mUpper0 hA z| :=
Finset.single_le_sum (f := fun z => |S.mUpper0 hA z|)
(fun _ _ => abs_nonneg _) (Finset.mem_univ _)
simpa using this
have hATE_eq :
S.ATE = ∫ ω, S.YofD true ω ∂P.μ - ∫ ω, S.YofD false ω ∂P.μ := by
unfold ATE
exact integral_sub hA.integrable_Y1 hA.integrable_Y0
have hL1 := S.miv_integral_mLower1_le_integral_Y1 hA hMIV
have hU1 := S.miv_integral_Y1_le_integral_mUpper1 hA hMIV
have hL0 := S.miv_integral_mLower0_le_integral_Y0 hA hMIV
have hU0 := S.miv_integral_Y0_le_integral_mUpper0 hA hMIV
refine ⟨?_, ?_⟩
· have hsub_lhs := integral_sub hint_mL1 hint_mU0
rw [hsub_lhs, hATE_eq]
linarith
· have hsub_rhs := integral_sub hint_mU1 hint_mL0
rw [hsub_rhs, hATE_eq]
linarith
8 supporting declarations (lemmas, instances)
-
miv_mLower1_le_cond_Y1theorem — mLower1 z ≤ E[Y(1) | Z = z] for every z ∈ supp Z.hypothesesconclusionletIProof (Lean source)
theorem miv_mLower1_le_cond_Y1 [IsFiniteMeasure P.μ] (hA : S.BaseAssumptions) (hMIV : S.MIV) {z : α} (hz : z ∈ S.support) : letI := hMIV.inst S.mLower1 hA z ≤ eventCondExp P.μ (S.zEvent z) (S.YofD true) := by letI := hMIV.inst -- The set whose sSup we take. set T : Set ℝ := {val : ℝ | ∃ u ∈ S.support, u ≤ z ∧ val = S.lowerBound1 hA.lo u} with hT -- Every element of `T` is ≤ the target. have hle_all : ∀ v ∈ T, v ≤ eventCondExp P.μ (S.zEvent z) (S.YofD true) := by rintro v ⟨u, hu, hule, rfl⟩ have h1 : S.lowerBound1 hA.lo u ≤ eventCondExp P.μ (S.zEvent u) (S.YofD true) := S.lowerBound1_le_cond_Y1 hA hu have h2 : eventCondExp P.μ (S.zEvent u) (S.YofD true) ≤ eventCondExp P.μ (S.zEvent z) (S.YofD true) := hMIV.monotone true u z hu hz hule exact le_trans h1 h2 -- Nonempty (take `u = z`). have hne : T.Nonempty := ⟨S.lowerBound1 hA.lo z, z, hz, le_refl z, rfl⟩ change sSup T ≤ _ exact csSup_le hne hle_all -
miv_cond_Y1_le_mUpper1theorem — E[Y(1) | Z = z] ≤ mUpper1 z for every z ∈ supp Z.hypothesesconclusionletIProof (Lean source)
theorem miv_cond_Y1_le_mUpper1 [IsFiniteMeasure P.μ] (hA : S.BaseAssumptions) (hMIV : S.MIV) {z : α} (hz : z ∈ S.support) : letI := hMIV.inst eventCondExp P.μ (S.zEvent z) (S.YofD true) ≤ S.mUpper1 hA z := by letI := hMIV.inst set T : Set ℝ := {val : ℝ | ∃ u ∈ S.support, z ≤ u ∧ val = S.upperBound1 hA.hi u} with hT have hge_all : ∀ v ∈ T, eventCondExp P.μ (S.zEvent z) (S.YofD true) ≤ v := by rintro v ⟨u, hu, hleu, rfl⟩ have h1 : eventCondExp P.μ (S.zEvent z) (S.YofD true) ≤ eventCondExp P.μ (S.zEvent u) (S.YofD true) := hMIV.monotone true z u hz hu hleu have h2 : eventCondExp P.μ (S.zEvent u) (S.YofD true) ≤ S.upperBound1 hA.hi u := S.cond_Y1_le_upperBound1 hA hu exact le_trans h1 h2 have hne : T.Nonempty := ⟨S.upperBound1 hA.hi z, z, hz, le_refl z, rfl⟩ change _ ≤ sInf T exact le_csInf hne hge_all -
miv_mLower0_le_cond_Y0theorem — mLower0 z ≤ E[Y(0) | Z = z] for every z ∈ supp Z.hypothesesconclusionletIProof (Lean source)
theorem miv_mLower0_le_cond_Y0 [IsFiniteMeasure P.μ] (hA : S.BaseAssumptions) (hMIV : S.MIV) {z : α} (hz : z ∈ S.support) : letI := hMIV.inst S.mLower0 hA z ≤ eventCondExp P.μ (S.zEvent z) (S.YofD false) := by letI := hMIV.inst set T : Set ℝ := {val : ℝ | ∃ u ∈ S.support, u ≤ z ∧ val = S.lowerBound0 hA.lo u} with hT have hle_all : ∀ v ∈ T, v ≤ eventCondExp P.μ (S.zEvent z) (S.YofD false) := by rintro v ⟨u, hu, hule, rfl⟩ have h1 : S.lowerBound0 hA.lo u ≤ eventCondExp P.μ (S.zEvent u) (S.YofD false) := S.lowerBound0_le_cond_Y0 hA hu have h2 : eventCondExp P.μ (S.zEvent u) (S.YofD false) ≤ eventCondExp P.μ (S.zEvent z) (S.YofD false) := hMIV.monotone false u z hu hz hule exact le_trans h1 h2 have hne : T.Nonempty := ⟨S.lowerBound0 hA.lo z, z, hz, le_refl z, rfl⟩ change sSup T ≤ _ exact csSup_le hne hle_all -
miv_cond_Y0_le_mUpper0theorem — E[Y(0) | Z = z] ≤ mUpper0 z for every z ∈ supp Z.hypothesesconclusionletIProof (Lean source)
theorem miv_cond_Y0_le_mUpper0 [IsFiniteMeasure P.μ] (hA : S.BaseAssumptions) (hMIV : S.MIV) {z : α} (hz : z ∈ S.support) : letI := hMIV.inst eventCondExp P.μ (S.zEvent z) (S.YofD false) ≤ S.mUpper0 hA z := by letI := hMIV.inst set T : Set ℝ := {val : ℝ | ∃ u ∈ S.support, z ≤ u ∧ val = S.upperBound0 hA.hi u} with hT have hge_all : ∀ v ∈ T, eventCondExp P.μ (S.zEvent z) (S.YofD false) ≤ v := by rintro v ⟨u, hu, hleu, rfl⟩ have h1 : eventCondExp P.μ (S.zEvent z) (S.YofD false) ≤ eventCondExp P.μ (S.zEvent u) (S.YofD false) := hMIV.monotone false z u hz hu hleu have h2 : eventCondExp P.μ (S.zEvent u) (S.YofD false) ≤ S.upperBound0 hA.hi u := S.cond_Y0_le_upperBound0 hA hu exact le_trans h1 h2 have hne : T.Nonempty := ⟨S.upperBound0 hA.hi z, z, hz, le_refl z, rfl⟩ change _ ≤ sInf T exact le_csInf hne hge_all -
miv_integral_mLower1_le_integral_Y1theorem — Integrated envelope bound for arm d = 1 (lower): ∫ mLower1(Z) ≤ ∫ Y(1).Proof (Lean source)
theorem miv_integral_mLower1_le_integral_Y1 [IsFiniteMeasure P.μ] [Fintype α] (hA : S.BaseAssumptions) (hMIV : S.MIV) : letI := hMIV.inst (∫ ω, S.mLower1 hA (S.factualZ ω) ∂P.μ) ≤ ∫ ω, S.YofD true ω ∂P.μ := by letI := hMIV.inst rw [S.integral_comp_factualZ_eq_sum (S.mLower1 hA), S.integral_YofD_eq_sum_over_zEvent hA true] refine Finset.sum_le_sum (fun z _ => ?_) exact S.mul_zEvent_measure_mono_of_stratum_le (a := fun z => S.mLower1 hA z) (b := fun z => eventCondExp P.μ (S.zEvent z) (S.YofD true)) (fun {z} hz => S.miv_mLower1_le_cond_Y1 hA hMIV hz) z -
miv_integral_Y1_le_integral_mUpper1theorem — Integrated envelope bound for arm d = 1 (upper): ∫ Y(1) ≤ ∫ mUpper1(Z).Proof (Lean source)
theorem miv_integral_Y1_le_integral_mUpper1 [IsFiniteMeasure P.μ] [Fintype α] (hA : S.BaseAssumptions) (hMIV : S.MIV) : letI := hMIV.inst (∫ ω, S.YofD true ω ∂P.μ) ≤ ∫ ω, S.mUpper1 hA (S.factualZ ω) ∂P.μ := by letI := hMIV.inst rw [S.integral_YofD_eq_sum_over_zEvent hA true, S.integral_comp_factualZ_eq_sum (S.mUpper1 hA)] refine Finset.sum_le_sum (fun z _ => ?_) exact S.mul_zEvent_measure_mono_of_stratum_le (a := fun z => eventCondExp P.μ (S.zEvent z) (S.YofD true)) (b := fun z => S.mUpper1 hA z) (fun {z} hz => S.miv_cond_Y1_le_mUpper1 hA hMIV hz) z -
miv_integral_mLower0_le_integral_Y0theorem — Integrated envelope bound for arm d = 0 (lower): ∫ mLower0(Z) ≤ ∫ Y(0).Proof (Lean source)
theorem miv_integral_mLower0_le_integral_Y0 [IsFiniteMeasure P.μ] [Fintype α] (hA : S.BaseAssumptions) (hMIV : S.MIV) : letI := hMIV.inst (∫ ω, S.mLower0 hA (S.factualZ ω) ∂P.μ) ≤ ∫ ω, S.YofD false ω ∂P.μ := by letI := hMIV.inst rw [S.integral_comp_factualZ_eq_sum (S.mLower0 hA), S.integral_YofD_eq_sum_over_zEvent hA false] refine Finset.sum_le_sum (fun z _ => ?_) exact S.mul_zEvent_measure_mono_of_stratum_le (a := fun z => S.mLower0 hA z) (b := fun z => eventCondExp P.μ (S.zEvent z) (S.YofD false)) (fun {z} hz => S.miv_mLower0_le_cond_Y0 hA hMIV hz) z -
miv_integral_Y0_le_integral_mUpper0theorem — Integrated envelope bound for arm d = 0 (upper): ∫ Y(0) ≤ ∫ mUpper0(Z).Proof (Lean source)
theorem miv_integral_Y0_le_integral_mUpper0 [IsFiniteMeasure P.μ] [Fintype α] (hA : S.BaseAssumptions) (hMIV : S.MIV) : letI := hMIV.inst (∫ ω, S.YofD false ω ∂P.μ) ≤ ∫ ω, S.mUpper0 hA (S.factualZ ω) ∂P.μ := by letI := hMIV.inst rw [S.integral_YofD_eq_sum_over_zEvent hA false, S.integral_comp_factualZ_eq_sum (S.mUpper0 hA)] refine Finset.sum_le_sum (fun z _ => ?_) exact S.mul_zEvent_measure_mono_of_stratum_le (a := fun z => eventCondExp P.μ (S.zEvent z) (S.YofD false)) (b := fun z => S.mUpper0 hA z) (fun {z} hz => S.miv_cond_Y0_le_mUpper0 hA hMIV hz) z
Combined 2 core · 0 supporting This file proves Manski corollaries that combine shape restrictions. ★ mtr_mts_bounds_ATE★ mtr_miv_bounds_ATE
Manski Combined Bounds
This file proves Manski corollaries that combine shape restrictions. Monotone treatment response with monotone treatment selection gives a nonnegative average treatment effect bounded above by the observed treated-control mean contrast, while monotone treatment response with a monotone instrument gives a nonnegative effect bounded above by the integrated monotone-instrument envelope.
The arguments reuse the separate monotonicity, selection, and instrument bounds proved in the preceding Manski modules.
theorem mtr_mts_bounds_ATE reviewed
⚑ flagged
Causalean.PO.POManskiIVSystem
cor:po-iv-mtr-mts. Under the baseline Manski assumptions, monotone treatment response, Y(0) ≤ Y(1) almost surely, and monotone treatment selection — each potential outcome's mean given control is no larger than its mean given treatment, the average treatment effect is nonnegative and is upper-bounded by the naive observed contrast E[Y | D=1] − E[Y | D=0].
Formal statement
hypotheses
hA :
S.BaseAssumptions
hMTR :
S.MTR
hMTS :
S.MTS
conclusion
0 ≤ S.ATE ∧
S.ATE
≤ eventCondExp P.μ (S.dEvent true) S.factualY
- eventCondExp P.μ (S.dEvent false) S.factualY
Proof (Lean source)
theorem mtr_mts_bounds_ATE (hA : S.BaseAssumptions)
(hMTR : S.MTR) (hMTS : S.MTS) :
0 ≤ S.ATE ∧
S.ATE ≤ eventCondExp P.μ (S.dEvent true) S.factualY
- eventCondExp P.μ (S.dEvent false) S.factualY := by
refine ⟨S.mtr_nonneg_ATE hA hMTR, ?_⟩
-- MTS gives E[Y(1)] ≤ E[Y|D=1] and E[Y|D=0] ≤ E[Y(0)].
have hU := S.mts_E_Y1_le_condY1 hA hMTS
have hL := S.mts_condY0_le_E_Y0 hA hMTS
have hATE_eq :
S.ATE = ∫ ω, S.YofD true ω ∂P.μ - ∫ ω, S.YofD false ω ∂P.μ := by
unfold ATE
exact integral_sub hA.integrable_Y1 hA.integrable_Y0
rw [hATE_eq]; linarith
theorem mtr_miv_bounds_ATE reviewed
⚑ flagged
Causalean.PO.POManskiIVSystem
cor:po-iv-mtr-miv. Under the baseline Manski assumptions, monotone treatment response, Y(0) ≤ Y(1) almost surely, and a monotone instrumental variable — the conditional mean of each potential outcome is nondecreasing in the instrument value across its support, the average treatment effect is nonnegative and is upper-bounded by the integrated monotone-instrument envelope contrast ∫ (mUpper1(Z) − mLower0(Z)).
Formal statement
hypotheses
conclusion
letI
Proof (Lean source)
theorem mtr_miv_bounds_ATE [IsFiniteMeasure P.μ] [Fintype α]
(hA : S.BaseAssumptions) (hMTR : S.MTR) (hMIV : S.MIV) :
letI := hMIV.inst
0 ≤ S.ATE ∧
S.ATE ≤
∫ ω, S.mUpper1 hA (S.factualZ ω) - S.mLower0 hA (S.factualZ ω) ∂P.μ := by
letI := hMIV.inst
refine ⟨S.mtr_nonneg_ATE hA hMTR, ?_⟩
exact (S.miv_bounds_ATE hA hMIV).2
Helpers 1 core · 10 supporting This file collects algebraic, measurability, integrability, and pointwise bound lemmas reused by the baseline Manski, monotone-treatment-response, monotone-treatment-selection, and monotone-instrument variants. ★ cond_YofD_le_boundArm_hi
Shared helpers for Manski-style bounds
This file collects algebraic, measurability, integrability, and pointwise bound lemmas reused by the baseline Manski, monotone-treatment-response, monotone-treatment-selection, and monotone-instrument variants. It also proves parametric conditional stratum bounds for each treatment arm.
The main public results are the arm-uniform bounds
boundArm_lo_le_cond_YofD and cond_YofD_le_boundArm_hi, together with the
legacy names lowerBound1_le_cond_Y1, cond_Y1_le_upperBound1,
lowerBound0_le_cond_Y0, and cond_Y0_le_upperBound0 used by downstream
Manski theorem files.
theorem cond_YofD_le_boundArm_hi reviewed
⚑ flagged
Causalean.PO.POManskiIVSystem
Under the baseline Manski assumptions, for any treatment arm d and any instrument value z in the support of the instrument, the conditional mean of the potential outcome Y(d) given Z = z is bounded above by the unified upper-envelope functional boundArm d hi evaluated at z.
Formal statement
hypotheses
conclusion
eventCondExp P.μ (S.zEvent z) (S.YofD d) ≤ S.boundArm d hA.hi z
Proof (Lean source)
theorem cond_YofD_le_boundArm_hi [IsFiniteMeasure P.μ]
(hA : S.BaseAssumptions) (d : Bool) {z : α} (_hz : z ∈ S.support) :
eventCondExp P.μ (S.zEvent z) (S.YofD d) ≤ S.boundArm d hA.hi z := by
have hcons : (fun ω => S.factualY ω * S.dVar.indicator d ω
+ hA.hi * S.dVar.indicator (!d) ω)
= (fun ω => S.YofD d ω * S.dVar.indicator d ω
+ hA.hi * S.dVar.indicator (!d) ω) := by
funext ω
have hvw : S.yVar.v ≠ S.dVar.v := Ne.symm S.hDY
have h := congr_fun (POVar.factual_mul_indicator_eq_cfUnder_mul_indicator_fn
hA.consistency S.yVar S.dVar d hvw) ω
rw [show S.factualY ω * S.dVar.indicator d ω = S.YofD d ω * S.dVar.indicator d ω from by
simpa [POManskiIVSystem.factualY, POManskiIVSystem.YofD] using h]
have hbound_ae :=
S.YofD_le_YofD_indD_plus_hi d hA.hi ((hA.bounded d).mono (fun _ h => h.2))
have hint_sum :
IntegrableOn (fun ω => S.YofD d ω * S.dVar.indicator d ω
+ hA.hi * S.dVar.indicator (!d) ω)
(S.zEvent z) P.μ :=
((S.YofD_mul_indD_integrable hA d).add
(S.const_mul_indD_integrable hA.hi (!d))).integrableOn
have hint_Yd : IntegrableOn (S.YofD d) (S.zEvent z) P.μ :=
(hA.integrable_YofD d).integrableOn
have hmono :
eventCondExp P.μ (S.zEvent z) (S.YofD d)
≤ eventCondExp P.μ (S.zEvent z)
(fun ω => S.YofD d ω * S.dVar.indicator d ω
+ hA.hi * S.dVar.indicator (!d) ω) := by
refine eventCondExp_mono_ae P.μ hint_Yd hint_sum ?_
exact ae_restrict_of_ae hbound_ae
calc
eventCondExp P.μ (S.zEvent z) (S.YofD d)
≤ eventCondExp P.μ (S.zEvent z)
(fun ω => S.YofD d ω * S.dVar.indicator d ω
+ hA.hi * S.dVar.indicator (!d) ω) := hmono
_ = S.boundArm d hA.hi z := by unfold boundArm; rw [hcons]
10 supporting declarations (lemmas, instances)
-
factualY_mul_indD_integrablelemma — factualY · indicator d is integrable.hypotheseshA :S.BaseAssumptionsd :conclusionIntegrable (fun ω => S.factualY ω * S.dVar.indicator d ω) P.μProof (Lean source)
lemma factualY_mul_indD_integrable (hA : S.BaseAssumptions) (d : Bool) : Integrable (fun ω => S.factualY ω * S.dVar.indicator d ω) P.μ := by exact S.dVar.integrable_mul_indicator d (measurableSet_singleton d) hA.integrable_factualY -
YofD_mul_indD_integrablelemma — YofD d · indicator d is integrable.hypotheseshA :S.BaseAssumptionsd :conclusionIntegrable (fun ω => S.YofD d ω * S.dVar.indicator d ω) P.μProof (Lean source)
lemma YofD_mul_indD_integrable (hA : S.BaseAssumptions) (d : Bool) : Integrable (fun ω => S.YofD d ω * S.dVar.indicator d ω) P.μ := by exact S.dVar.integrable_mul_indicator d (measurableSet_singleton d) (hA.integrable_YofD d) -
const_mul_indD_integrablelemma — Constant times indicator d is integrable.hypothesesconclusionIntegrable (fun ω => c * S.dVar.indicator d ω) P.μProof (Lean source)
lemma const_mul_indD_integrable [IsFiniteMeasure P.μ] (c : ℝ) (d : Bool) : Integrable (fun ω => c * S.dVar.indicator d ω) P.μ := (S.dVar.integrable_indicator d (measurableSet_singleton d)).const_mul c -
YofD_indD_plus_lo_le_YofDlemma — Pointwise a.e. bound: Y(d) · 1_{D=d} + lo · 1_{D=!d} ≤ Y(d) under lo ≤ Y(d).hypothesesconclusion(fun ω => S.YofD d ω * S.dVar.indicator d ω + lo * S.dVar.indicator (!d) ω)≤ᵐ[P.μ] S.YofD dProof (Lean source)
lemma YofD_indD_plus_lo_le_YofD (d : Bool) (lo : ℝ) (hbound : ∀ᵐ ω ∂P.μ, lo ≤ S.YofD d ω) : (fun ω => S.YofD d ω * S.dVar.indicator d ω + lo * S.dVar.indicator (!d) ω) ≤ᵐ[P.μ] S.YofD d := by refine hbound.mono (fun ω hlo => ?_) rcases S.dVar_inds_at_ω d ω with ⟨h₁, h₂⟩ | ⟨h₁, h₂⟩ <;> simp [h₁, h₂, hlo] -
YofD_le_YofD_indD_plus_hilemma — Pointwise a.e. bound: Y(d) ≤ Y(d) · 1_{D=d} + hi · 1_{D=!d} under Y(d) ≤ hi.hypothesesconclusionS.YofD d≤ᵐ[P.μ] (fun ω => S.YofD d ω * S.dVar.indicator d ω + hi * S.dVar.indicator (!d) ω)Proof (Lean source)
lemma YofD_le_YofD_indD_plus_hi (d : Bool) (hi : ℝ) (hbound : ∀ᵐ ω ∂P.μ, S.YofD d ω ≤ hi) : S.YofD d ≤ᵐ[P.μ] (fun ω => S.YofD d ω * S.dVar.indicator d ω + hi * S.dVar.indicator (!d) ω) := by refine hbound.mono (fun ω hhi => ?_) rcases S.dVar_inds_at_ω d ω with ⟨h₁, h₂⟩ | ⟨h₁, h₂⟩ <;> simp [h₁, h₂, hhi] -
boundArm_lo_le_cond_YofDtheorem — Stratum-level lower bound on eventCondExp μ (Z=z) (Y(d)) via the unified arm functional boundArm d lo.hypothesesconclusionS.boundArm d hA.lo z ≤ eventCondExp P.μ (S.zEvent z) (S.YofD d)Proof (Lean source)
theorem boundArm_lo_le_cond_YofD [IsFiniteMeasure P.μ] (hA : S.BaseAssumptions) (d : Bool) {z : α} (_hz : z ∈ S.support) : S.boundArm d hA.lo z ≤ eventCondExp P.μ (S.zEvent z) (S.YofD d) := by -- Rewrite `factualY · 1_{D=d}` as `Y(d) · 1_{D=d}` using consistency. have hcons : (fun ω => S.factualY ω * S.dVar.indicator d ω + hA.lo * S.dVar.indicator (!d) ω) = (fun ω => S.YofD d ω * S.dVar.indicator d ω + hA.lo * S.dVar.indicator (!d) ω) := by funext ω have hvw : S.yVar.v ≠ S.dVar.v := Ne.symm S.hDY have h := congr_fun (POVar.factual_mul_indicator_eq_cfUnder_mul_indicator_fn hA.consistency S.yVar S.dVar d hvw) ω rw [show S.factualY ω * S.dVar.indicator d ω = S.YofD d ω * S.dVar.indicator d ω from by simpa [POManskiIVSystem.factualY, POManskiIVSystem.YofD] using h] have hbound_ae := S.YofD_indD_plus_lo_le_YofD d hA.lo ((hA.bounded d).mono (fun _ h => h.1)) have hint_sum : IntegrableOn (fun ω => S.YofD d ω * S.dVar.indicator d ω + hA.lo * S.dVar.indicator (!d) ω) (S.zEvent z) P.μ := ((S.YofD_mul_indD_integrable hA d).add (S.const_mul_indD_integrable hA.lo (!d))).integrableOn have hint_Yd : IntegrableOn (S.YofD d) (S.zEvent z) P.μ := (hA.integrable_YofD d).integrableOn have hmono : eventCondExp P.μ (S.zEvent z) (fun ω => S.YofD d ω * S.dVar.indicator d ω + hA.lo * S.dVar.indicator (!d) ω) ≤ eventCondExp P.μ (S.zEvent z) (S.YofD d) := by refine eventCondExp_mono_ae P.μ hint_sum hint_Yd ?_ exact ae_restrict_of_ae hbound_ae calc S.boundArm d hA.lo z = eventCondExp P.μ (S.zEvent z) (fun ω => S.YofD d ω * S.dVar.indicator d ω + hA.lo * S.dVar.indicator (!d) ω) := by unfold boundArm; rw [hcons] _ ≤ eventCondExp P.μ (S.zEvent z) (S.YofD d) := hmono -
lowerBound1_le_cond_Y1theorem — Stratum-level lower bound on the *conditional expectation* of Y(1).hypothesesconclusionS.lowerBound1 hA.lo z ≤ eventCondExp P.μ (S.zEvent z) (S.YofD true)Proof (Lean source)
theorem lowerBound1_le_cond_Y1 [IsFiniteMeasure P.μ] (hA : S.BaseAssumptions) {z : α} (hz : z ∈ S.support) : S.lowerBound1 hA.lo z ≤ eventCondExp P.μ (S.zEvent z) (S.YofD true) := S.boundArm_lo_le_cond_YofD hA true hz -
cond_Y1_le_upperBound1theorem — Stratum-level upper bound on the *conditional expectation* of Y(1).hypothesesconclusioneventCondExp P.μ (S.zEvent z) (S.YofD true) ≤ S.upperBound1 hA.hi zProof (Lean source)
theorem cond_Y1_le_upperBound1 [IsFiniteMeasure P.μ] (hA : S.BaseAssumptions) {z : α} (hz : z ∈ S.support) : eventCondExp P.μ (S.zEvent z) (S.YofD true) ≤ S.upperBound1 hA.hi z := S.cond_YofD_le_boundArm_hi hA true hz -
lowerBound0_le_cond_Y0theorem — Stratum-level lower bound on the *conditional expectation* of Y(0).hypothesesconclusionS.lowerBound0 hA.lo z ≤ eventCondExp P.μ (S.zEvent z) (S.YofD false)Proof (Lean source)
theorem lowerBound0_le_cond_Y0 [IsFiniteMeasure P.μ] (hA : S.BaseAssumptions) {z : α} (hz : z ∈ S.support) : S.lowerBound0 hA.lo z ≤ eventCondExp P.μ (S.zEvent z) (S.YofD false) := S.boundArm_lo_le_cond_YofD hA false hz -
cond_Y0_le_upperBound0theorem — Stratum-level upper bound on the *conditional expectation* of Y(0).hypothesesconclusioneventCondExp P.μ (S.zEvent z) (S.YofD false) ≤ S.upperBound0 hA.hi zProof (Lean source)
theorem cond_Y0_le_upperBound0 [IsFiniteMeasure P.μ] (hA : S.BaseAssumptions) {z : α} (hz : z ∈ S.support) : eventCondExp P.μ (S.zEvent z) (S.YofD false) ≤ S.upperBound0 hA.hi z := S.cond_YofD_le_boundArm_hi hA false hz
IntervalForm 4 core · 0 supporting This file restates Manski scalar lower-and-upper bounds as closed interval membership statements for the average treatment effect. ★ manski_ATE_mem_Icc★ manski_ATE_mem_Icc_ciSup★ mtr_mts_ATE_mem_Icc★ mtr_miv_ATE_mem_Icc
Manski Interval Forms
This file restates Manski scalar lower-and-upper bounds as closed interval membership statements for the average treatment effect. It covers the no-assumption, monotone treatment response with monotone treatment selection, and monotone treatment response with monotone instrumental variable bounds.
These results add no new identification content; they translate existing sandwich inequalities into the interval vocabulary used by the partial identification engine.
theorem manski_ATE_mem_Icc reviewed
⚑ flagged
Causalean.PO.POManskiIVSystem
Set.Icc form of manski_bounds_ATE. Under the baseline Manski assumptions and mean independence of both potential outcomes from the instrument, for any two instrument values z₁, z₀ in the support of the instrument, the average treatment effect lies in the closed interval from the z₁-lower/z₀-upper worst-case bound to the z₁-upper/z₀-lower worst-case bound — the per-stratum-pair Manski no-assumption sandwich restated as interval membership.
Formal statement
hypotheses
IsFiniteMeasure P.μ
hA :
S.BaseAssumptions
hMI :
S.MeanIndep
z₁ z₀ :
α
hz₁ :
z₁ ∈ S.support
hz₀ :
z₀ ∈ S.support
conclusion
S.ATE ∈ Icc (S.lowerBound1 hA.lo z₁ - S.upperBound0 hA.hi z₀) (S.upperBound1 hA.hi z₁ - S.lowerBound0 hA.lo z₀)
Proof (Lean source)
theorem manski_ATE_mem_Icc [IsFiniteMeasure P.μ]
(hA : S.BaseAssumptions) (hMI : S.MeanIndep)
{z₁ z₀ : α} (hz₁ : z₁ ∈ S.support) (hz₀ : z₀ ∈ S.support) :
S.ATE ∈ Icc (S.lowerBound1 hA.lo z₁ - S.upperBound0 hA.hi z₀)
(S.upperBound1 hA.hi z₁ - S.lowerBound0 hA.lo z₀) := by
have h := S.manski_bounds_ATE hA hMI hz₁ hz₀
exact mem_Icc_of_sandwich h.1 h.2
theorem manski_ATE_mem_Icc_ciSup reviewed
⚑ flagged
Causalean.PO.POManskiIVSystem
Set.Icc form of manski_bounds_ATE_ciSup. Under the baseline Manski assumptions, mean independence of both potential outcomes from the instrument, and a nonempty instrument support, the average treatment effect lies in the closed interval from the supremum-of-lowers-minus-infimum-of-uppers bound to the infimum-of-uppers-minus-supremum-of-lowers bound, aggregated over every instrument stratum — the sup/inf-aggregated Manski no-assumption sandwich restated as interval membership.
Formal statement
hypotheses
conclusion
S.ATE ∈ Icc ((⨆ z : ↑S.support, S.lowerBound1 hA.lo z.val) - (⨅ z : ↑S.support, S.upperBound0 hA.hi z.val)) ((⨅ z : ↑S.support, S.upperBound1 hA.hi z.val) - (⨆ z : ↑S.support, S.lowerBound0 hA.lo z.val))
Proof (Lean source)
theorem manski_ATE_mem_Icc_ciSup [IsFiniteMeasure P.μ]
(hA : S.BaseAssumptions) (hMI : S.MeanIndep) (hne : S.support.Nonempty) :
S.ATE ∈ Icc
((⨆ z : ↑S.support, S.lowerBound1 hA.lo z.val)
- (⨅ z : ↑S.support, S.upperBound0 hA.hi z.val))
((⨅ z : ↑S.support, S.upperBound1 hA.hi z.val)
- (⨆ z : ↑S.support, S.lowerBound0 hA.lo z.val)) := by
have h := S.manski_bounds_ATE_ciSup hA hMI hne
exact mem_Icc_of_sandwich h.1 h.2
theorem mtr_mts_ATE_mem_Icc reviewed
⚑ flagged
Causalean.PO.POManskiIVSystem
Set.Icc form of mtr_mts_bounds_ATE. Under the baseline Manski assumptions, monotone treatment response, and monotone treatment selection, the average treatment effect lies in the closed interval from 0 to the naive observed contrast E[Y | D=1] − E[Y | D=0] — the MTR + MTS sandwich restated as interval membership.
Formal statement
hypotheses
hA :
S.BaseAssumptions
hMTR :
S.MTR
hMTS :
S.MTS
conclusion
S.ATE ∈ Icc 0 (eventCondExp P.μ (S.dEvent true) S.factualY - eventCondExp P.μ (S.dEvent false) S.factualY)
Proof (Lean source)
theorem mtr_mts_ATE_mem_Icc (hA : S.BaseAssumptions)
(hMTR : S.MTR) (hMTS : S.MTS) :
S.ATE ∈ Icc 0
(eventCondExp P.μ (S.dEvent true) S.factualY
- eventCondExp P.μ (S.dEvent false) S.factualY) := by
have h := S.mtr_mts_bounds_ATE hA hMTR hMTS
exact mem_Icc_of_sandwich h.1 h.2
theorem mtr_miv_ATE_mem_Icc reviewed
⚑ flagged
Causalean.PO.POManskiIVSystem
Set.Icc form of mtr_miv_bounds_ATE. Under the baseline Manski assumptions, monotone treatment response, and a monotone instrumental variable, the average treatment effect lies in the closed interval from 0 to the integrated monotone-instrument envelope contrast ∫ (mUpper1(Z) − mLower0(Z)) — the MTR + MIV sandwich restated as interval membership.
Formal statement
hypotheses
conclusion
letI
Proof (Lean source)
theorem mtr_miv_ATE_mem_Icc [IsFiniteMeasure P.μ] [Fintype α]
(hA : S.BaseAssumptions) (hMTR : S.MTR) (hMIV : S.MIV) :
letI := hMIV.inst
S.ATE ∈ Icc 0
(∫ ω, S.mUpper1 hA (S.factualZ ω) - S.mLower0 hA (S.factualZ ω) ∂P.μ) := by
letI := hMIV.inst
have h := S.mtr_miv_bounds_ATE hA hMTR hMIV
exact mem_Icc_of_sandwich h.1 h.2
MTR 1 core · 5 supporting This file proves the monotone-treatment-response sharpening of Manski bounds. ★ mtr_bounds_ATE
Manski bounds under monotone treatment response
This file proves the monotone-treatment-response sharpening of Manski bounds.
Consistency, binary-treatment event decompositions, bounded outcomes, and the
almost-sure inequality Y(0) <= Y(1) imply a nonnegative ATE and tighter
arm-wise and ATE sandwiches.
The main public conclusions are the arm comparisons mtr_E_Y_le_E_Y1 and
mtr_E_Y0_le_E_Y, the bounded-arm inequalities mtr_E_Y1_le_upper and
mtr_lower_le_E_Y0, the nonnegativity theorem mtr_nonneg_ATE, and the final
two-sided ATE statement mtr_bounds_ATE.
theorem mtr_bounds_ATE reviewed
⚑ flagged
Causalean.PO.POManskiIVSystem
The two-sided ATE sandwich from prop:po-iv-mtr. Under the baseline Manski assumptions and monotone treatment response, Y(0) ≤ Y(1) almost surely, the average treatment effect is nonnegative and is upper-bounded by the probability-weighted mix of the observed treated/control means and the range endpoints lo, hi — imputing hi for Y(1) on the control arm and lo for Y(0) on the treated arm.
Formal statement
hypotheses
hA :
S.BaseAssumptions
hMTR :
S.MTR
conclusion
0 ≤ S.ATE ∧
S.ATE
≤ ((P.μ (S.dEvent true)).toReal * eventCondExp P.μ (S.dEvent true) S.factualY + (P.μ (S.dEvent false)).toReal * hA.hi)
- ((P.μ (S.dEvent false)).toReal * eventCondExp P.μ (S.dEvent false) S.factualY + (P.μ (S.dEvent true)).toReal * hA.lo)
Proof (Lean source)
theorem mtr_bounds_ATE (hA : S.BaseAssumptions) (hMTR : S.MTR) :
0 ≤ S.ATE ∧
S.ATE ≤ ((P.μ (S.dEvent true)).toReal
* eventCondExp P.μ (S.dEvent true) S.factualY
+ (P.μ (S.dEvent false)).toReal * hA.hi)
- ((P.μ (S.dEvent false)).toReal
* eventCondExp P.μ (S.dEvent false) S.factualY
+ (P.μ (S.dEvent true)).toReal * hA.lo) := by
refine ⟨S.mtr_nonneg_ATE hA hMTR, ?_⟩
-- ATE = E[Y(1)] - E[Y(0)].
have hATE_eq :
S.ATE = ∫ ω, S.YofD true ω ∂P.μ - ∫ ω, S.YofD false ω ∂P.μ := by
unfold ATE
exact integral_sub hA.integrable_Y1 hA.integrable_Y0
have hU := S.mtr_E_Y1_le_upper hA
have hL := S.mtr_lower_le_E_Y0 hA
rw [hATE_eq]; linarith
5 supporting declarations (lemmas, instances)
-
mtr_E_Y_le_E_Y1theorem — Step 1 of prop:po-iv-mtr: E[Y] ≤ E[Y(1)].hypotheseshA :S.BaseAssumptionshMTR :S.MTRconclusion∫ ω, S.factualY ω ∂P.μ ≤ ∫ ω, S.YofD true ω ∂P.μProof (Lean source)
theorem mtr_E_Y_le_E_Y1 (hA : S.BaseAssumptions) (hMTR : S.MTR) : ∫ ω, S.factualY ω ∂P.μ ≤ ∫ ω, S.YofD true ω ∂P.μ := integral_mono_ae hA.integrable_factualY hA.integrable_Y1 (S.factualY_le_YofD_true hA hMTR) -
mtr_E_Y0_le_E_Ytheorem — Step 4 of prop:po-iv-mtr: E[Y(0)] ≤ E[Y].hypotheseshA :S.BaseAssumptionshMTR :S.MTRconclusion∫ ω, S.YofD false ω ∂P.μ ≤ ∫ ω, S.factualY ω ∂P.μProof (Lean source)
theorem mtr_E_Y0_le_E_Y (hA : S.BaseAssumptions) (hMTR : S.MTR) : ∫ ω, S.YofD false ω ∂P.μ ≤ ∫ ω, S.factualY ω ∂P.μ := integral_mono_ae hA.integrable_Y0 hA.integrable_factualY (S.YofD_false_le_factualY hA hMTR) -
mtr_E_Y1_le_uppertheorem — Step 2 of prop:po-iv-mtr: E[Y(1)] ≤ p·E[Y|D=1] + (1-p)·b.hypotheseshA :S.BaseAssumptionsProof (Lean source)
theorem mtr_E_Y1_le_upper (hA : S.BaseAssumptions) : ∫ ω, S.YofD true ω ∂P.μ ≤ (P.μ (S.dEvent true)).toReal * eventCondExp P.μ (S.dEvent true) S.factualY + (P.μ (S.dEvent false)).toReal * hA.hi := by -- Decompose: E[Y(1)] = p·E[Y(1)|D=1] + (1-p)·E[Y(1)|D=0]. have hdecomp := S.integral_eq_sum_eventCondExp_dEvent (S.YofD true) hA.integrable_Y1 -- Rewrite both summands as set integrals. have h1 := eventCondExp_mul_measure_toReal P.μ (S.dEvent true) (measure_ne_top _ _) (S.YofD true) have h0 := eventCondExp_mul_measure_toReal P.μ (S.dEvent false) (measure_ne_top _ _) (S.YofD true) rw [h1, h0] at hdecomp -- First set integral: use consistency to swap Y(1) ↔ Y on {D=1}. have hset_true : ∫ ω in S.dEvent true, S.YofD true ω ∂P.μ = ∫ ω in S.dEvent true, S.factualY ω ∂P.μ := by refine setIntegral_congr_fun (S.measurableSet_dEvent true) ?_ intro ω hω have hvw : S.yVar.v ≠ S.dVar.v := Ne.symm S.hDY have := POVar.cf_eq_factual_on_event hA.consistency S.yVar S.dVar true hvw hω simpa [POManskiIVSystem.YofD, POManskiIVSystem.factualY] using this -- Rewrite the first summand as p · E[Y|D=1]. have hfirst : ∫ ω in S.dEvent true, S.YofD true ω ∂P.μ = (P.μ (S.dEvent true)).toReal * eventCondExp P.μ (S.dEvent true) S.factualY := by rw [hset_true, ← eventCondExp_mul_measure_toReal P.μ (S.dEvent true) (measure_ne_top _ _) S.factualY, mul_comm] -- Bound the second summand: ∫_{D=0} Y(1) ≤ hi · (μ(D=0)).toReal. have hbd_ae : S.YofD true ≤ᵐ[P.μ] (fun _ => hA.hi) := hA.bounded_one.mono (fun _ h => h.2) have hsecond_le : ∫ ω in S.dEvent false, S.YofD true ω ∂P.μ ≤ (P.μ (S.dEvent false)).toReal * hA.hi := by have hconst_int : ∫ _ω in S.dEvent false, hA.hi ∂P.μ = (P.μ (S.dEvent false)).toReal * hA.hi := by rw [MeasureTheory.setIntegral_const, MeasureTheory.measureReal_def, smul_eq_mul, mul_comm] calc ∫ ω in S.dEvent false, S.YofD true ω ∂P.μ ≤ ∫ _ω in S.dEvent false, hA.hi ∂P.μ := by exact setIntegral_mono_ae hA.integrable_Y1.integrableOn (integrable_const hA.hi).integrableOn hbd_ae _ = (P.μ (S.dEvent false)).toReal * hA.hi := hconst_int -- Combine. rw [hdecomp, hfirst] linarith [hsecond_le] -
mtr_lower_le_E_Y0theorem — Step 3 of prop:po-iv-mtr: (1-p)·E[Y|D=0] + p·a ≤ E[Y(0)].hypotheseshA :S.BaseAssumptionsProof (Lean source)
theorem mtr_lower_le_E_Y0 (hA : S.BaseAssumptions) : (P.μ (S.dEvent false)).toReal * eventCondExp P.μ (S.dEvent false) S.factualY + (P.μ (S.dEvent true)).toReal * hA.lo ≤ ∫ ω, S.YofD false ω ∂P.μ := by -- Decompose: E[Y(0)] = p·E[Y(0)|D=1] + (1-p)·E[Y(0)|D=0]. have hdecomp := S.integral_eq_sum_eventCondExp_dEvent (S.YofD false) hA.integrable_Y0 have h1 := eventCondExp_mul_measure_toReal P.μ (S.dEvent true) (measure_ne_top _ _) (S.YofD false) have h0 := eventCondExp_mul_measure_toReal P.μ (S.dEvent false) (measure_ne_top _ _) (S.YofD false) rw [h1, h0] at hdecomp -- On {D = 0}: consistency gives ∫_{D=0} Y(0) = ∫_{D=0} Y. have hset_false : ∫ ω in S.dEvent false, S.YofD false ω ∂P.μ = ∫ ω in S.dEvent false, S.factualY ω ∂P.μ := by refine setIntegral_congr_fun (S.measurableSet_dEvent false) ?_ intro ω hω have hvw : S.yVar.v ≠ S.dVar.v := Ne.symm S.hDY have := POVar.cf_eq_factual_on_event hA.consistency S.yVar S.dVar false hvw hω simpa [POManskiIVSystem.YofD, POManskiIVSystem.factualY] using this have hsecond : ∫ ω in S.dEvent false, S.YofD false ω ∂P.μ = (P.μ (S.dEvent false)).toReal * eventCondExp P.μ (S.dEvent false) S.factualY := by rw [hset_false, ← eventCondExp_mul_measure_toReal P.μ (S.dEvent false) (measure_ne_top _ _) S.factualY, mul_comm] -- Bound the first summand below: lo · (μ(D=1)).toReal ≤ ∫_{D=1} Y(0). have hbd_ae : (fun _ : P.Ω => hA.lo) ≤ᵐ[P.μ] S.YofD false := hA.bounded_zero.mono (fun _ h => h.1) have hfirst_ge : (P.μ (S.dEvent true)).toReal * hA.lo ≤ ∫ ω in S.dEvent true, S.YofD false ω ∂P.μ := by have hconst_int : ∫ _ω in S.dEvent true, hA.lo ∂P.μ = (P.μ (S.dEvent true)).toReal * hA.lo := by rw [MeasureTheory.setIntegral_const, MeasureTheory.measureReal_def, smul_eq_mul, mul_comm] calc (P.μ (S.dEvent true)).toReal * hA.lo = ∫ _ω in S.dEvent true, hA.lo ∂P.μ := hconst_int.symm _ ≤ ∫ ω in S.dEvent true, S.YofD false ω ∂P.μ := by exact setIntegral_mono_ae (integrable_const hA.lo).integrableOn hA.integrable_Y0.integrableOn hbd_ae rw [hdecomp, hsecond] linarith [hfirst_ge] -
mtr_nonneg_ATEtheorem — Step 5 (ATE nonnegativity) of prop:po-iv-mtr: 0 ≤ ATE.hypotheseshA :S.BaseAssumptionshMTR :S.MTRconclusion0 ≤ S.ATEProof (Lean source)
theorem mtr_nonneg_ATE (hA : S.BaseAssumptions) (hMTR : S.MTR) : 0 ≤ S.ATE := by have hdiff : (0 : P.Ω → ℝ) ≤ᵐ[P.μ] (fun ω => S.YofD true ω - S.YofD false ω) := by refine hMTR.monotone.mono (fun ω h => ?_) simpa using sub_nonneg.mpr h have hint : Integrable (fun ω => S.YofD true ω - S.YofD false ω) P.μ := hA.integrable_Y1.sub hA.integrable_Y0 have h := integral_mono_ae (integrable_const 0) hint hdiff simpa [ATE, integral_zero] using h
MTS 1 core · 11 supporting This file proves the monotone-treatment-selection version of the Manski bounds. ★ mts_bounds_ATE
Manski bounds under monotone treatment selection
This file proves the monotone-treatment-selection version of the Manski bounds.
Under consistency and bounded outcomes, the monotone-treatment-selection
inequalities compare treatment-specific conditional means and yield a two-sided
ATE sandwich. The statements use the zero-measure convention of eventCondExp
and do not require strict treated/control cell positivity.
The central public results are the binary total-law decomposition
integral_YofD_eq_total_law, the four arm bounds mts_lower_le_E_Y1,
mts_E_Y1_le_condY1, mts_condY0_le_E_Y0, mts_E_Y0_le_upper, and the final
ATE sandwich mts_bounds_ATE.
theorem mts_bounds_ATE reviewed
⚑ flagged
Causalean.PO.POManskiIVSystem
MTS bounds for the ATE. Under the baseline Manski assumptions and monotone treatment selection — each potential outcome's mean given control is no larger than its mean given treatment, the average treatment effect is sandwiched between a lower bound built from the probability-weighted observed treated mean plus the range floor lo, minus the probability-weighted mix of the range ceiling hi and the observed control mean, and an upper bound equal to the naive observed contrast E[Y | D=1] − E[Y | D=0] — obtained by subtracting the Y(0) upper/lower bounds from the Y(1) lower/upper bounds.
Formal statement
hypotheses
hA :
S.BaseAssumptions
hMTS :
S.MTS
conclusion
+ (1 - (P.μ (S.dEvent true)).toReal) * hA.lo
- ((P.μ (S.dEvent true)).toReal * hA.hi + (1 - (P.μ (S.dEvent true)).toReal) * eventCondExp P.μ (S.dEvent false) S.factualY)
≤ S.ATE ∧
S.ATE
≤ eventCondExp P.μ (S.dEvent true) S.factualY
- eventCondExp P.μ (S.dEvent false) S.factualY
Proof (Lean source)
theorem mts_bounds_ATE (hA : S.BaseAssumptions) (hMTS : S.MTS) :
(P.μ (S.dEvent true)).toReal
* eventCondExp P.μ (S.dEvent true) S.factualY
+ (1 - (P.μ (S.dEvent true)).toReal) * hA.lo
- ((P.μ (S.dEvent true)).toReal * hA.hi
+ (1 - (P.μ (S.dEvent true)).toReal)
* eventCondExp P.μ (S.dEvent false) S.factualY)
≤ S.ATE
∧ S.ATE
≤ eventCondExp P.μ (S.dEvent true) S.factualY
- eventCondExp P.μ (S.dEvent false) S.factualY := by
have hATE_eq :
S.ATE = ∫ ω, S.YofD true ω ∂P.μ - ∫ ω, S.YofD false ω ∂P.μ := by
unfold ATE
exact integral_sub hA.integrable_Y1 hA.integrable_Y0
have h1L := S.mts_lower_le_E_Y1 hA hMTS
have h1U := S.mts_E_Y1_le_condY1 hA hMTS
have h0L := S.mts_condY0_le_E_Y0 hA hMTS
have h0U := S.mts_E_Y0_le_upper hA hMTS
refine ⟨?_, ?_⟩
· rw [hATE_eq]; linarith
· rw [hATE_eq]; linarith
11 supporting declarations (lemmas, instances)
-
compl_dEvent_truelemma — Complement of {D = true} is {D = false} (Bool case-split). -
compl_dEvent_falselemma — Complement of {D = false} is {D = true} (Bool case-split). -
prob_dEvent_true_add_falselemma — Probability split: P(D=true).toReal + P(D=false).toReal = 1.Proof (Lean source)
lemma prob_dEvent_true_add_false : (P.μ (S.dEvent true)).toReal + (P.μ (S.dEvent false)).toReal = 1 := by have hmeas : MeasurableSet (S.dEvent true) := S.measurableSet_dEvent true have hcompl : (S.dEvent true)ᶜ = S.dEvent false := S.compl_dEvent_true have hadd : P.μ (S.dEvent true) + P.μ (S.dEvent false) = 1 := by rw [← hcompl] rw [MeasureTheory.measure_add_measure_compl hmeas] exact MeasureTheory.IsProbabilityMeasure.measure_univ have hfin1 : P.μ (S.dEvent true) ≠ ⊤ := measure_ne_top _ _ have hfin2 : P.μ (S.dEvent false) ≠ ⊤ := measure_ne_top _ _ have := congrArg toReal hadd rw [ENNReal.toReal_add hfin1 hfin2] at this simpa using this -
integral_YofD_eq_total_lawtheorem — Total-law decomposition for YofD d across the binary partition {D=true} ⊔ {D=false}, via the generic Fintype total law.hypotheseshA :S.BaseAssumptionsd :conclusion∫ ω, S.YofD d ω ∂P.μProof (Lean source)
theorem integral_YofD_eq_total_law (hA : S.BaseAssumptions) (d : Bool) : ∫ ω, S.YofD d ω ∂P.μ = (P.μ (S.dEvent true)).toReal * eventCondExp P.μ (S.dEvent true) (S.YofD d) + (P.μ (S.dEvent false)).toReal * eventCondExp P.μ (S.dEvent false) (S.YofD d) := by have hint : Integrable (S.YofD d) P.μ := by cases d · exact hA.integrable_Y0 · exact hA.integrable_Y1 have h := integral_eq_sum_measure_mul_eventCondExp (μ := P.μ) (A := S.dEvent) S.measurableSet_dEvent S.pairwise_disjoint_dEvent S.iUnion_dEvent (S.YofD d) hint simpa [Fintype.sum_bool] using h -
YofD_eq_factualY_on_dEventlemma — Pointwise consistency on {D = d}: YofD d = factualY on this event.hypothesesconclusionS.YofD d ω = S.factualY ωProof (Lean source)
lemma YofD_eq_factualY_on_dEvent (hA : S.BaseAssumptions) (d : Bool) {ω : P.Ω} (hω : ω ∈ S.dEvent d) : S.YofD d ω = S.factualY ω := POVar.cf_eq_factual_on_event hA.consistency S.yVar S.dVar d (Ne.symm S.hDY) hω -
eventCondExp_YofD_eq_factualYlemma — E[Y(d) | D = d] = E[Y | D = d] via consistency on the event.hypotheseshA :S.BaseAssumptionsd :conclusioneventCondExp P.μ (S.dEvent d) (S.YofD d) = eventCondExp P.μ (S.dEvent d) S.factualYProof (Lean source)
lemma eventCondExp_YofD_eq_factualY (hA : S.BaseAssumptions) (d : Bool) : eventCondExp P.μ (S.dEvent d) (S.YofD d) = eventCondExp P.μ (S.dEvent d) S.factualY := POVar.eventCondExp_cfUnder_eq_factual_on_event hA.consistency S.yVar S.dVar d (S.measurableSet_dEvent d) (Ne.symm S.hDY) P.μ -
measure_mul_eventCondExp_constlemma — (μ A).toReal * eventCondExp μ A (fun _ => c) = (μ A).toReal * c. Follows from eventCondExp_mul_measure_toReal with the constant integrand.hypothesesA :Set P.Ωc :ℝconclusion(P.μ A).toReal * eventCondExp P.μ A (fun _ : P.Ω => c) = (P.μ A).toReal * cProof (Lean source)
lemma measure_mul_eventCondExp_const (A : Set P.Ω) (c : ℝ) : (P.μ A).toReal * eventCondExp P.μ A (fun _ : P.Ω => c) = (P.μ A).toReal * c := by rw [mul_comm, eventCondExp_mul_measure_toReal P.μ A (measure_ne_top _ _)] rw [MeasureTheory.setIntegral_const, smul_eq_mul, MeasureTheory.measureReal_def, mul_comm] -
mts_lower_le_E_Y1theorem — MTS lower bound on E[Y(1)]: p · E[Y|D=1] + (1-p) · a ≤ E[Y(1)].hypotheseshA :S.BaseAssumptions_hMTS :S.MTSProof (Lean source)
theorem mts_lower_le_E_Y1 (hA : S.BaseAssumptions) (_hMTS : S.MTS) : (P.μ (S.dEvent true)).toReal * eventCondExp P.μ (S.dEvent true) S.factualY + (1 - (P.μ (S.dEvent true)).toReal) * hA.lo ≤ ∫ ω, S.YofD true ω ∂P.μ := by -- From boundedness: `a ≤ E[Y(1) | D=0]`. set p := (P.μ (S.dEvent true)).toReal with hp have hp_add : p + (P.μ (S.dEvent false)).toReal = 1 := S.prob_dEvent_true_add_false have hq : (P.μ (S.dEvent false)).toReal = 1 - p := by linarith -- Total-law decomposition. have hTL := S.integral_YofD_eq_total_law hA true -- Bound `E[Y(1) | D=0] ≥ a` via `bounded_one` + `eventCondExp_mono_ae`. have hlo_ae : (fun _ : P.Ω => hA.lo) ≤ᵐ[P.μ] S.YofD true := hA.bounded_one.mono (fun _ h => h.1) have hint_const : IntegrableOn (fun _ : P.Ω => hA.lo) (S.dEvent false) P.μ := (integrable_const hA.lo).integrableOn have hint_Y1 : IntegrableOn (S.YofD true) (S.dEvent false) P.μ := hA.integrable_Y1.integrableOn have hlo_cond : eventCondExp P.μ (S.dEvent false) (fun _ => hA.lo) ≤ eventCondExp P.μ (S.dEvent false) (S.YofD true) := by exact eventCondExp_mono_ae P.μ hint_const hint_Y1 (ae_restrict_of_ae hlo_ae) -- `eventCondExp μ A (fun _ => c) = c` when `μ A ≠ 0`; else both sides are -- `0`. In either case the inequality `c ≤ eventCondExp μ A f` together -- with `(μ A).toReal * c ≤ (μ A).toReal * eventCondExp μ A f` follows by -- multiplying by a nonneg scalar. have hq_nn : (0 : ℝ) ≤ (P.μ (S.dEvent false)).toReal := ENNReal.toReal_nonneg -- Compute: (μ (dEvent false)).toReal * eventCondExp ... (fun _ => a) = -- ∫ in dEvent false, a = (μ (dEvent false)).toReal * a. have heq_const : (P.μ (S.dEvent false)).toReal * eventCondExp P.μ (S.dEvent false) (fun _ : P.Ω => hA.lo) = (P.μ (S.dEvent false)).toReal * hA.lo := measure_mul_eventCondExp_const (P := P) (S.dEvent false) hA.lo -- Multiply both sides of hlo_cond by (μ (dEvent false)).toReal. have hmul : (P.μ (S.dEvent false)).toReal * eventCondExp P.μ (S.dEvent false) (fun _ => hA.lo) ≤ (P.μ (S.dEvent false)).toReal * eventCondExp P.μ (S.dEvent false) (S.YofD true) := mul_le_mul_of_nonneg_left hlo_cond hq_nn rw [heq_const] at hmul -- Use consistency on `{D=1}`: eventCondExp μ (dEvent true) (YofD true) -- = eventCondExp μ (dEvent true) factualY. have hcons1 := S.eventCondExp_YofD_eq_factualY hA true -- Combine. rw [hq] at hmul calc p * eventCondExp P.μ (S.dEvent true) S.factualY + (1 - p) * hA.lo = p * eventCondExp P.μ (S.dEvent true) (S.YofD true) + (1 - p) * hA.lo := by rw [hcons1] _ ≤ p * eventCondExp P.μ (S.dEvent true) (S.YofD true) + (1 - p) * eventCondExp P.μ (S.dEvent false) (S.YofD true) := by linarith _ = ∫ ω, S.YofD true ω ∂P.μ := by rw [hTL, hq] -
mts_E_Y1_le_condY1theorem — MTS upper bound on E[Y(1)]: E[Y(1)] ≤ E[Y|D=1].hypotheseshA :S.BaseAssumptionshMTS :S.MTSconclusionProof (Lean source)
theorem mts_E_Y1_le_condY1 (hA : S.BaseAssumptions) (hMTS : S.MTS) : ∫ ω, S.YofD true ω ∂P.μ ≤ eventCondExp P.μ (S.dEvent true) S.factualY := by set p := (P.μ (S.dEvent true)).toReal with hp have hp_add : p + (P.μ (S.dEvent false)).toReal = 1 := S.prob_dEvent_true_add_false have hq : (P.μ (S.dEvent false)).toReal = 1 - p := by linarith have hp_nn : (0 : ℝ) ≤ p := ENNReal.toReal_nonneg have hq_nn : (0 : ℝ) ≤ 1 - p := hq ▸ ENNReal.toReal_nonneg have hTL := S.integral_YofD_eq_total_law hA true -- MTS: E[Y(1)|D=0] ≤ E[Y(1)|D=1]. have hmts := hMTS.mts_one true have hcons1 := S.eventCondExp_YofD_eq_factualY hA true -- Chain: -- ∫ YofD true = p · E[Y(1)|D=1] + (1-p) · E[Y(1)|D=0] -- ≤ p · E[Y(1)|D=1] + (1-p) · E[Y(1)|D=1] -- = E[Y(1)|D=1] -- = E[Y|D=1]. calc ∫ ω, S.YofD true ω ∂P.μ = p * eventCondExp P.μ (S.dEvent true) (S.YofD true) + (1 - p) * eventCondExp P.μ (S.dEvent false) (S.YofD true) := by rw [hTL, hq] _ ≤ p * eventCondExp P.μ (S.dEvent true) (S.YofD true) + (1 - p) * eventCondExp P.μ (S.dEvent true) (S.YofD true) := by have := mul_le_mul_of_nonneg_left hmts hq_nn linarith _ = eventCondExp P.μ (S.dEvent true) (S.YofD true) := by ring _ = eventCondExp P.μ (S.dEvent true) S.factualY := hcons1 -
mts_condY0_le_E_Y0theorem — MTS lower bound on E[Y(0)]: E[Y|D=0] ≤ E[Y(0)].hypotheseshA :S.BaseAssumptionshMTS :S.MTSconclusionProof (Lean source)
theorem mts_condY0_le_E_Y0 (hA : S.BaseAssumptions) (hMTS : S.MTS) : eventCondExp P.μ (S.dEvent false) S.factualY ≤ ∫ ω, S.YofD false ω ∂P.μ := by set p := (P.μ (S.dEvent true)).toReal with hp have hp_add : p + (P.μ (S.dEvent false)).toReal = 1 := S.prob_dEvent_true_add_false have hq : (P.μ (S.dEvent false)).toReal = 1 - p := by linarith have hp_nn : (0 : ℝ) ≤ p := ENNReal.toReal_nonneg have hq_nn : (0 : ℝ) ≤ 1 - p := hq ▸ ENNReal.toReal_nonneg have hTL := S.integral_YofD_eq_total_law hA false -- MTS on `d = 0`: E[Y(0)|D=0] ≤ E[Y(0)|D=1]. have hmts := hMTS.mts_one false have hcons0 := S.eventCondExp_YofD_eq_factualY hA false calc eventCondExp P.μ (S.dEvent false) S.factualY = eventCondExp P.μ (S.dEvent false) (S.YofD false) := hcons0.symm _ = p * eventCondExp P.μ (S.dEvent false) (S.YofD false) + (1 - p) * eventCondExp P.μ (S.dEvent false) (S.YofD false) := by ring _ ≤ p * eventCondExp P.μ (S.dEvent true) (S.YofD false) + (1 - p) * eventCondExp P.μ (S.dEvent false) (S.YofD false) := by have := mul_le_mul_of_nonneg_left hmts hp_nn linarith _ = ∫ ω, S.YofD false ω ∂P.μ := by rw [hTL, hq] -
mts_E_Y0_le_uppertheorem — MTS upper bound on E[Y(0)]: E[Y(0)] ≤ p · b + (1-p) · E[Y|D=0].hypotheseshA :S.BaseAssumptions_hMTS :S.MTSProof (Lean source)
theorem mts_E_Y0_le_upper (hA : S.BaseAssumptions) (_hMTS : S.MTS) : ∫ ω, S.YofD false ω ∂P.μ ≤ (P.μ (S.dEvent true)).toReal * hA.hi + (1 - (P.μ (S.dEvent true)).toReal) * eventCondExp P.μ (S.dEvent false) S.factualY := by set p := (P.μ (S.dEvent true)).toReal with hp have hp_add : p + (P.μ (S.dEvent false)).toReal = 1 := S.prob_dEvent_true_add_false have hq : (P.μ (S.dEvent false)).toReal = 1 - p := by linarith have hp_nn : (0 : ℝ) ≤ p := ENNReal.toReal_nonneg have hTL := S.integral_YofD_eq_total_law hA false -- Boundedness: Y(0) ≤ b a.s., hence E[Y(0)|D=1] ≤ b. have hhi_ae : S.YofD false ≤ᵐ[P.μ] (fun _ : P.Ω => hA.hi) := hA.bounded_zero.mono (fun _ h => h.2) have hint_Y0 : IntegrableOn (S.YofD false) (S.dEvent true) P.μ := hA.integrable_Y0.integrableOn have hint_const : IntegrableOn (fun _ : P.Ω => hA.hi) (S.dEvent true) P.μ := (integrable_const hA.hi).integrableOn have hhi_cond : eventCondExp P.μ (S.dEvent true) (S.YofD false) ≤ eventCondExp P.μ (S.dEvent true) (fun _ => hA.hi) := eventCondExp_mono_ae P.μ hint_Y0 hint_const (ae_restrict_of_ae hhi_ae) have heq_const : p * eventCondExp P.μ (S.dEvent true) (fun _ : P.Ω => hA.hi) = p * hA.hi := measure_mul_eventCondExp_const (P := P) (S.dEvent true) hA.hi have hmul : p * eventCondExp P.μ (S.dEvent true) (S.YofD false) ≤ p * eventCondExp P.μ (S.dEvent true) (fun _ => hA.hi) := mul_le_mul_of_nonneg_left hhi_cond hp_nn rw [heq_const] at hmul have hcons0 := S.eventCondExp_YofD_eq_factualY hA false calc ∫ ω, S.YofD false ω ∂P.μ = p * eventCondExp P.μ (S.dEvent true) (S.YofD false) + (1 - p) * eventCondExp P.μ (S.dEvent false) (S.YofD false) := by rw [hTL, hq] _ ≤ p * hA.hi + (1 - p) * eventCondExp P.μ (S.dEvent false) (S.YofD false) := by linarith _ = p * hA.hi + (1 - p) * eventCondExp P.μ (S.dEvent false) S.factualY := by rw [hcons0]
NonAsp 2 core · 8 supporting This file proves the baseline integral-level Manski bounds without additional shape restrictions. ★ manski_bounds_ATE★ manski_bounds_ATE_ciSup
Baseline non-asymptotic Manski bounds
This file proves the baseline integral-level Manski bounds without additional shape restrictions. Conditional stratum bounds from the shared helper file are combined with mean independence to place the ATE between the worst-case lower and upper endpoints.
The file exposes per-stratum integral bounds for Y(1) and Y(0), the
two-stratum ATE sandwich manski_bounds_ATE, and the support-aggregated
supremum/infimum statement manski_bounds_ATE_ciSup.
theorem manski_bounds_ATE reviewed
⚑ flagged
Causalean.PO.POManskiIVSystem
Manski bounds for the ATE under an imperfect instrument. For any two instrument strata z₁ and z₀ in the support of the instrument, the average treatment effect is sandwiched between the worst-case lower bound formed from the z₁-stratum lower envelope and z₀-stratum upper envelope, and the corresponding upper bound with the roles reversed — using only bounded outcomes and mean independence of the instrument, with no selection assumptions.
Formal statement
hypotheses
IsFiniteMeasure P.μ
hA :
S.BaseAssumptions
hMI :
S.MeanIndep
z₁ z₀ :
α
hz₁ :
z₁ ∈ S.support
hz₀ :
z₀ ∈ S.support
conclusion
S.lowerBound1 hA.lo z₁ - S.upperBound0 hA.hi z₀ ≤ S.ATE ∧
S.ATE ≤ S.upperBound1 hA.hi z₁ - S.lowerBound0 hA.lo z₀
Proof (Lean source)
theorem manski_bounds_ATE [IsFiniteMeasure P.μ]
(hA : S.BaseAssumptions) (hMI : S.MeanIndep)
{z₁ z₀ : α} (hz₁ : z₁ ∈ S.support) (hz₀ : z₀ ∈ S.support) :
S.lowerBound1 hA.lo z₁ - S.upperBound0 hA.hi z₀ ≤ S.ATE
∧ S.ATE ≤ S.upperBound1 hA.hi z₁ - S.lowerBound0 hA.lo z₀ := by
have hL1 : S.lowerBound1 hA.lo z₁ ≤ ∫ ω, S.YofD true ω ∂P.μ :=
S.lowerBound1_le_integral_Y1 hA hMI hz₁
have hU1 : ∫ ω, S.YofD true ω ∂P.μ ≤ S.upperBound1 hA.hi z₁ :=
S.integral_Y1_le_upperBound1 hA hMI hz₁
have hL0 : S.lowerBound0 hA.lo z₀ ≤ ∫ ω, S.YofD false ω ∂P.μ :=
S.lowerBound0_le_integral_Y0 hA hMI hz₀
have hU0 : ∫ ω, S.YofD false ω ∂P.μ ≤ S.upperBound0 hA.hi z₀ :=
S.integral_Y0_le_upperBound0 hA hMI hz₀
have hATE_eq :
S.ATE = ∫ ω, S.YofD true ω ∂P.μ - ∫ ω, S.YofD false ω ∂P.μ := by
unfold ATE
exact integral_sub hA.integrable_Y1 hA.integrable_Y0
refine ⟨?_, ?_⟩
· rw [hATE_eq]; linarith
· rw [hATE_eq]; linarith
theorem manski_bounds_ATE_ciSup reviewed
⚑ flagged
Causalean.PO.POManskiIVSystem
Manski bounds for the ATE in sup/inf form. Under the baseline Manski assumptions, mean independence of the instrument, and a nonempty instrument support, the average treatment effect is sandwiched between the supremum of the lower-envelope bounds minus the infimum of the upper-envelope bounds on one side, and the infimum of the upper-envelope bounds minus the supremum of the lower-envelope bounds on the other, aggregated over the whole instrument support.
Formal statement
hypotheses
conclusion
(⨆ z : ↑S.support, S.lowerBound1 hA.lo z.val)
- (⨅ z : ↑S.support, S.upperBound0 hA.hi z.val)
≤ S.ATE ∧
S.ATE
≤ (⨅ z : ↑S.support, S.upperBound1 hA.hi z.val)
- (⨆ z : ↑S.support, S.lowerBound0 hA.lo z.val)
Proof (Lean source)
theorem manski_bounds_ATE_ciSup [IsFiniteMeasure P.μ]
(hA : S.BaseAssumptions) (hMI : S.MeanIndep) (hne : S.support.Nonempty) :
(⨆ z : ↑S.support, S.lowerBound1 hA.lo z.val)
- (⨅ z : ↑S.support, S.upperBound0 hA.hi z.val) ≤ S.ATE
∧ S.ATE ≤ (⨅ z : ↑S.support, S.upperBound1 hA.hi z.val)
- (⨆ z : ↑S.support, S.lowerBound0 hA.lo z.val) := by
have hL1 := S.ciSup_lowerBound1_le_integral_Y1 hA hMI hne
have hU1 := S.integral_Y1_le_ciInf_upperBound1 hA hMI hne
have hL0 := S.ciSup_lowerBound0_le_integral_Y0 hA hMI hne
have hU0 := S.integral_Y0_le_ciInf_upperBound0 hA hMI hne
have hATE_eq :
S.ATE = ∫ ω, S.YofD true ω ∂P.μ - ∫ ω, S.YofD false ω ∂P.μ := by
unfold ATE
exact integral_sub hA.integrable_Y1 hA.integrable_Y0
refine ⟨?_, ?_⟩
· rw [hATE_eq]; linarith
· rw [hATE_eq]; linarith
8 supporting declarations (lemmas, instances)
-
lowerBound1_le_integral_Y1theorem — Stratum-level lower bound on E[Y(1)].hypothesesconclusionS.lowerBound1 hA.lo z ≤ ∫ ω, S.YofD true ω ∂P.μProof (Lean source)
theorem lowerBound1_le_integral_Y1 [IsFiniteMeasure P.μ] (hA : S.BaseAssumptions) (hMI : S.MeanIndep) {z : α} (hz : z ∈ S.support) : S.lowerBound1 hA.lo z ≤ ∫ ω, S.YofD true ω ∂P.μ := (S.lowerBound1_le_cond_Y1 hA hz).trans_eq (hMI.meanIndep_one z hz) -
integral_Y1_le_upperBound1theorem — Stratum-level upper bound on E[Y(1)].hypothesesconclusion∫ ω, S.YofD true ω ∂P.μ ≤ S.upperBound1 hA.hi zProof (Lean source)
theorem integral_Y1_le_upperBound1 [IsFiniteMeasure P.μ] (hA : S.BaseAssumptions) (hMI : S.MeanIndep) {z : α} (hz : z ∈ S.support) : ∫ ω, S.YofD true ω ∂P.μ ≤ S.upperBound1 hA.hi z := (hMI.meanIndep_one z hz).symm.trans_le (S.cond_Y1_le_upperBound1 hA hz) -
lowerBound0_le_integral_Y0theorem — Stratum-level lower bound on E[Y(0)].hypothesesconclusionS.lowerBound0 hA.lo z ≤ ∫ ω, S.YofD false ω ∂P.μProof (Lean source)
theorem lowerBound0_le_integral_Y0 [IsFiniteMeasure P.μ] (hA : S.BaseAssumptions) (hMI : S.MeanIndep) {z : α} (hz : z ∈ S.support) : S.lowerBound0 hA.lo z ≤ ∫ ω, S.YofD false ω ∂P.μ := (S.lowerBound0_le_cond_Y0 hA hz).trans_eq (hMI.meanIndep_zero z hz) -
integral_Y0_le_upperBound0theorem — Stratum-level upper bound on E[Y(0)].hypothesesconclusion∫ ω, S.YofD false ω ∂P.μ ≤ S.upperBound0 hA.hi zProof (Lean source)
theorem integral_Y0_le_upperBound0 [IsFiniteMeasure P.μ] (hA : S.BaseAssumptions) (hMI : S.MeanIndep) {z : α} (hz : z ∈ S.support) : ∫ ω, S.YofD false ω ∂P.μ ≤ S.upperBound0 hA.hi z := (hMI.meanIndep_zero z hz).symm.trans_le (S.cond_Y0_le_upperBound0 hA hz) -
ciSup_lowerBound1_le_integral_Y1theorem — Sup-over-support form of lowerBound1_le_integral_Y1.hypothesesconclusion⨆ z : ↑S.support, S.lowerBound1 hA.lo z.val ≤ ∫ ω, S.YofD true ω ∂P.μProof (Lean source)
theorem ciSup_lowerBound1_le_integral_Y1 [IsFiniteMeasure P.μ] (hA : S.BaseAssumptions) (hMI : S.MeanIndep) (hne : S.support.Nonempty) : ⨆ z : ↑S.support, S.lowerBound1 hA.lo z.val ≤ ∫ ω, S.YofD true ω ∂P.μ := by haveI : Nonempty ↑S.support := hne.to_subtype exact ciSup_le (fun z => S.lowerBound1_le_integral_Y1 hA hMI z.property) -
integral_Y1_le_ciInf_upperBound1theorem — Inf-over-support form of integral_Y1_le_upperBound1.hypothesesconclusion∫ ω, S.YofD true ω ∂P.μ ≤ ⨅ z : ↑S.support, S.upperBound1 hA.hi z.valProof (Lean source)
theorem integral_Y1_le_ciInf_upperBound1 [IsFiniteMeasure P.μ] (hA : S.BaseAssumptions) (hMI : S.MeanIndep) (hne : S.support.Nonempty) : ∫ ω, S.YofD true ω ∂P.μ ≤ ⨅ z : ↑S.support, S.upperBound1 hA.hi z.val := by haveI : Nonempty ↑S.support := hne.to_subtype exact le_ciInf (fun z => S.integral_Y1_le_upperBound1 hA hMI z.property) -
ciSup_lowerBound0_le_integral_Y0theorem — Sup-over-support form of lowerBound0_le_integral_Y0.hypothesesconclusion⨆ z : ↑S.support, S.lowerBound0 hA.lo z.val ≤ ∫ ω, S.YofD false ω ∂P.μProof (Lean source)
theorem ciSup_lowerBound0_le_integral_Y0 [IsFiniteMeasure P.μ] (hA : S.BaseAssumptions) (hMI : S.MeanIndep) (hne : S.support.Nonempty) : ⨆ z : ↑S.support, S.lowerBound0 hA.lo z.val ≤ ∫ ω, S.YofD false ω ∂P.μ := by haveI : Nonempty ↑S.support := hne.to_subtype exact ciSup_le (fun z => S.lowerBound0_le_integral_Y0 hA hMI z.property) -
integral_Y0_le_ciInf_upperBound0theorem — Inf-over-support form of integral_Y0_le_upperBound0.hypothesesconclusion∫ ω, S.YofD false ω ∂P.μ ≤ ⨅ z : ↑S.support, S.upperBound0 hA.hi z.valProof (Lean source)
theorem integral_Y0_le_ciInf_upperBound0 [IsFiniteMeasure P.μ] (hA : S.BaseAssumptions) (hMI : S.MeanIndep) (hne : S.support.Nonempty) : ∫ ω, S.YofD false ω ∂P.μ ≤ ⨅ z : ↑S.support, S.upperBound0 hA.hi z.val := by haveI : Nonempty ↑S.support := hne.to_subtype exact le_ciInf (fun z => S.integral_Y0_le_upperBound0 hA hMI z.property)