PO.ID.Partial.CriterionSet

Identified sets defined by moment criteria: the criterion-function representation of partial identification.

Basic 3 core · 4 supporting This file defines the basic objects in the Chernozhukov-Hong-Tamer criterion-function approach to partial identification. ★ identifiedSet★ levelSet★ mem_identifiedSet

Criterion Sets

This file defines the basic objects in the Chernozhukov-Hong-Tamer criterion-function approach to partial identification. The identified set is the zero set of a population criterion, and a sample level-set estimator is the set of parameters whose sample criterion value is below a cutoff.

The file contains only definitions and elementary set lemmas; Hausdorff consistency of the level-set estimator is developed separately.

def identifiedSet reviewed

Causalean.PartialID.CriterionSet

A criterion function's identified set is the set of parameters where the population criterion reaches zero.

Definition (Lean source)

def identifiedSet (Q : Θ → ℝ) : Set Θ := {θ | Q θ = 0}

Causalean.PartialID.CriterionSet.identifiedSet · Causalean/PO/ID/Partial/CriterionSet/Basic.lean:23

def levelSet reviewed

Causalean.PartialID.CriterionSet

The level-set estimator keeps the parameters whose sample criterion is no larger than the cutoff.

Definition (Lean source)

def levelSet (Qn : Θ → ℝ) (c : ℝ) : Set Θ := {θ | Qn θ ≤ c}

Causalean.PartialID.CriterionSet.levelSet · Causalean/PO/ID/Partial/CriterionSet/Basic.lean:30

theorem mem_identifiedSet reviewed

Causalean.PartialID.CriterionSet

For a criterion function Q and a candidate parameter θ, θ belongs to the identified set of Q if and only if Q vanishes at θ.

Formal statement

hypotheses

Q :

Θ → ℝ

θ :

conclusion

θ ∈ identifiedSet Q ↔ Q θ = 0

Proof (Lean source)

@[simp] theorem mem_identifiedSet {Q : Θ → ℝ} {θ : Θ} : θ ∈ identifiedSet Q ↔ Q θ = 0 := Iff.rfl

Causalean.PartialID.CriterionSet.mem_identifiedSet · Causalean/PO/ID/Partial/CriterionSet/Basic.lean:37 · uses identifiedSet

4 supporting declarations (lemmas, instances)

mem_levelSet theorem — Membership in a level set is the same as having criterion value below the cutoff.

hypotheses

Qn :

Θ → ℝ

c :

ℝ

θ :

Θ

conclusion

θ ∈ levelSet Qn c ↔ Qn θ ≤ c

Proof (Lean source)

@[simp] theorem mem_levelSet {Qn : Θ → ℝ} {c : ℝ} {θ : Θ} : θ ∈ levelSet Qn c ↔ Qn θ ≤ c := Iff.rfl

Causalean.PartialID.CriterionSet.mem_levelSet · Causalean/PO/ID/Partial/CriterionSet/Basic.lean:43
levelSet_mono theorem — The level set is monotone in the cutoff c.

hypotheses

Qn :

Θ → ℝ

c₁ c₂ :

ℝ

h :

c₁ ≤ c₂

conclusion

levelSet Qn c₁ ⊆ levelSet Qn c₂

Proof (Lean source)

theorem levelSet_mono {Qn : Θ → ℝ} {c₁ c₂ : ℝ} (h : c₁ ≤ c₂) : levelSet Qn c₁ ⊆ levelSet Qn c₂ := fun _ hθ => le_trans hθ h

Causalean.PartialID.CriterionSet.levelSet_mono · Causalean/PO/ID/Partial/CriterionSet/Basic.lean:47
identifiedSet_eq_levelSet_zero_of_nonneg theorem — For a nonnegative criterion, the identified set is the level-0 set of the same criterion (since Q θ = 0 ↔ Q θ ≤ 0 under nonnegativity).

hypotheses

Q :

Θ → ℝ

hQ :

∀ θ, 0 ≤ Q θ

conclusion

