PO.ID.Partial

Partial identification: bounds on treatment effects when point identification fails — Manski-style worst-case bounds, IV bounds, selection bounds, proxies, and the supporting set-valued machinery.

SupportFunction 17 core · 31 supporting · 5 submodules Support-function representations of convex identified sets and their estimation theory. RandomSet 34 core · 38 supporting · 8 submodules Random-set foundations for partial identification: selections, Aumann expectations, and sharp identified sets. BalkePearl 89 core · 95 supporting · 9 submodules Sharp bounds on the average treatment effect with a binary instrument, binary treatment and binary outcome. CriterionSet 6 core · 8 supporting · 2 submodules Identified sets defined by moment criteria: the criterion-function representation of partial identification. Inference 8 core · 6 supporting · 3 submodules Inference on partially identified parameters: confidence statements for identified sets. Lee 42 core · 19 supporting · 11 submodules Lee's trimming bounds for a treatment effect under sample selection, with a binary treatment and an outcome observed only for selected units. LP 9 core · 2 supporting · 1 submodule The linear-programming representation of bound computations over finite outcome spaces. Manski 39 core · 50 supporting · 9 submodules Worst-case (Manski) bounds on the average treatment effect of a binary treatment with an outcome bounded in [lo, hi] and a discrete instrument, together with their sharpenings under shape restrictions. Proxy 32 core · 21 supporting · 7 submodules Bounds on counterfactual means in the proximal causal inference setting when completeness fails and the bridge functions are not identified, following Ghassami, Shpitser and Tchetgen Tchetgen (arXiv:2304.04374). Sensitivity 121 core · 128 supporting · 1 submodule Sensitivity-analysis bounds for potential outcomes, including marginal-sensitivity-model feasible propensities, calibrated cutoffs, and treatment-effect intervals.

Basic 2 core · 4 supporting This file provides abstract infrastructure for scalar partial-identification sets. ★ identifiedSet_eq_Icc★ identifiedSet_param_Icc

Partial Identification Basics

This file provides abstract infrastructure for scalar partial-identification sets. It builds on the shared identified set—the set of objective values attainable over a feasible parameter set—and proves general criteria for placing that set inside, or identifying it exactly with, a closed real interval.

The results are independent of the potential-outcome framework and are reused by concrete bound constructions such as Balke-Pearl intervals.

theorem identifiedSet_eq_Icc reviewed

Causalean.PartialID

Sharp interval (order-connected form). For an abstract objective function over a feasible parameter set, suppose the objective is bounded below by L on every feasible parameter, bounded above by U on every feasible parameter, the value L itself is attained by some feasible parameter, the value U itself is attained by some feasible parameter, and the set of attainable objective values is order-connected — it contains every real number between any two of its members. Then the identified interval — the set of all objective values attainable over the feasible parameter set — equals the closed interval [L, U] exactly. Order-connectedness is the abstract substitute for "no gaps", supplied concretely by identifiedSet_param_Icc through continuity + connectedness of a parameterization.

Formal statement

hypotheses

α :

Type u_1

α → ℝ

α → Prop

shared

L U :

ℝ

hL :

∀ x

feasible x

then

L ≤ obj x

hU :

∀ x

feasible x

then

obj x ≤ U

hLmem :

L ∈ IdentifiedSet obj feasible

hUmem :

U ∈ IdentifiedSet obj feasible

hconn :

(IdentifiedSet obj feasible).OrdConnected

conclusion

IdentifiedSet obj feasible = Icc L U

Proof (Lean source)

theorem identifiedSet_eq_Icc {L U : ℝ} (hL : ∀ x, feasible x → L ≤ obj x) (hU : ∀ x, feasible x → obj x ≤ U) (hLmem : L ∈ IdentifiedSet obj feasible) (hUmem : U ∈ IdentifiedSet obj feasible) (hconn : (IdentifiedSet obj feasible).OrdConnected) : IdentifiedSet obj feasible = Icc L U := Set.Subset.antisymm (identifiedSet_subset_Icc hL hU) (hconn.out hLmem hUmem)

Causalean.PartialID.identifiedSet_eq_Icc · Causalean/PO/ID/Partial/Basic.lean:64 · uses IdentifiedSet

theorem identifiedSet_param_Icc reviewed

Causalean.PartialID

Mixing-pattern constructor. Suppose the feasible parameter set is exactly the image of the unit interval [0, 1] under a path γ, the objective composed with γ is continuous on [0, 1], the objective value at the path's start equals L, the objective value at the path's end equals U, and the objective stays between L and U at every point along the path. Then the identified set is exactly [L, U]. This is the canonical partial-identification "mixing" shape: an unidentified nuisance ranging over a connected parameter set sweeps the objective continuously across the whole interval between its extreme values.

