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 23 core · 25 supporting · 5 submodules Support-function representations of convex identified sets and their estimation theory. RandomSet 36 core · 36 supporting · 8 submodules Random-set foundations for partial identification: selections, Aumann expectations, and sharp identified sets. BalkePearl 86 core · 92 supporting · 9 submodules This module re-exports the Balke-Pearl partial-identification development for the average treatment effect in a binary instrumental-variable design. 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 This file re-exports the Lee bounds development for treatment effects under sample selection. LP 9 core · 2 supporting · 1 submodule The linear-programming representation of bound computations over finite outcome spaces. Manski 40 core · 49 supporting · 9 submodules This file is the umbrella module for the Manski partial-identification bound family for treatment effects with a discrete instrument. Proxy 32 core · 19 supporting · 7 submodules This file is the umbrella module for proximal partial-identification bounds, bringing together the setup, assumptions, shared helpers, one-proxy bounds, two-proxy bounds, and interval statements. Sensitivity 102 core · 70 supporting · 1 submodule Sensitivity-analysis bounds for potential outcomes, including marginal-sensitivity-model feasible propensities, calibrated cutoffs, and treatment-effect intervals.

Basic 3 core · 4 supporting This file provides abstract infrastructure for scalar partial-identification intervals. ★ IdentifiedInterval★ identifiedInterval_eq_Icc★ identifiedInterval_param_Icc

Partial Identification Basics

This file provides abstract infrastructure for scalar partial-identification intervals. It defines the identified interval as 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.

def IdentifiedInterval reviewed

Causalean.PartialID

For a parameter space, an objective function, and a feasibility condition on its parameter values, the sharp identified interval is the set of all objective values attained by feasible parameters.

Definition (Lean source)

parameters

α :

Type*

obj :

α → ℝ

feasible :

α → Prop

def

IdentifiedInterval obj feasible :

Set ℝ

given by

range (fun x : {x // feasible x} => obj x)

Causalean.PartialID.IdentifiedInterval · Causalean/PO/ID/Partial/Basic.lean:25

theorem identifiedInterval_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 identifiedInterval_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 ∈ IdentifiedInterval obj feasible

hUmem :

U ∈ IdentifiedInterval obj feasible

hconn :

(IdentifiedInterval obj feasible).OrdConnected

conclusion

IdentifiedInterval obj feasible = Icc L U

Proof (Lean source)

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

Causalean.PartialID.identifiedInterval_eq_Icc · Causalean/PO/ID/Partial/Basic.lean:67 · uses IdentifiedInterval

theorem identifiedInterval_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 sharp identified interval 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

IdentifiedInterval obj feasible = Icc L U

Proof (Lean source)

theorem identifiedInterval_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) : IdentifiedInterval obj feasible = Icc L U := by have himg : IdentifiedInterval obj feasible = (fun t => obj (γ t)) '' Icc 0 1 := by ext y simp only [IdentifiedInterval, 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.identifiedInterval_param_Icc · Causalean/PO/ID/Partial/Basic.lean:86 · uses IdentifiedInterval

4 supporting declarations (lemmas, instances)

mem_identifiedInterval lemma — A feasible parameter's objective value belongs to the identified interval.

hypotheses

α :

Type*
α → ℝ
α → Prop
α

hx :

feasible x

conclusion

obj x ∈ IdentifiedInterval obj feasible

Proof (Lean source)

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

Causalean.PartialID.mem_identifiedInterval · Causalean/PO/ID/Partial/Basic.lean:34
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:39
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:47
identifiedInterval_subset_Icc theorem — Outer bound. If the objective is uniformly bounded below by L and above by U over the feasible set, the sharp identified interval 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

IdentifiedInterval obj feasible ⊆ Icc L U

Proof (Lean source)

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

Causalean.PartialID.identifiedInterval_subset_Icc · Causalean/PO/ID/Partial/Basic.lean:58

Frechet 4 core · 0 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_upper★ 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_upper reviewed

Causalean.PartialID

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).

Formal statement

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:67

theorem frechet_lower reviewed

Causalean.PartialID

Fréchet–Hoeffding lower bound. For a fixed joint law of two real random variables X, Y under a probability measure, 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).

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:83

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 X, Y, 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:98

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 X, Y, if Y is measurable, then 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 the given threshold.

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:132