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 a singleton-stratum data layer for Manski bounds with a measurable instrument, a binary treatment, and a real-valued outcome. ★ POManskiIVSystem★ measurable_YofD
Manski IV Setup
This file defines a singleton-stratum data layer for Manski bounds with a measurable instrument, a binary treatment, and a real-valued outcome. It provides the potential outcomes, factual variables, atomic 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.
For a potential-outcome system and an instrument value space whose singletons are measurable, the Manski singleton-stratum data layer records an instrument, a binary treatment, and a real outcome, with measurable equivalences to their value spaces and pairwise distinct variable labels.
Definition (Lean source)
For a potential-outcome system, a measurable instrument-value space whose singleton values are measurable, and a Manski instrumental-variables system based on them, the instrument variable is its instrument represented as a potential-outcome variable.
Definition (Lean source)
For a potential-outcome system, a measurable instrument-value space whose singleton values are measurable, and a Manski instrumental-variables system based on them, the binary treatment variable is its treatment represented as a potential-outcome variable.
Definition (Lean source)
For a potential-outcome system, a measurable instrument-value space whose singleton values are measurable, and a Manski instrumental-variables system based on them, the real-valued outcome variable is its outcome represented as a potential-outcome variable.
Definition (Lean source)
For a potential-outcome system, a measurable instrument-value space whose singleton values are measurable, a Manski instrumental-variables system based on them, and a binary treatment arm, the potential outcome under that arm assigns each unit its real-valued outcome were treatment set to that arm.
Definition (Lean source)
For a potential-outcome system, a measurable instrument-value space whose singleton values are measurable, and a Manski instrumental-variables system based on them, the observed instrument assigns each unit its realized instrument value.
Definition (Lean source)
For a potential-outcome system, a measurable instrument-value space whose singleton values are measurable, and a Manski instrumental-variables system based on them, the observed binary treatment assigns each unit its realized treatment arm.
Definition (Lean source)
For a potential-outcome system, a measurable instrument-value space whose singleton values are measurable, and a Manski instrumental-variables system based on them, the observed outcome assigns each unit its realized real-valued outcome.
Definition (Lean source)
For a potential-outcome system, a measurable instrument-value space whose singleton values are measurable, a Manski instrumental-variables system based on them, and an instrument value, the corresponding instrument stratum is the set of units whose observed instrument equals that value.
Definition (Lean source)
For a potential-outcome system, a measurable instrument-value space whose singleton values are measurable, a Manski instrumental-variables system based on them, and a binary treatment arm, the corresponding treatment stratum is the set of units whose observed treatment equals that arm.
Definition (Lean source)
For a fixed treatment arm d, the counterfactual outcome Y(d) is measurable.
Formal statement
Proof (Lean source)
For a potential-outcome system, a measurable instrument-value space whose singleton values are measurable, and a Manski instrumental-variables system based on them, the average treatment effect is the population expectation of the potential outcome under treatment minus the potential outcome under control.
Definition (Lean source)
For a potential-outcome system, a measurable instrument-value space whose singleton values are measurable, and a Manski instrumental-variables system based on them, the instrument support is the set of instrument values whose observed-instrument stratum has nonzero probability.
Definition (Lean source)
For a potential-outcome system, a measurable instrument-value space whose singleton values are measurable, a Manski instrumental-variables system based on them, a binary treatment arm, a real-valued outcome bound, and an instrument value, the arm-bound functional is the normalized restricted integral within that instrument stratum of the observed outcome for units on the specified arm and the supplied bound for units on the opposite arm.
Definition (Lean source)
For a potential-outcome system, a measurable instrument-value space whose singleton values are measurable, a Manski instrumental-variables system based on them, a real outcome floor, and an instrument value, the lower bound for the treated potential-outcome mean is the arm-bound functional that uses the floor for untreated units in that instrument stratum.
Definition (Lean source)
For a potential-outcome system, a measurable instrument-value space whose singleton values are measurable, a Manski instrumental-variables system based on them, a real outcome ceiling, and an instrument value, the upper bound for the treated potential-outcome mean is the arm-bound functional that uses the ceiling for untreated units in that instrument stratum.
Definition (Lean source)
For a potential-outcome system, a measurable instrument-value space whose singleton values are measurable, a Manski instrumental-variables system based on them, a real outcome floor, and an instrument value, the lower bound for the control potential-outcome mean is the arm-bound functional that uses the floor for treated units in that instrument stratum.
Definition (Lean source)
For a potential-outcome system, a measurable instrument-value space whose singleton values are measurable, a Manski instrumental-variables system based on them, a real outcome ceiling, and an instrument value, the upper bound for the control potential-outcome mean is the arm-bound functional that uses the ceiling for treated units in that instrument stratum.
Definition (Lean source)
5 supporting declarations (lemmas, instances)
-
measurable_factualZlemma — Factual instrument is measurable.hypothesesconclusionMeasurable S.factualZProof (Lean source)
@[fun_prop] lemma measurable_factualZ : Measurable S.factualZ := S.zVar.measurable_factual -
measurable_factualDlemma — Factual treatment is measurable.hypothesesconclusionMeasurable S.factualDProof (Lean source)
@[fun_prop] lemma measurable_factualD : Measurable S.factualD := S.dVar.measurable_factual -
measurable_factualYlemma — Factual outcome is measurable.hypothesesconclusionMeasurable S.factualYProof (Lean source)
@[fun_prop] lemma measurable_factualY : Measurable S.factualY := S.yVar.measurable_factual -
measurableSet_zEventlemma — Each instrument stratum event is measurable.hypothesesconclusionMeasurableSet (S.zEvent z)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.hypothesesconclusionMeasurableSet (S.dEvent d)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 on measurable singleton instrument strata. ★ bounded
Manski Assumptions
This file states the assumption bundles for Manski bounds on measurable singleton instrument strata. 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.
For a Manski singleton-stratum system, the baseline assumptions bundle records consistency, lower and upper outcome bounds, their ordering, almost-sure boundedness of each arm, and integrability of each arm.
Definition (Lean source)
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
Mean independence requires the treated potential-outcome mean on every positive-mass singleton stratum to equal its population mean and the analogous equality for the control potential outcome.
Definition (Lean source)
Monotone treatment response -- prop:po-iv-mtr, item 1. Y(0) ≤ Y(1) almost surely.
Definition (Lean source)
Monotone treatment selection requires the mean of each potential outcome given control to be no larger than its mean given treatment, as in prop:po-iv-mts.
Definition (Lean source)
Monotone instrumental variable -- prop:po-iv-miv.
Definition (Lean source)
2 supporting declarations (lemmas, instances)
-
integrable_YofDlemma — Binary-folded form of integrable_Y1 / integrable_Y0.hypothesesconclusionIntegrable (S.YofD d) P.μ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.hypothesesconclusionIntegrable S.factualY P.μ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. For a finite instrument value space, they are 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.
For a potential-outcome system, a measurable instrument-value space whose singleton values are measurable, a Manski instrumental-variables system based on them, its base assumptions, including an outcome floor, and an instrument value in a linearly ordered instrument space, the lower monotone-instrument envelope for the treated potential outcome is the supremum of the treated-arm lower bounds over support values no greater than that value.
Definition (Lean source)
For a potential-outcome system, a measurable instrument-value space whose singleton values are measurable, a Manski instrumental-variables system based on them, its base assumptions, including an outcome ceiling, and an instrument value in a linearly ordered instrument space, the upper monotone-instrument envelope for the treated potential outcome is the infimum of the treated-arm upper bounds over support values no smaller than that value.
Definition (Lean source)
For a potential-outcome system, a measurable instrument-value space whose singleton values are measurable, a Manski instrumental-variables system based on them, its base assumptions, including an outcome floor, and an instrument value in a linearly ordered instrument space, the lower monotone-instrument envelope for the control potential outcome is the supremum of the control-arm lower bounds over support values no greater than that value.
Definition (Lean source)
For a potential-outcome system, a measurable instrument-value space whose singleton values are measurable, a Manski instrumental-variables system based on them, its base assumptions, including an outcome ceiling, and an instrument value in a linearly ordered instrument space, the upper monotone-instrument envelope for the control potential outcome is the infimum of the control-arm upper bounds over support values no smaller than that value.
Definition (Lean source)
Finite-value-space specialization of the integrated MIV ATE bounds. For a finite instrument value space, under the baseline Manski assumptions and a monotone instrumental variable, the average treatment effect is sandwiched between the integrated lower- and upper-envelope contrasts.
Formal statement
Proof (Lean source)
8 supporting declarations (lemmas, instances)
-
miv_mLower1_le_cond_Y1theorem — mLower1 z ≤ E[Y(1) | Z = z] for every z ∈ supp Z.hypothesesα :sharedType u_1IsFiniteMeasure P.μhA :S.BaseAssumptionshMIV :S.MIVz :αhz :z ∈ S.supportconclusionletIProof (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 ≤ normalizedRestrictedIntegral 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 ≤ normalizedRestrictedIntegral P.μ (S.zEvent z) (S.YofD true) := by rintro v ⟨u, hu, hule, rfl⟩ have h1 : S.lowerBound1 hA.lo u ≤ normalizedRestrictedIntegral P.μ (S.zEvent u) (S.YofD true) := S.lowerBound1_le_cond_Y1 hA have h2 : normalizedRestrictedIntegral P.μ (S.zEvent u) (S.YofD true) ≤ normalizedRestrictedIntegral 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.hypothesesα :sharedType u_1IsFiniteMeasure P.μhA :S.BaseAssumptionshMIV :S.MIVz :αhz :z ∈ S.supportconclusionletIProof (Lean source)
theorem miv_cond_Y1_le_mUpper1 [IsFiniteMeasure P.μ] (hA : S.BaseAssumptions) (hMIV : S.MIV) {z : α} (hz : z ∈ S.support) : letI := hMIV.inst normalizedRestrictedIntegral 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, normalizedRestrictedIntegral P.μ (S.zEvent z) (S.YofD true) ≤ v := by rintro v ⟨u, hu, hleu, rfl⟩ have h1 : normalizedRestrictedIntegral P.μ (S.zEvent z) (S.YofD true) ≤ normalizedRestrictedIntegral P.μ (S.zEvent u) (S.YofD true) := hMIV.monotone true z u hz hu hleu have h2 : normalizedRestrictedIntegral P.μ (S.zEvent u) (S.YofD true) ≤ S.upperBound1 hA.hi u := S.cond_Y1_le_upperBound1 hA 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.hypothesesα :sharedType u_1IsFiniteMeasure P.μhA :S.BaseAssumptionshMIV :S.MIVz :αhz :z ∈ S.supportconclusionletIProof (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 ≤ normalizedRestrictedIntegral 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 ≤ normalizedRestrictedIntegral P.μ (S.zEvent z) (S.YofD false) := by rintro v ⟨u, hu, hule, rfl⟩ have h1 : S.lowerBound0 hA.lo u ≤ normalizedRestrictedIntegral P.μ (S.zEvent u) (S.YofD false) := S.lowerBound0_le_cond_Y0 hA have h2 : normalizedRestrictedIntegral P.μ (S.zEvent u) (S.YofD false) ≤ normalizedRestrictedIntegral 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.hypothesesα :sharedType u_1IsFiniteMeasure P.μhA :S.BaseAssumptionshMIV :S.MIVz :αhz :z ∈ S.supportconclusionletIProof (Lean source)
theorem miv_cond_Y0_le_mUpper0 [IsFiniteMeasure P.μ] (hA : S.BaseAssumptions) (hMIV : S.MIV) {z : α} (hz : z ∈ S.support) : letI := hMIV.inst normalizedRestrictedIntegral 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, normalizedRestrictedIntegral P.μ (S.zEvent z) (S.YofD false) ≤ v := by rintro v ⟨u, hu, hleu, rfl⟩ have h1 : normalizedRestrictedIntegral P.μ (S.zEvent z) (S.YofD false) ≤ normalizedRestrictedIntegral P.μ (S.zEvent u) (S.YofD false) := hMIV.monotone false z u hz hu hleu have h2 : normalizedRestrictedIntegral P.μ (S.zEvent u) (S.YofD false) ≤ S.upperBound0 hA.hi u := S.cond_Y0_le_upperBound0 hA 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 — For a finite instrument value space, under the baseline Manski assumptions and a monotone instrumental variable, the integrated lower envelope for arm 1 is no larger than the mean of Y(1).hypothesesconclusionletIProof (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 => normalizedRestrictedIntegral 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 — For a finite instrument value space, under the baseline Manski assumptions and a monotone instrumental variable, the mean of Y(1) is no larger than the integrated upper envelope for arm 1.hypothesesconclusionletIProof (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 => normalizedRestrictedIntegral 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 — For a finite instrument value space, under the baseline Manski assumptions and a monotone instrumental variable, the integrated lower envelope for arm 0 is no larger than the mean of Y(0).hypothesesconclusionletIProof (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 => normalizedRestrictedIntegral 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 — For a finite instrument value space, under the baseline Manski assumptions and a monotone instrumental variable, the mean of Y(0) is no larger than the integrated upper envelope for arm 0.hypothesesconclusionletIProof (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 => normalizedRestrictedIntegral 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, for a finite instrument value space, 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.
cor:po-iv-mtr-mts. Under the baseline Manski assumptions, monotone treatment response, Y(0) ≤ Y(1) almost surely, and monotone treatment selection, the average treatment effect is nonnegative and is upper-bounded by the observed treated-control mean contrast.
Formal statement
Proof (Lean source)
Finite-value-space specialization of cor:po-iv-mtr-miv. For a finite instrument value space, under the baseline Manski assumptions, monotone treatment response, Y(0) ≤ Y(1) almost surely, and a monotone instrumental variable, the average treatment effect is nonnegative and is upper-bounded by the integrated monotone-instrument envelope contrast.
Formal statement
Proof (Lean source)
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 normalized restricted-integral bounds for each treatment arm. On a null stratum these quantities use the library's zero convention rather than representing ordinary conditional means.
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.
Under the baseline Manski assumptions, for a treatment arm and a singleton instrument stratum, the normalized restricted integral of the arm's potential outcome is bounded above by the unified upper-envelope functional.
Formal statement
Proof (Lean source)
10 supporting declarations (lemmas, instances)
-
factualY_mul_indD_integrablelemma — factualY · indicator d is integrable.hypothesesα :sharedType u_1hA :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.hypothesesα :sharedType u_1hA :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).hypothesesα :sharedType u_1d :lo :ℝhbound :∀ᵐ ω ∂P.μ, lo ≤ S.YofD d ωconclusion(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.hypothesesα :sharedType u_1d :hi :ℝhbound :∀ᵐ ω ∂P.μ, S.YofD d ω ≤ hiconclusionS.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 — Under the baseline Manski assumptions, for a treatment arm and a singleton instrument stratum, the normalized restricted integral is bounded below by the unified lower-envelope functional.hypothesesconclusionS.boundArm d hA.lo z ≤ normalizedRestrictedIntegral P.μ (S.zEvent z) (S.YofD d)Proof (Lean source)
theorem boundArm_lo_le_cond_YofD [IsFiniteMeasure P.μ] (hA : S.BaseAssumptions) (d : Bool) {z : α} : S.boundArm d hA.lo z ≤ normalizedRestrictedIntegral 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 : normalizedRestrictedIntegral P.μ (S.zEvent z) (fun ω => S.YofD d ω * S.dVar.indicator d ω + hA.lo * S.dVar.indicator (!d) ω) ≤ normalizedRestrictedIntegral 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 = normalizedRestrictedIntegral P.μ (S.zEvent z) (fun ω => S.YofD d ω * S.dVar.indicator d ω + hA.lo * S.dVar.indicator (!d) ω) := by unfold boundArm; rw [hcons] _ ≤ normalizedRestrictedIntegral P.μ (S.zEvent z) (S.YofD d) := hmono -
lowerBound1_le_cond_Y1theorem — Under the baseline Manski assumptions, within an instrument stratum, the treated-arm lower functional does not exceed the treated potential-outcome mean in that stratum.hypothesesconclusionS.lowerBound1 hA.lo z ≤ normalizedRestrictedIntegral P.μ (S.zEvent z) (S.YofD true)Proof (Lean source)
theorem lowerBound1_le_cond_Y1 [IsFiniteMeasure P.μ] (hA : S.BaseAssumptions) {z : α} : S.lowerBound1 hA.lo z ≤ normalizedRestrictedIntegral P.μ (S.zEvent z) (S.YofD true) := S.boundArm_lo_le_cond_YofD hA true -
cond_Y1_le_upperBound1theorem — Under the baseline Manski assumptions, within an instrument stratum, the treated potential-outcome mean in that stratum does not exceed the treated-arm upper functional.hypothesesconclusionnormalizedRestrictedIntegral 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 : α} : normalizedRestrictedIntegral P.μ (S.zEvent z) (S.YofD true) ≤ S.upperBound1 hA.hi z := S.cond_YofD_le_boundArm_hi hA true -
lowerBound0_le_cond_Y0theorem — Under the baseline Manski assumptions, within an instrument stratum, the control-arm lower functional does not exceed the control potential-outcome mean in that stratum.hypothesesconclusionS.lowerBound0 hA.lo z ≤ normalizedRestrictedIntegral P.μ (S.zEvent z) (S.YofD false)Proof (Lean source)
theorem lowerBound0_le_cond_Y0 [IsFiniteMeasure P.μ] (hA : S.BaseAssumptions) {z : α} : S.lowerBound0 hA.lo z ≤ normalizedRestrictedIntegral P.μ (S.zEvent z) (S.YofD false) := S.boundArm_lo_le_cond_YofD hA false -
cond_Y0_le_upperBound0theorem — Under the baseline Manski assumptions, within an instrument stratum, the control potential-outcome mean in that stratum does not exceed the control-arm upper functional.hypothesesconclusionnormalizedRestrictedIntegral 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 : α} : normalizedRestrictedIntegral P.μ (S.zEvent z) (S.YofD false) ≤ S.upperBound0 hA.hi z := S.cond_YofD_le_boundArm_hi hA false
IntervalForm 3 core · 1 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_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 baseline mean-independent-instrument bound, monotone treatment response with monotone treatment selection, and, for finite instrument value spaces, 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.
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 mean-independent-instrument sandwich restated as interval membership.
Formal statement
Proof (Lean source)
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 mean-independent-instrument sandwich restated as interval membership.
Formal statement
Proof (Lean source)
Finite-value-space Set.Icc form of mtr_miv_bounds_ATE. For a finite instrument value space, under the baseline Manski assumptions, monotone treatment response, and a monotone instrumental variable, the average treatment effect lies in the closed interval from zero to the integrated monotone-instrument envelope contrast.
Formal statement
Proof (Lean source)
1 supporting declaration (lemmas, instances)
-
mtr_mts_ATE_mem_Icctheorem — 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 observed treated-control mean contrast.hypothesesα :sharedType u_1hA :S.BaseAssumptionshMTR :S.MTRhMTS :S.MTSconclusionS.ATE ∈ Icc 0 (normalizedRestrictedIntegral P.μ (S.dEvent true) S.factualY - normalizedRestrictedIntegral 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 (normalizedRestrictedIntegral P.μ (S.dEvent true) S.factualY - normalizedRestrictedIntegral 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
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.
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
Proof (Lean source)
5 supporting declarations (lemmas, instances)
-
mtr_E_Y_le_E_Y1theorem — Step 1 of prop:po-iv-mtr: E[Y] ≤ E[Y(1)].hypothesesα :sharedType u_1hA :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].hypothesesα :sharedType u_1hA :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.hypothesesProof (Lean source)
theorem mtr_E_Y1_le_upper (hA : S.BaseAssumptions) : ∫ ω, S.YofD true ω ∂P.μ ≤ (P.μ (S.dEvent true)).toReal * normalizedRestrictedIntegral 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 * normalizedRestrictedIntegral 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)].hypothesesProof (Lean source)
theorem mtr_lower_le_E_Y0 (hA : S.BaseAssumptions) : (P.μ (S.dEvent false)).toReal * normalizedRestrictedIntegral 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 * normalizedRestrictedIntegral 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.hypothesesα :sharedType u_1hA :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
normalizedRestrictedIntegral 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 baseline bounded-outcome inequalities
baseline_lower_le_E_Y1 and baseline_E_Y0_le_upper, the two MTS inequalities
mts_E_Y1_le_condY1 and mts_condY0_le_E_Y0, and the final ATE sandwich
mts_bounds_ATE.
MTS bounds for the ATE. Under the baseline Manski assumptions and monotone treatment selection, the average treatment effect is sandwiched between a probability-weighted range bound and the observed treated-control mean contrast.
Formal statement
Proof (Lean source)
11 supporting declarations (lemmas, instances)
-
compl_dEvent_truelemma — Complement of {D = true} is {D = false} (Bool case-split).hypotheses -
compl_dEvent_falselemma — Complement of {D = false} is {D = true} (Bool case-split).hypotheses -
prob_dEvent_true_add_falselemma — Probability split: P(D=true).toReal + P(D=false).toReal = 1.hypothesesProof (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.hypothesesα :sharedType u_1hA :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 * normalizedRestrictedIntegral P.μ (S.dEvent true) (S.YofD d) + (P.μ (S.dEvent false)).toReal * normalizedRestrictedIntegral 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.hypothesesα :sharedType u_1hA :S.BaseAssumptionsd :ω :P.Ωhω :ω ∈ S.dEvent dconclusionS.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.hypothesesα :sharedType u_1hA :S.BaseAssumptionsd :conclusionnormalizedRestrictedIntegral P.μ (S.dEvent d) (S.YofD d)= normalizedRestrictedIntegral P.μ (S.dEvent d) S.factualYProof (Lean source)
lemma eventCondExp_YofD_eq_factualY (hA : S.BaseAssumptions) (d : Bool) : normalizedRestrictedIntegral P.μ (S.dEvent d) (S.YofD d) = normalizedRestrictedIntegral P.μ (S.dEvent d) S.factualY := eventCondExp_congr_on P.μ (S.measurableSet_dEvent d) fun _ω hω => POVar.cf_eq_factual_on_event hA.consistency S.yVar S.dVar d (Ne.symm S.hDY) hω -
measure_mul_eventCondExp_constlemma — (μ A).toReal * normalizedRestrictedIntegral μ A (fun _ => c) = (μ A).toReal * c. Follows from eventCondExp_mul_measure_toReal with the constant integrand.hypothesesconclusion(P.μ A).toReal * normalizedRestrictedIntegral P.μ A (fun _ : P.Ω => c)= (P.μ A).toReal * cProof (Lean source)
lemma measure_mul_eventCondExp_const (A : Set P.Ω) (c : ℝ) : (P.μ A).toReal * normalizedRestrictedIntegral 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] -
baseline_lower_le_E_Y1theorem — Baseline bounded-outcome lower bound on E[Y(1)]. Under the baseline Manski assumptions, the inequality p · E[Y|D=1] + (1-p) · lo ≤ E[Y(1)].hypothesesProof (Lean source)
theorem baseline_lower_le_E_Y1 (hA : S.BaseAssumptions) : (P.μ (S.dEvent true)).toReal * normalizedRestrictedIntegral 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 : normalizedRestrictedIntegral P.μ (S.dEvent false) (fun _ => hA.lo) ≤ normalizedRestrictedIntegral P.μ (S.dEvent false) (S.YofD true) := by exact eventCondExp_mono_ae P.μ hint_const hint_Y1 (ae_restrict_of_ae hlo_ae) -- `normalizedRestrictedIntegral μ A (fun _ => c) = c` when `μ A ≠ 0`; else both sides are -- `0`. In either case the inequality `c ≤ normalizedRestrictedIntegral μ A f` together -- with `(μ A).toReal * c ≤ (μ A).toReal * normalizedRestrictedIntegral μ 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 * normalizedRestrictedIntegral ... (fun _ => a) = -- ∫ in dEvent false, a = (μ (dEvent false)).toReal * a. have heq_const : (P.μ (S.dEvent false)).toReal * normalizedRestrictedIntegral 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 * normalizedRestrictedIntegral P.μ (S.dEvent false) (fun _ => hA.lo) ≤ (P.μ (S.dEvent false)).toReal * normalizedRestrictedIntegral 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}`: normalizedRestrictedIntegral μ (dEvent true) (YofD true) -- = normalizedRestrictedIntegral μ (dEvent true) factualY. have hcons1 := S.eventCondExp_YofD_eq_factualY hA true -- Combine. rw [hq] at hmul calc p * normalizedRestrictedIntegral P.μ (S.dEvent true) S.factualY + (1 - p) * hA.lo = p * normalizedRestrictedIntegral P.μ (S.dEvent true) (S.YofD true) + (1 - p) * hA.lo := by rw [hcons1] _ ≤ p * normalizedRestrictedIntegral P.μ (S.dEvent true) (S.YofD true) + (1 - p) * normalizedRestrictedIntegral P.μ (S.dEvent false) (S.YofD true) := by linarith _ = ∫ ω, S.YofD true ω ∂P.μ := by rw [hTL, hq] -
mts_E_Y1_le_condY1theorem — Under the baseline Manski assumptions and monotone treatment selection, the treated potential-outcome mean is no larger than the observed treated-cell mean.hypothesesα :sharedType u_1hA :S.BaseAssumptionshMTS :S.MTSconclusionProof (Lean source)
theorem mts_E_Y1_le_condY1 (hA : S.BaseAssumptions) (hMTS : S.MTS) : ∫ ω, S.YofD true ω ∂P.μ ≤ normalizedRestrictedIntegral 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 * normalizedRestrictedIntegral P.μ (S.dEvent true) (S.YofD true) + (1 - p) * normalizedRestrictedIntegral P.μ (S.dEvent false) (S.YofD true) := by rw [hTL, hq] _ ≤ p * normalizedRestrictedIntegral P.μ (S.dEvent true) (S.YofD true) + (1 - p) * normalizedRestrictedIntegral P.μ (S.dEvent true) (S.YofD true) := by have := mul_le_mul_of_nonneg_left hmts hq_nn linarith _ = normalizedRestrictedIntegral P.μ (S.dEvent true) (S.YofD true) := by ring _ = normalizedRestrictedIntegral P.μ (S.dEvent true) S.factualY := hcons1 -
mts_condY0_le_E_Y0theorem — Under the baseline Manski assumptions and monotone treatment selection, the observed control-cell mean is no larger than the control potential-outcome mean.hypothesesα :sharedType u_1hA :S.BaseAssumptionshMTS :S.MTSconclusionProof (Lean source)
theorem mts_condY0_le_E_Y0 (hA : S.BaseAssumptions) (hMTS : S.MTS) : normalizedRestrictedIntegral 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 normalizedRestrictedIntegral P.μ (S.dEvent false) S.factualY = normalizedRestrictedIntegral P.μ (S.dEvent false) (S.YofD false) := hcons0.symm _ = p * normalizedRestrictedIntegral P.μ (S.dEvent false) (S.YofD false) + (1 - p) * normalizedRestrictedIntegral P.μ (S.dEvent false) (S.YofD false) := by ring _ ≤ p * normalizedRestrictedIntegral P.μ (S.dEvent true) (S.YofD false) + (1 - p) * normalizedRestrictedIntegral 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] -
baseline_E_Y0_le_uppertheorem — Baseline bounded-outcome upper bound on E[Y(0)]. Under the baseline Manski assumptions, the inequality E[Y(0)] ≤ p · hi + (1-p) · E[Y|D=0].hypothesesProof (Lean source)
theorem baseline_E_Y0_le_upper (hA : S.BaseAssumptions) : ∫ ω, S.YofD false ω ∂P.μ ≤ (P.μ (S.dEvent true)).toReal * hA.hi + (1 - (P.μ (S.dEvent true)).toReal) * normalizedRestrictedIntegral 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 : normalizedRestrictedIntegral P.μ (S.dEvent true) (S.YofD false) ≤ normalizedRestrictedIntegral 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 * normalizedRestrictedIntegral 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 * normalizedRestrictedIntegral P.μ (S.dEvent true) (S.YofD false) ≤ p * normalizedRestrictedIntegral 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 * normalizedRestrictedIntegral P.μ (S.dEvent true) (S.YofD false) + (1 - p) * normalizedRestrictedIntegral P.μ (S.dEvent false) (S.YofD false) := by rw [hTL, hq] _ ≤ p * hA.hi + (1 - p) * normalizedRestrictedIntegral P.μ (S.dEvent false) (S.YofD false) := by linarith _ = p * hA.hi + (1 - p) * normalizedRestrictedIntegral 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.
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
Proof (Lean source)
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
Proof (Lean source)
8 supporting declarations (lemmas, instances)
-
lowerBound1_le_integral_Y1theorem — Stratum-level lower bound on E[Y(1)].hypothesesα :sharedType u_1IsFiniteMeasure P.μhA :S.BaseAssumptionshMI :S.MeanIndepz :αhz :z ∈ S.supportconclusionS.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).trans_eq (hMI.meanIndep_one z hz) -
integral_Y1_le_upperBound1theorem — Stratum-level upper bound on E[Y(1)].hypothesesα :sharedType u_1IsFiniteMeasure P.μhA :S.BaseAssumptionshMI :S.MeanIndepz :αhz :z ∈ S.supportconclusion∫ ω, 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) -
lowerBound0_le_integral_Y0theorem — Stratum-level lower bound on E[Y(0)].hypothesesα :sharedType u_1IsFiniteMeasure P.μhA :S.BaseAssumptionshMI :S.MeanIndepz :αhz :z ∈ S.supportconclusionS.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).trans_eq (hMI.meanIndep_zero z hz) -
integral_Y0_le_upperBound0theorem — Stratum-level upper bound on E[Y(0)].hypothesesα :sharedType u_1IsFiniteMeasure P.μhA :S.BaseAssumptionshMI :S.MeanIndepz :αhz :z ∈ S.supportconclusion∫ ω, 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) -
ciSup_lowerBound1_le_integral_Y1theorem — Sup-over-support form of lowerBound1_le_integral_Y1.hypothesesα :sharedType u_1IsFiniteMeasure P.μhA :S.BaseAssumptionshMI :S.MeanIndephne :S.support.Nonemptyconclusion⨆ 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.hypothesesα :sharedType u_1IsFiniteMeasure P.μhA :S.BaseAssumptionshMI :S.MeanIndephne :S.support.Nonemptyconclusion∫ ω, 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.hypothesesα :sharedType u_1IsFiniteMeasure P.μhA :S.BaseAssumptionshMI :S.MeanIndephne :S.support.Nonemptyconclusion⨆ 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.hypothesesα :sharedType u_1IsFiniteMeasure P.μhA :S.BaseAssumptionshMI :S.MeanIndephne :S.support.Nonemptyconclusion∫ ω, 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)