Formal statement

hypotheses

α :

Type u_1

α → ℝ

α → Prop

ℝ → α

shared

L U :

ℝ

hfeas :

∀ x, feasible x ↔ ∃ t ∈ Icc (0 : ℝ) 1, γ t = x

hcont :

ContinuousOn (fun t => obj (γ t)) (Icc 0 1)

hL :

obj (γ 0) = L

hU :

obj (γ 1) = U

hbound :

∀ t ∈ Icc (0 : ℝ) 1, L ≤ obj (γ t) ∧ obj (γ t) ≤ U

conclusion

IdentifiedSet obj feasible = Icc L U

Proof (Lean source)

theorem identifiedSet_param_Icc {γ : ℝ → α} {L U : ℝ} (hfeas : ∀ x, feasible x ↔ ∃ t ∈ Icc (0 : ℝ) 1, γ t = x) (hcont : ContinuousOn (fun t => obj (γ t)) (Icc 0 1)) (hL : obj (γ 0) = L) (hU : obj (γ 1) = U) (hbound : ∀ t ∈ Icc (0 : ℝ) 1, L ≤ obj (γ t) ∧ obj (γ t) ≤ U) : IdentifiedSet obj feasible = Icc L U := by have himg : IdentifiedSet obj feasible = (fun t => obj (γ t)) '' Icc 0 1 := by ext y simp only [IdentifiedSet, Set.mem_range, Set.mem_image, Subtype.exists] constructor · rintro ⟨x, hx, rfl⟩ obtain ⟨t, ht, rfl⟩ := (hfeas x).1 hx exact ⟨t, ht, rfl⟩ · rintro ⟨t, ht, rfl⟩ exact ⟨γ t, (hfeas (γ t)).2 ⟨t, ht, rfl⟩, rfl⟩ rw [himg] have hord : ((fun t => obj (γ t)) '' Icc 0 1).OrdConnected := ((isPreconnected_Icc).image _ hcont).ordConnected apply Set.Subset.antisymm · rintro _ ⟨t, ht, rfl⟩ exact ⟨(hbound t ht).1, (hbound t ht).2⟩ · exact hord.out ⟨0, by norm_num, hL⟩ ⟨1, by norm_num, hU⟩

Causalean.PartialID.identifiedSet_param_Icc · Causalean/PO/ID/Partial/Basic.lean:83 · uses IdentifiedSet

4 supporting declarations (lemmas, instances)

mem_identifiedSet lemma — A feasible parameter's objective value belongs to the identified set.

hypotheses

α :

Type*
α → ℝ
α → Prop
α

hx :

feasible x

conclusion

obj x ∈ IdentifiedSet obj feasible

Proof (Lean source)

lemma mem_identifiedSet {α : Type*} {obj : α → ℝ} {feasible : α → Prop} {x : α} (hx : feasible x) : obj x ∈ IdentifiedSet obj feasible := ⟨⟨x, hx⟩, rfl⟩

Causalean.PartialID.mem_identifiedSet · Causalean/PO/ID/Partial/Basic.lean:31
mem_Icc_of_sandwich theorem — Sandwich → membership. The literal content of a two-sided bound L ≤ θ ≤ U: the target functional θ lies in the reported interval [L, U]. Names the step that turns the inequality pair every concrete bound produces into the Set.Icc vocabulary.

hypotheses

θ L U :

ℝ

hlo :

L ≤ θ

hhi :

θ ≤ U

conclusion

θ ∈ Icc L U

Proof (Lean source)

theorem mem_Icc_of_sandwich {θ L U : ℝ} (hlo : L ≤ θ) (hhi : θ ≤ U) : θ ∈ Icc L U := ⟨hlo, hhi⟩

Causalean.PartialID.mem_Icc_of_sandwich · Causalean/PO/ID/Partial/Basic.lean:36
mem_Icc_csInf_csSup theorem — Worst/best case over a nuisance. If a set s ⊆ ℝ is bounded, every one of its members lies between sInf s and sSup s. Applied with s = range obj this is the engine form of "the truth is bracketed by the extreme feasible values".

hypotheses

s :

Set ℝ

y :

ℝ

hb :

BddBelow s

ha :

BddAbove s

hy :

y ∈ s

conclusion

y ∈ Icc (sInf s) (sSup s)

Proof (Lean source)

theorem mem_Icc_csInf_csSup {s : Set ℝ} {y : ℝ} (hb : BddBelow s) (ha : BddAbove s) (hy : y ∈ s) : y ∈ Icc (sInf s) (sSup s) := ⟨csInf_le hb hy, le_csSup ha hy⟩

