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 41 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 · 15 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 · 45 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

Sharp identified interval: the set of all objective values attainable by a feasible parameter.

Definition (Lean source)

noncomputable def IdentifiedInterval {α : Type*} (obj : α → ℝ) (feasible : α → Prop) : Set ℝ := 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

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:63 · 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

γ :

ℝ → α

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:82 · 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:30
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:35
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:43
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

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

Frechet 4 core · 0 supporting This file proves probability bounds for the joint distribution of two real random variables with a fixed joint law. ★ frechet_upper★ frechet_lower★ makarov_lower_param★ makarov_lower_iSup

Fréchet-Hoeffding and Makarov Bounds

This file proves probability bounds for the joint distribution of two real random variables with a fixed joint law. The Fréchet-Hoeffding theorems frechet_upper and frechet_lower bound the joint CDF value P(X <= u, Y <= v) by the marginal CDF values. The Makarov theorems makarov_lower_param and makarov_lower_iSup give the elementary lower bound on the CDF of the difference X - Y.

These results are the directions that follow from an already fixed coupling of X and Y. The file deliberately does not claim the sharp attainability part of Makarov's theorem, which would require constructing 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

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

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

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

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

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

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