identifiedSet Q = levelSet Q 0

Proof (Lean source)

theorem identifiedSet_eq_levelSet_zero_of_nonneg {Q : Θ → ℝ} (hQ : ∀ θ, 0 ≤ Q θ) : identifiedSet Q = levelSet Q 0 := by ext θ simp only [mem_identifiedSet, mem_levelSet] exact ⟨fun h => h.le, fun h => le_antisymm h (hQ θ)⟩

Causalean.PartialID.CriterionSet.identifiedSet_eq_levelSet_zero_of_nonneg · Causalean/PO/ID/Partial/CriterionSet/Basic.lean:51
identifiedSet_subset_levelSet_self theorem — The identified set sits inside any nonnegative-cutoff level set of the same criterion.

hypotheses

Q :

Θ → ℝ

c :

ℝ

hc :

0 ≤ c

conclusion

identifiedSet Q ⊆ levelSet Q c

Proof (Lean source)

theorem identifiedSet_subset_levelSet_self {Q : Θ → ℝ} {c : ℝ} (hc : 0 ≤ c) : identifiedSet Q ⊆ levelSet Q c := fun _ hθ => by rw [mem_levelSet, mem_identifiedSet.mp hθ]; exact hc

Causalean.PartialID.CriterionSet.identifiedSet_subset_levelSet_self · Causalean/PO/ID/Partial/CriterionSet/Basic.lean:59

Consistency 3 core · 4 supporting This file proves deterministic Hausdorff-distance bounds for level sets of sample criterion functions, following the Chernozhukov-Hong-Tamer criterion-set consistency argument. ★ hausdorffDist_levelSet_le★ tendsto_hausdorffDist_levelSet

Hausdorff consistency for criterion-set estimators

This file proves deterministic Hausdorff-distance bounds for level sets of sample criterion functions, following the Chernozhukov-Hong-Tamer criterion-set consistency argument. The population identified set is identifiedSet Q = {theta | Q theta = 0}, the sample estimator is levelSet Qn c = {theta | Qn theta <= c}, and the key identifiability condition is LinearMinorant Q delta, a linear lower bound on criterion values in terms of distance to the identified set.

The main theorem hausdorffDist_levelSet_le states that a uniform sup-norm error bound |Qn - Q| <= epsilon, a cutoff epsilon <= c, and a positive minorant modulus delta imply hausdorffDist (levelSet Qn c) (identifiedSet Q) <= (c + epsilon) / delta. The consistency theorem tendsto_hausdorffDist_levelSet turns this deterministic bound into Hausdorff convergence when both the cutoff and the uniform error vanish. The file also supplies reusable helpers for nonnegativity and subset control of directedHausdorff and hausdorffDist.

def LinearMinorant reviewed

Causalean.PartialID.CriterionSet

A criterion Q satisfies a linear minorant with modulus δ relative to its identified set: δ · d(θ, Θ_I) ≤ Q θ for all θ. This is the Chernozhukov–Hong–Tamer (2007) polynomial-minorant identifiability condition of degree γ = 1 — it forces Q to grow at least linearly away from Θ_I, so a small criterion value pins θ near the identified set.

Definition (Lean source)

def LinearMinorant (Q : Θ → ℝ) (δ : ℝ) : Prop := ∀ θ, δ * infDist θ (identifiedSet Q) ≤ Q θ

Causalean.PartialID.CriterionSet.LinearMinorant · Causalean/PO/ID/Partial/CriterionSet/Consistency.lean:99

theorem hausdorffDist_levelSet_le reviewed

Causalean.PartialID.CriterionSet

Deterministic CHT rate bound. Fix a positive linear-minorant modulus δ, a nonnegative sup-norm error bound ε, and a cutoff c at least ε. If the population criterion Q satisfies a linear minorant of modulus δ relative to its identified set — δ times the distance to the identified set never exceeds Q, and the sample criterion Qn is within ε of Q in sup norm at every point, then the level-set estimator {Qn ≤ c} is within Hausdorff distance (c + ε) / δ of the population identified set {Q = 0}:

Formal statement

hypotheses

Q Qn :

Θ → ℝ

δ c ε :

ℝ

hδ :

0 < δ

hε :

0 ≤ ε

hc :

ε ≤ c

hmin :

LinearMinorant Q δ

hunif :

∀ θ, |Qn θ - Q θ| ≤ ε

conclusion

hausdorffDist (levelSet Qn c) (identifiedSet Q) ≤ (c + ε) / δ

Proof (Lean source)

theorem hausdorffDist_levelSet_le {Q Qn : Θ → ℝ} {δ c ε : ℝ} (hδ : 0 < δ) (hε : 0 ≤ ε) (hc : ε ≤ c) (hmin : LinearMinorant Q δ) (hunif : ∀ θ, |Qn θ - Q θ| ≤ ε) : hausdorffDist (levelSet Qn c) (identifiedSet Q) ≤ (c + ε) / δ := by have hbound : (0 : ℝ) ≤ (c + ε) / δ := div_nonneg (by linarith) hδ.le refine max_le ?_ ?_ · -- points of the estimator are pinned near `Θ_I` by the minorant refine directedHausdorff_le_of_forall hbound (fun θ hθ => ?_) have hQc : Q θ ≤ c + ε := by have hcl := (abs_le.mp (hunif θ)).1 have : Qn θ ≤ c := mem_levelSet.mp hθ linarith rw [le_div_iff₀ hδ] have hm := hmin θ nlinarith [hm, hQc] · -- the identified set sits inside the estimator, so its directed distance is 0 have hsub : identifiedSet Q ⊆ levelSet Qn c := by intro θ hθ rw [mem_levelSet] have hQ0 : Q θ = 0 := mem_identifiedSet.mp hθ have hcu := (abs_le.mp (hunif θ)).2 linarith rw [directedHausdorff_eq_zero_of_subset hsub] exact hbound

Causalean.PartialID.CriterionSet.hausdorffDist_levelSet_le · Causalean/PO/ID/Partial/CriterionSet/Consistency.lean:107 · uses LinearMinorant , identifiedSet , levelSet , hausdorffDist

theorem tendsto_hausdorffDist_levelSet reviewed

Causalean.PartialID.CriterionSet

Hausdorff consistency of the criterion-set estimator. Fix a positive linear-minorant modulus δ such that the population criterion Q satisfies a linear minorant of modulus δ. Suppose each sup-norm error tolerance is nonnegative, each cutoff is at least the corresponding error tolerance, the sample criterion Qn n is within tolerance ε n of Q in sup norm at every sample size n, the cutoffs tend to zero, and the error tolerances tend to zero. Then the Hausdorff distance between the level-set estimator {Qn n ≤ c n} and the population identified set {Q = 0} tends to zero as the sample size grows: H(levelSet Qnₙ cₙ, identifiedSet Q) → 0.

Formal statement

hypotheses

Q :

Θ → ℝ

Qn :

ℕ → Θ → ℝ

δ :

ℝ

c ε :

ℕ → ℝ

hδ :

0 < δ

hmin :

LinearMinorant Q δ

hε :

∀ n, 0 ≤ ε n

hc :

∀ n, ε n ≤ c n

hunif :

∀ n θ, |Qn n θ - Q θ| ≤ ε n

hc0 :

Tendsto c atTop (𝓝 0)

hε0 :

Tendsto ε atTop (𝓝 0)

conclusion

Tendsto (fun n => hausdorffDist (levelSet (Qn n) (c n)) (identifiedSet Q)) atTop (𝓝 0)

Proof (Lean source)