Causalean.PartialID.mem_Icc_csInf_csSup · Causalean/PO/ID/Partial/Basic.lean:44
identifiedSet_subset_Icc theorem — Outer bound. If the objective is uniformly bounded below by L and above by U over the feasible set, the identified set is contained in [L, U].

hypotheses

α :

Type u_1
α → ℝ
α → Prop
shared

L U :

ℝ

hL :

∀ x
if
feasible x
then
L ≤ obj x

hU :

∀ x
if
feasible x
then
obj x ≤ U

conclusion

IdentifiedSet obj feasible ⊆ Icc L U

Proof (Lean source)

theorem identifiedSet_subset_Icc {L U : ℝ} (hL : ∀ x, feasible x → L ≤ obj x) (hU : ∀ x, feasible x → obj x ≤ U) : IdentifiedSet obj feasible ⊆ Icc L U := by rintro _ ⟨x, rfl⟩ exact ⟨hL x.1 x.2, hU x.1 x.2⟩

Causalean.PartialID.identifiedSet_subset_Icc · Causalean/PO/ID/Partial/Basic.lean:55

Frechet 3 core · 1 supporting This file establishes Fréchet–Hoeffding bounds for the joint cumulative distribution function of two real-valued random variables under a fixed joint probability law, and an elementary lower Makarov bound for the cumulat ★ frechet_lower★ makarov_lower_param★ makarov_lower_iSup

Fréchet-Hoeffding and Makarov Bounds

This file establishes Fréchet–Hoeffding bounds for the joint cumulative distribution function of two real-valued random variables under a fixed joint probability law, and an elementary lower Makarov bound for the cumulative distribution function of their difference.

The results apply to an already fixed coupling and do not establish the sharp attainability part of Makarov's theorem, which requires construction of extremal couplings.

theorem frechet_lower reviewed

Causalean.PartialID

Fréchet–Hoeffding lower bound. For a fixed joint law of two real random variables, if Y is measurable, then the joint probability P(X ≤ u, Y ≤ v) is at least the larger of zero and the sum of the two marginal CDF values at u and v minus one: max (P(X ≤ u) + P(Y ≤ v) - 1) 0 ≤ P(X ≤ u, Y ≤ v), for thresholds u and v.

Formal statement

hypotheses

Ω :

Type u_1

shared

P :

Measure Ω

shared

X :

Ω → ℝ

shared

Y :

Ω → ℝ

shared

hY :

Measurable Y

u v :

ℝ

conclusion

max ((P {ω | X ω ≤ u}).toReal + (P {ω | Y ω ≤ v}).toReal - 1) 0

≤ (P {ω | X ω ≤ u ∧ Y ω ≤ v}).toReal

Proof (Lean source)

theorem frechet_lower (hY : Measurable Y) (u v : ℝ) : max ((P {ω | X ω ≤ u}).toReal + (P {ω | Y ω ≤ v}).toReal - 1) 0 ≤ (P {ω | X ω ≤ u ∧ Y ω ≤ v}).toReal := by have hseteq : {ω | X ω ≤ u ∧ Y ω ≤ v} = {ω | X ω ≤ u} ∩ {ω | Y ω ≤ v} := by ext ω; simp [Set.mem_inter_iff] have hB : MeasurableSet {ω : Ω | Y ω ≤ v} := measurableSet_le hY measurable_const refine max_le ?_ ENNReal.toReal_nonneg rw [hseteq] exact prob_inter_ge P hB

Causalean.PartialID.frechet_lower · Causalean/PO/ID/Partial/Frechet.lean:87

theorem makarov_lower_param reviewed

Causalean.PartialID

Makarov lower bound (easy direction), per-threshold form. For a fixed joint law of two real random variables, if Y is measurable, then for every reference point a and threshold s, the CDF of the difference X - Y at s is at least the larger of zero and the gap between the CDF of X at a and the CDF of Y just below a - s: max (P(X ≤ a) - P(Y < a - s)) 0 ≤ P(X - Y ≤ s).

Formal statement

hypotheses

Ω :

Type u_1

shared

P :

Measure Ω

shared

X :

Ω → ℝ

shared

Y :

Ω → ℝ

shared

hY :

Measurable Y

s a :

ℝ

conclusion

max ((P {ω | X ω ≤ a}).toReal - (P {ω | Y ω < a - s}).toReal) 0

≤ (P {ω | X ω - Y ω ≤ s}).toReal

Proof (Lean source)

