PO.ID.Partial.Inference
Inference on partially identified parameters: confidence statements for identified sets.
Basic 4 core · 4 supporting This file defines the two coverage events used for confidence intervals around an interval-identified scalar parameter: coverage of a fixed parameter value and coverage of the whole identified interval. ★ honest_ci_set_cover★ honest_ci_point_cover
Coverage Vocabulary for Interval-Identified Parameters
This file defines the two coverage events used for confidence intervals around an
interval-identified scalar parameter: coverage of a fixed parameter value and
coverage of the whole identified interval. RandomCoversPoint A B theta is the
sample event that the random interval [A omega, B omega] contains theta;
RandomCoversIcc A B L U is the event that it contains the whole population
identified interval [L, U].
The theorem randomCoversIcc_subset_randomCoversPoint records the elementary
Horowitz-Manski to Imbens-Manski implication: set coverage implies point
coverage for every true value inside [L, U]. The endpoint lemmas
lowerOvershoot_subset_absMiss and upperUndershoot_subset_absMiss, together
with randomCoversIcc_compl_subset, isolate the two one-sided failure events
used by concentration-based intervals. The abstract theorems
honest_ci_set_cover and honest_ci_point_cover then prove honest set and
parameter coverage from upper bounds on those endpoint miss probabilities.
Coverage of the parameter (Imbens–Manski notion). The event that the random interval [A ω, B ω] contains the fixed real value θ.
Definition (Lean source)
Coverage of the identified set (Horowitz–Manski notion). The event that the random interval [A ω, B ω] contains the whole population interval [L, U]. Equivalently A ω ≤ L and U ≤ B ω.
Definition (Lean source)
Abstract honest confidence interval (set coverage). Let lo, hi be the (random) lower/upper endpoint estimators of the population bounds L, U, with lo measurable and hi measurable. Suppose the probability that the widened lower endpoint lo − wL overshoots L is at most δL, and the probability that the widened upper endpoint hi + wU undershoots U is at most δU. Then the widened random interval [lo − wL, hi + wU] covers the entire identified set [L, U] with probability at least 1 − δL − δU.
Formal statement
Proof (Lean source)
Abstract honest confidence interval (parameter coverage). Let lo, hi be random lower/upper endpoint estimators of a population interval [L, U], with lo measurable and hi measurable. Suppose the true value θ lies in [L, U], the probability that the widened lower endpoint lo − wL overshoots L is at most δL, and the probability that the widened upper endpoint hi + wU undershoots U is at most δU. Then the widened random interval [lo − wL, hi + wU] covers θ with probability at least 1 − δL − δU.
Formal statement
Proof (Lean source)
4 supporting declarations (lemmas, instances)
-
randomCoversIcc_subset_randomCoversPointtheorem — Set coverage ⟹ point coverage (the easy half of Imbens–Manski 2004, Lemma 1). If the true value θ lies in the identified set [L, U], then every sample realization whose random interval covers all of [L, U] also covers θ. Consequently a confidence interval that is honest for the *set* is automatically honest for the *parameter* — which is why parameter-coverage intervals can be no larger, and generically strictly smaller.hypothesesconclusionRandomCoversIcc A B L U ⊆ RandomCoversPoint A B θProof (Lean source)
theorem randomCoversIcc_subset_randomCoversPoint (A B : Ω → ℝ) {L U θ : ℝ} (hθ : θ ∈ Icc L U) : RandomCoversIcc A B L U ⊆ RandomCoversPoint A B θ := by rintro ω ⟨hAL, hUB⟩ exact ⟨hAL.trans hθ.1, hθ.2.trans hUB⟩ -
randomCoversIcc_compl_subsettheorem — The complement of the set-coverage event is contained in the union of the two one-sided endpoint-failure events: lower overshoot after widening or upper undershoot after widening.hypotheseslo hi :Ω → ℝL U wL wU :ℝconclusion(RandomCoversIcc (fun ω => lo ω - wL) (fun ω => hi ω + wU) L U)ᶜ ⊆ {ω | L < lo ω - wL} ∪ {ω | hi ω + wU < U}Proof (Lean source)
theorem randomCoversIcc_compl_subset {lo hi : Ω → ℝ} {L U wL wU : ℝ} : (RandomCoversIcc (fun ω => lo ω - wL) (fun ω => hi ω + wU) L U)ᶜ ⊆ {ω | L < lo ω - wL} ∪ {ω | hi ω + wU < U} := by intro ω hω simp only [RandomCoversIcc, Set.mem_compl_iff, Set.mem_setOf_eq, not_and_or, not_le] at hω rcases hω with hL | hU · left exact hL · right exact hU -
lowerOvershoot_subset_absMisstheorem — A lower endpoint overshoot after widening implies the corresponding two-sided absolute-deviation miss.hypotheseslo :Ω → ℝL wL :ℝconclusion{ω | L < lo ω - wL} ⊆ {ω | wL ≤ |lo ω - L|}Proof (Lean source)
theorem lowerOvershoot_subset_absMiss {lo : Ω → ℝ} {L wL : ℝ} : {ω | L < lo ω - wL} ⊆ {ω | wL ≤ |lo ω - L|} := by intro ω hω change L < lo ω - wL at hω have : wL < lo ω - L := by linarith exact (le_of_lt this).trans (le_abs_self _) -
upperUndershoot_subset_absMisstheorem — An upper endpoint undershoot after widening implies the corresponding two-sided absolute-deviation miss.hypotheseshi :Ω → ℝU wU :ℝconclusion{ω | hi ω + wU < U} ⊆ {ω | wU ≤ |hi ω - U|}Proof (Lean source)
theorem upperUndershoot_subset_absMiss {hi : Ω → ℝ} {U wU : ℝ} : {ω | hi ω + wU < U} ⊆ {ω | wU ≤ |hi ω - U|} := by intro ω hω change hi ω + wU < U at hω have : wU < U - hi ω := by linarith refine (le_of_lt this).trans ?_ rw [abs_sub_comm] exact le_abs_self _
ImbensManski 1 core · 2 supporting This file formalizes the lower-protected, upper-far orientation of the asymptotic one-sided critical-value argument for confidence intervals covering a true scalar parameter inside an identified interval. ★ imbensManski_pointwise_coverage
Imbens-Manski Asymptotic Confidence Intervals
This file formalizes the lower-protected, upper-far orientation of the asymptotic one-sided critical-value argument for confidence intervals covering a true scalar parameter inside an identified interval. It relates lower-endpoint convergence and vanishing upper far-tail failure to the Imbens-Manski parameter-coverage refinement.
The helper gaussianMeasure_zero_one_frontier_Iic supplies the continuity-point
fact needed for portmanteau at a closed half-line. The theorem
farEnd_vanishes_of_tendsto_atBot proves that a normalized endpoint statistic
with a standard-normal limit has vanishing probability below a threshold tending
to -infinity. The main theorem imbensManski_pointwise_coverage combines the
lower endpoint's normal limit, a nonnegative lower offset, and the far-endpoint
tail condition to show eventual coverage at least Phi(c) - epsilon for the
one-sided critical value c.
Only this endpoint orientation is formalized here; the symmetric upper-protected statement and uniform-in-distribution refinements are outside this file.
Lower-protected Imbens-Manski pointwise coverage. Let Sl, Su be the normalized lower- and upper-endpoint statistics for an interval-identified scalar parameter, with Sl n measurable for every sample size n, Su n measurable for every sample size n, and Sl converging in distribution to the standard normal law. Fix a one-sided critical value c. Suppose the normalized lower offset aL n, of the target point inside the identified interval, is nonnegative for every n, and the far-endpoint failure probability — that Su n falls below -(c + bU n) — tends to zero as n → ∞. Then for any positive tolerance ε, eventually, as n → ∞, the probability that the Imbens-Manski interval covers the target point is at least Φ(c) − ε, where Φ is the standard-normal distribution function.
Formal statement
Proof (Lean source)
2 supporting declarations (lemmas, instances)
-
gaussianMeasure_zero_one_frontier_Iictheorem — The standard normal gives zero mass to the boundary {c} of the closed half-line (-∞, c]; the continuity-point fact needed to apply portmanteau to a one-sided threshold.Proof (Lean source)
theorem gaussianMeasure_zero_one_frontier_Iic (c : ℝ) : gaussianMeasure 0 1 (frontier (Iic c)) = 0 := by rw [frontier_Iic] exact gaussianMeasure_zero_one_singleton c -
farEnd_vanishes_of_tendsto_atBottheorem — Far-endpoint failure vanishes (the Δ > 0 regime). If the normalized upper-endpoint statistic Sᵤ ⇒ N(0,1) and the (signed) threshold drifts to −∞, then the probability that Sᵤ,ₙ falls below it tends to 0. Concretely tₙ = −(c + bₙ) with bₙ → ∞ (the positive-width regime); the proof bounds the moving tail by a fixed Gaussian tail N(0,1)((-∞,-R]) made arbitrarily small via finite_measure_halfline_tails_small, then transported by portmanteau.hypothesesSu :ℕ → Ω → ℝhSu :∀ n, Measurable (Su n)hSud :Tendsto_dist Su (gaussianMeasure 0 1) μ (fun n => (hSu n).aemeasurable)t :ℕ → ℝProof (Lean source)
theorem farEnd_vanishes_of_tendsto_atBot {Su : ℕ → Ω → ℝ} (hSu : ∀ n, Measurable (Su n)) (hSud : Tendsto_dist Su (gaussianMeasure 0 1) μ (fun n => (hSu n).aemeasurable)) {t : ℕ → ℝ} (ht : Tendsto t atTop atBot) : Tendsto (fun n => (μ {ω | Su n ω < t n}).toReal) atTop (𝓝 0) := by rw [Metric.tendsto_atTop] intro ε hε -- A fixed Gaussian lower tail below level `ε/2`. obtain ⟨R, hRpos, hRiic, _⟩ := gaussian_tail_small_gaussian (v := 1) (ε := ε / 2) (by linarith) -- Portmanteau at the fixed continuity point `-R`: `P(Su,ₙ ≤ -R) → N(0,1)((-∞,-R])`. have hport : Tendsto (fun n => ((μ.map (Su n)) (Iic (-R))).toReal) atTop (𝓝 ((gaussianMeasure 0 1) (Iic (-R))).toReal) := Tendsto_dist.tendsto_measure_of_null_frontier (fun n => (hSu n).aemeasurable) hSud (gaussianMeasure_zero_one_frontier_Iic (-R)) -- Rewrite the pushforward as a probability of `Su,ₙ ≤ -R`. have hmapeq : ∀ n, ((μ.map (Su n)) (Iic (-R))).toReal = (μ {ω | Su n ω ≤ -R}).toReal := by intro n rw [Measure.map_apply_of_aemeasurable (hSu n).aemeasurable measurableSet_Iic]; rfl rw [tendsto_congr hmapeq] at hport -- The Gaussian fixed tail is `≤ ε/2`. have hGle : ((gaussianMeasure 0 1) (Iic (-R))).toReal ≤ ε / 2 := by have hfin : (gaussianMeasure 0 1) (Iic (-R)) ≤ ofReal (ε / 2) := hRiic calc ((gaussianMeasure 0 1) (Iic (-R))).toReal ≤ (ofReal (ε / 2)).toReal := ENNReal.toReal_mono ENNReal.ofReal_ne_top hfin _ = ε / 2 := ENNReal.toReal_ofReal (by linarith) -- Eventually the fixed-tail probability is within `ε/2` of its Gaussian limit, hence `< ε`. have hport_ev : ∀ᶠ n in atTop, (μ {ω | Su n ω ≤ -R}).toReal < ε := by have := (Metric.tendsto_atTop.mp hport) (ε / 2) (by linarith) obtain ⟨N, hN⟩ := this filter_upwards [eventually_ge_atTop N] with n hn have hd := hN n hn rw [Real.dist_eq] at hd have : (μ {ω | Su n ω ≤ -R}).toReal < ((gaussianMeasure 0 1) (Iic (-R))).toReal + ε / 2 := by have := abs_lt.mp hd linarith [this.2] linarith [hGle] -- Eventually the moving threshold is below `-R`. have ht_ev : ∀ᶠ n in atTop, t n ≤ -R := by have := ht.eventually (eventually_le_atBot (-R)) exact this -- Combine: `{Su,ₙ < tₙ} ⊆ {Su,ₙ ≤ -R}` once `tₙ ≤ -R`. rw [eventually_atTop] at hport_ev ht_ev obtain ⟨N1, hN1⟩ := hport_ev obtain ⟨N2, hN2⟩ := ht_ev refine ⟨max N1 N2, fun n hn => ?_⟩ have hprob := hN1 n (le_trans (le_max_left N1 N2) hn) have htn := hN2 n (le_trans (le_max_right N1 N2) hn) have hsub : {ω | Su n ω < t n} ⊆ {ω | Su n ω ≤ -R} := by intro ω hω exact le_of_lt (lt_of_lt_of_le hω htn) have hmono : (μ {ω | Su n ω < t n}).toReal ≤ (μ {ω | Su n ω ≤ -R}).toReal := ENNReal.toReal_mono (measure_ne_top μ _) (measure_mono hsub) rw [Real.dist_eq, sub_zero] have hnn : 0 ≤ (μ {ω | Su n ω < t n}).toReal := ENNReal.toReal_nonneg rw [abs_of_nonneg hnn] linarith [hmono, hprob]
IntervalCI 3 core · 0 supporting This file turns plug-in estimates of lower and upper population bounds into finite-sample confidence intervals for an interval-identified scalar parameter. ★ hoeffding_honest_ci_set_cover★ hoeffding_honest_ci_point_cover★ bernstein_honest_ci_point_cover
Finite-Sample Confidence Intervals for Interval Bounds
This file turns plug-in estimates of lower and upper population bounds into
finite-sample confidence intervals for an interval-identified scalar parameter.
Given observable bounding statistics fL and fU, the lower and upper
population bounds are their means, and the random interval widens the two sample
means by concentration half-widths.
The theorem hoeffding_honest_ci_set_cover proves finite-sample coverage of the
whole identified interval using Hoeffding half-widths. Its corollary
hoeffding_honest_ci_point_cover gives parameter coverage for any
theta0 in the population sandwich. The theorem
bernstein_honest_ci_point_cover gives the corresponding variance-adaptive
Bernstein version. All results are conservative two-endpoint guarantees based on
the abstract union-bound lemma in Inference.Basic; the one-sided asymptotic
Imbens-Manski refinement is developed separately in Inference.ImbensManski.
Finite-sample honest CI for the identified set (Hoeffding). Given lower and upper bounding statistics f_L, f_U that are measurable, each confined a.s. to a known bounded range — f_L ∈ [aL, bL] with aL < bL, f_U ∈ [aU, bU] with aU < bU — at any positive sample size n and any pair of failure probabilities δ_L, δ_U in (0, 1], widening the sample means X̄ₙ(f_L) and X̄ₙ(f_U) outward by the matching Hoeffding half-widths produces a random interval that covers the whole identified interval [∫ f_L dP, ∫ f_U dP] with probability at least 1 − δ_L − δ_U.
Formal statement
Proof (Lean source)
Finite-sample honest CI for the parameter (Hoeffding). The parameter-coverage corollary of hoeffding_honest_ci_set_cover: under the same setup — measurable bounding statistics f_L, f_U a.s. confined to [aL, bL] and [aU, bU] respectively, a positive sample size n, and failure probabilities δ_L, δ_U in (0, 1] — if the true scalar parameter θ₀ lies in the population sandwich [∫ f_L dP, ∫ f_U dP], then the same widened random interval covers θ₀ with probability at least 1 − δ_L − δ_U.
Formal statement
Proof (Lean source)
Finite-sample honest CI for the parameter (Bernstein). Variance-adaptive version: with measurable and integrable bounding statistics f_L, f_U, deviation bounds |f_L − ∫f_L| ≤ cL and |f_U − ∫f_U| ≤ cU holding a.s. for nonnegative constants cL, cU, and variance proxies σL, σU > 0 dominating the respective second central moments, for a positive sample size n and failure probabilities δ_L, δ_U in (0, 1], if the true parameter θ₀ lies in the population sandwich [∫ f_L dP, ∫ f_U dP], then widening the sample means by the corresponding Bernstein half-widths yields a random interval covering θ₀ with probability at least 1 − δ_L − δ_U.