theorem tendsto_hausdorffDist_levelSet {Q : Θ → ℝ} {Qn : ℕ → Θ → ℝ} {δ : ℝ} {c ε : ℕ → ℝ} (hδ : 0 < δ) (hmin : LinearMinorant Q δ) (hε : ∀ n, 0 ≤ ε n) (hc : ∀ n, ε n ≤ c n) (hunif : ∀ n θ, |Qn n θ - Q θ| ≤ ε n) (hc0 : Tendsto c atTop (𝓝 0)) (hε0 : Tendsto ε atTop (𝓝 0)) : Tendsto (fun n => hausdorffDist (levelSet (Qn n) (c n)) (identifiedSet Q)) atTop (𝓝 0) := by refine squeeze_zero (fun n => hausdorffDist_nonneg _ _) (fun n => hausdorffDist_levelSet_le hδ (hε n) (hc n) hmin (hunif n)) ?_ have : Tendsto (fun n => (c n + ε n) / δ) atTop (𝓝 ((0 + 0) / δ)) := ((hc0.add hε0).div_const δ) simpa using this

Causalean.PartialID.CriterionSet.tendsto_hausdorffDist_levelSet · Causalean/PO/ID/Partial/CriterionSet/Consistency.lean:143 · uses LinearMinorant , identifiedSet , levelSet , hausdorffDist

4 supporting declarations (lemmas, instances)

directedHausdorff_nonneg lemma — The directed Hausdorff distance is nonnegative (a sup of nonnegative point-to-set distances).

hypotheses

A B :

Set Θ

conclusion

0 ≤ directedHausdorff A B

Proof (Lean source)

lemma directedHausdorff_nonneg (A B : Set Θ) : 0 ≤ directedHausdorff A B := Real.sSup_nonneg (by rintro _ ⟨a, _, rfl⟩; exact Metric.infDist_nonneg)

Causalean.PartialID.CriterionSet.directedHausdorff_nonneg · Causalean/PO/ID/Partial/CriterionSet/Consistency.lean:74
hausdorffDist_nonneg lemma — The symmetric Hausdorff distance is nonnegative.

hypotheses

A B :

Set Θ

conclusion

0 ≤ hausdorffDist A B

Proof (Lean source)

lemma hausdorffDist_nonneg (A B : Set Θ) : 0 ≤ hausdorffDist A B := le_max_of_le_left (directedHausdorff_nonneg A B)

Causalean.PartialID.CriterionSet.hausdorffDist_nonneg · Causalean/PO/ID/Partial/CriterionSet/Consistency.lean:79
directedHausdorff_le_of_forall lemma — If every point of A is within M of B (and M ≥ 0), the directed Hausdorff distance from A to B is at most M.

hypotheses

A B :

Set Θ

M :

ℝ

hM :

0 ≤ M

h :

∀ a ∈ A, infDist a B ≤ M

conclusion

directedHausdorff A B ≤ M

Proof (Lean source)

lemma directedHausdorff_le_of_forall {A B : Set Θ} {M : ℝ} (hM : 0 ≤ M) (h : ∀ a ∈ A, infDist a B ≤ M) : directedHausdorff A B ≤ M := Real.sSup_le (by rintro _ ⟨a, ha, rfl⟩; exact h a ha) hM

Causalean.PartialID.CriterionSet.directedHausdorff_le_of_forall · Causalean/PO/ID/Partial/CriterionSet/Consistency.lean:83
directedHausdorff_eq_zero_of_subset lemma — If A ⊆ B then the directed Hausdorff distance from A to B is 0.

hypotheses

A B :

Set Θ

h :

A ⊆ B

conclusion

directedHausdorff A B = 0

Proof (Lean source)

lemma directedHausdorff_eq_zero_of_subset {A B : Set Θ} (h : A ⊆ B) : directedHausdorff A B = 0 := le_antisymm (directedHausdorff_le_of_forall le_rfl (fun _ ha => le_of_eq (Metric.infDist_zero_of_mem (h ha)))) (directedHausdorff_nonneg A B)

Causalean.PartialID.CriterionSet.directedHausdorff_eq_zero_of_subset · Causalean/PO/ID/Partial/CriterionSet/Consistency.lean:89

PO.ID.Partial.Criterion­Set

Criterion Sets

Hausdorff consistency for criterion-set estimators

PO.ID.Partial.CriterionSet