theorem makarov_lower_param (hY : Measurable Y) (s a : ℝ) : max ((P {ω | X ω ≤ a}).toReal - (P {ω | Y ω < a - s}).toReal) 0 ≤ (P {ω | X ω - Y ω ≤ s}).toReal := by refine max_le ?_ ENNReal.toReal_nonneg -- Set inclusion: {X ≤ a} ∩ {a - s ≤ Y} ⊆ {X - Y ≤ s}. have hsub : {ω : Ω | X ω ≤ a} ∩ {ω : Ω | a - s ≤ Y ω} ⊆ {ω | X ω - Y ω ≤ s} := by intro ω hω have hXa : X ω ≤ a := hω.1 have hYa : a - s ≤ Y ω := hω.2 change X ω - Y ω ≤ s linarith -- {a - s ≤ Y} is the complement of {Y < a - s}, so its measure is 1 - P(Y < a - s). have hBmeas : MeasurableSet {ω : Ω | a - s ≤ Y ω} := measurableSet_le measurable_const hY have hcompl : {ω : Ω | a - s ≤ Y ω} = {ω : Ω | Y ω < a - s}ᶜ := by ext ω; simp [not_lt] have hBval : (P {ω : Ω | a - s ≤ Y ω}).toReal = 1 - (P {ω : Ω | Y ω < a - s}).toReal := by rw [hcompl, prob_compl_eq_one_sub (measurableSet_lt hY measurable_const)] rw [ENNReal.toReal_sub_of_le prob_le_one (by simp)] simp -- Lower bound on the intersection, then monotonicity to the difference event. have hinter : (P {ω | X ω ≤ a}).toReal + (P {ω : Ω | a - s ≤ Y ω}).toReal - 1 ≤ (P ({ω | X ω ≤ a} ∩ {ω : Ω | a - s ≤ Y ω})).toReal := prob_inter_ge P hBmeas have hmono : (P ({ω | X ω ≤ a} ∩ {ω : Ω | a - s ≤ Y ω})).toReal ≤ (P {ω | X ω - Y ω ≤ s}).toReal := ENNReal.toReal_mono (measure_ne_top_of_prob P _) (measure_mono hsub) rw [hBval] at hinter linarith

Causalean.PartialID.makarov_lower_param · Causalean/PO/ID/Partial/Frechet.lean:103

theorem makarov_lower_iSup reviewed

Causalean.PartialID

Makarov lower bound (easy direction), sup-convolution envelope form. For a fixed joint law of two real random variables, if Y is measurable, then for a threshold s, taking the supremum over every reference point of the per-threshold Makarov lower bound still lower-bounds the CDF of the difference X - Y at s.

Formal statement

hypotheses

Ω :

Type u_1

shared

P :

Measure Ω

shared

X :

Ω → ℝ

shared

Y :

Ω → ℝ

shared

hY :

Measurable Y

s :

ℝ

conclusion

⨆ a : ℝ, max ((P {ω | X ω ≤ a}).toReal - (P {ω | Y ω < a - s}).toReal) 0

≤ (P {ω | X ω - Y ω ≤ s}).toReal

Proof (Lean source)

theorem makarov_lower_iSup (hY : Measurable Y) (s : ℝ) : ⨆ a : ℝ, max ((P {ω | X ω ≤ a}).toReal - (P {ω | Y ω < a - s}).toReal) 0 ≤ (P {ω | X ω - Y ω ≤ s}).toReal := ciSup_le (fun a => makarov_lower_param P hY s a)

Causalean.PartialID.makarov_lower_iSup · Causalean/PO/ID/Partial/Frechet.lean:138

1 supporting declaration (lemmas, instances)

frechet_upper theorem — Fréchet–Hoeffding upper bound. For any threshold u for X and any threshold v for Y, the joint probability P(X ≤ u, Y ≤ v) is at most the smaller of the two marginal probabilities P(X ≤ u) and P(Y ≤ v).

hypotheses

Ω :

Type u_1
shared

P :

Measure Ω
shared

X :

Ω → ℝ
shared

Y :

Ω → ℝ
shared

u v :

ℝ

conclusion

(P {ω | X ω ≤ u ∧ Y ω ≤ v}).toReal ≤ min (P {ω | X ω ≤ u}).toReal (P {ω | Y ω ≤ v}).toReal

Proof (Lean source)

theorem frechet_upper (u v : ℝ) : (P {ω | X ω ≤ u ∧ Y ω ≤ v}).toReal ≤ min (P {ω | X ω ≤ u}).toReal (P {ω | Y ω ≤ v}).toReal := by refine le_min ?_ ?_ · exact ENNReal.toReal_mono (measure_ne_top_of_prob P _) (measure_mono (fun ω hω => hω.1)) · exact ENNReal.toReal_mono (measure_ne_top_of_prob P _) (measure_mono (fun ω hω => hω.2))

Causalean.PartialID.frechet_upper · Causalean/PO/ID/Partial/Frechet.lean:71