PO.ID.Partial.RandomSet
Random-set foundations for partial identification: selections, Aumann expectations, and sharp identified sets.
Hausdorff 3 core · 2 supporting This file develops the directed and symmetric Hausdorff distances needed for scalar interval-valued identified sets. ★ hausdorffDist_Icc
Hausdorff Distance for Intervals
This file develops the directed and symmetric Hausdorff distances needed for scalar interval-valued identified sets. It proves the explicit formulas for distances between compact real intervals that later connect interval inference to support-function and central-limit-theorem arguments.
Main declarations:
* directedHausdorff and hausdorffDist define one-sided and symmetric
Hausdorff distances in real-valued form.
* infDist_Icc computes the distance from a point to a closed real interval.
* directedHausdorff_Icc gives the directed interval formula.
* hausdorffDist_Icc gives the symmetric endpoint-gap formula
H([a,b],[c,d]) = max |a-c| |b-d|.
In a pseudo-metric space, for a set and a set , the directed, one-sided Hausdorff distance from to is the supremum, over points of , of their distance to ; it is defined to be zero when is empty.
Definition (Lean source)
In a pseudo-metric space, for a set and a set , the symmetric Hausdorff distance is the larger of the directed distance from to and the directed distance from to .
Definition (Lean source)
The geometric keystone (Beresteanu–Molinari eq. (A.1), d = 1). For real numbers a ≤ b and c ≤ d forming two well-ordered closed intervals, the symmetric Hausdorff distance between [a,b] and [c,d] equals the larger of the two endpoint gaps: H([a,b], [c,d]) = max(|a − c|, |b − d|).
Formal statement
Proof (Lean source)
2 supporting declarations (lemmas, instances)
-
infDist_Icctheorem — Distance from a real point to a closed interval. For c ≤ d, infDist x [c,d] = max 0 (max (c − x) (x − d)) — zero inside the interval, and the signed gap to the nearer endpoint outside it.Proof (Lean source)
theorem infDist_Icc {c d : ℝ} (hcd : c ≤ d) (x : ℝ) : infDist x (Icc c d) = max 0 (max (c - x) (x - d)) := by refine le_antisymm ?_ ?_ · -- the clamp point `p = max c (min x d) ∈ [c,d]` realises the upper bound set p : ℝ := max c (min x d) with hp have hpmem : p ∈ Icc c d := by constructor · exact le_max_left _ _ · exact max_le hcd (min_le_right _ _) have hle : infDist x (Icc c d) ≤ dist x p := Metric.infDist_le_dist_of_mem hpmem refine hle.trans ?_ rw [Real.dist_eq] rcases le_total x c with hxc | hcx · -- x ≤ c ⇒ p = c, |x − c| = c − x have hmin : min x d = x := min_eq_left (hxc.trans hcd) have : p = c := by rw [hp, hmin]; exact max_eq_left hxc rw [this, abs_of_nonpos (by linarith)] have : c - x ≤ max (c - x) (x - d) := le_max_left _ _ linarith [le_max_right (0 : ℝ) (max (c - x) (x - d))] · rcases le_total x d with hxd | hdx · -- c ≤ x ≤ d ⇒ p = x, distance 0 have hmin : min x d = x := min_eq_left hxd have : p = x := by rw [hp, hmin]; exact max_eq_right hcx rw [this]; simp only [sub_self, abs_zero] exact le_max_left _ _ · -- x ≥ d ⇒ p = d, |x − d| = x − d have hmin : min x d = d := min_eq_right hdx have : p = d := by rw [hp, hmin]; exact max_eq_right hcd rw [this, abs_of_nonneg (by linarith)] have : x - d ≤ max (c - x) (x - d) := le_max_right _ _ linarith [le_max_right (0 : ℝ) (max (c - x) (x - d))] · -- lower bound: 0, c−x, x−d are each ≤ every point-to-point distance have hne_cd : (Icc c d).Nonempty := ⟨c, ⟨le_rfl, hcd⟩⟩ refine max_le (Metric.infDist_nonneg) (max_le ?_ ?_) · refine (Metric.le_infDist hne_cd).mpr ?_ intro y hy rw [Real.dist_eq] have : c ≤ y := hy.1 rcases le_total x y with h | h · rw [abs_of_nonpos (by linarith)]; linarith · rw [abs_of_nonneg (by linarith)]; linarith · refine (Metric.le_infDist hne_cd).mpr ?_ intro y hy rw [Real.dist_eq] have : y ≤ d := hy.2 rcases le_total x y with h | h · rw [abs_of_nonpos (by linarith)]; linarith · rw [abs_of_nonneg (by linarith)]; linarith -
directedHausdorff_Icctheorem — Directed Hausdorff distance between intervals. dᴴ([a,b], [c,d]) = max 0 (max (c − a) (b − d)) (for a ≤ b, c ≤ d): the worst over-reach of [a,b] beyond [c,d], achieved at the endpoints.hypothesesa b c d :ℝhab :a ≤ bhcd :c ≤ dconclusionProof (Lean source)
theorem directedHausdorff_Icc {a b c d : ℝ} (hab : a ≤ b) (hcd : c ≤ d) : directedHausdorff (Icc a b) (Icc c d) = max 0 (max (c - a) (b - d)) := by unfold directedHausdorff rw [image_infDist_Icc hcd] set g : ℝ → ℝ := fun x => max 0 (max (c - x) (x - d)) with hg have hne : (g '' Icc a b).Nonempty := ⟨g a, a, ⟨le_rfl, hab⟩, rfl⟩ have hga : g a = max 0 (max (c - a) (a - d)) := rfl have hgb : g b = max 0 (max (c - b) (b - d)) := rfl -- upper bound on the image have hub : ∀ z ∈ g '' Icc a b, z ≤ max 0 (max (c - a) (b - d)) := by rintro _ ⟨x, ⟨hax, hxb⟩, rfl⟩ have h1 : c - x ≤ c - a := by linarith have h2 : x - d ≤ b - d := by linarith have hmax : max (c - x) (x - d) ≤ max (c - a) (b - d) := max_le_max h1 h2 exact max_le_max (le_refl 0) hmax refine le_antisymm (csSup_le hne hub) ?_ -- the target is ≤ sSup because it equals max (g a) (g b), both in the image have hbdd : BddAbove (g '' Icc a b) := ⟨_, hub⟩ have hsa : g a ≤ sSup (g '' Icc a b) := le_csSup hbdd ⟨a, ⟨le_rfl, hab⟩, rfl⟩ have hsb : g b ≤ sSup (g '' Icc a b) := le_csSup hbdd ⟨b, ⟨hab, le_rfl⟩, rfl⟩ -- max 0 (max (c−a) (b−d)) ≤ max (g a) (g b) ≤ sSup have h0a : (0 : ℝ) ≤ g a := by rw [hga]; exact le_max_left _ _ have hca : c - a ≤ g a := by rw [hga]; exact le_trans (le_max_left _ _) (le_max_right 0 _) have hdb : b - d ≤ g b := by rw [hgb]; exact le_trans (le_max_right _ _) (le_max_right 0 _) have hmax_gg : max 0 (max (c - a) (b - d)) ≤ max (g a) (g b) := by refine max_le (le_trans h0a (le_max_left _ _)) (max_le ?_ ?_) · exact le_trans hca (le_max_left _ _) · exact le_trans hdb (le_max_right _ _) exact le_trans hmax_gg (max_le hsa hsb)
Interval 6 core · 3 supporting This file treats an interval-valued random set as measurable lower and upper endpoint functions and characterizes functions that belong to the interval at every sample outcome. ★ selectionExpectation_eq_Icc★ sInf_selectionExpectation★ sSup_selectionExpectation
Interval Random Sets and Everywhere-Selection Expectations
This file treats an interval-valued random set as measurable lower and upper endpoint functions and characterizes functions that belong to the interval at every sample outcome. It proves that the integrals of integrable measurable everywhere-selections form the interval between the endpoint expectations. This pointwise interface is stronger than the standard almost-sure selection used to define the Aumann expectation.
Main declarations:
* randomInterval and IsSelection encode interval-valued random sets and
their measurable selections.
* isSelection_iff_exists_param parametrizes every selection as
L + t * (U - L) with measurable t : Ω -> [0,1].
* selectionExpectation_eq_Icc identifies the everywhere-selection
expectation with [∫ L, ∫ U].
* sInf_selectionExpectation and sSup_selectionExpectation recover the sharp
lower and upper endpoints from the set of selection integrals.
For a sample space, a lower endpoint function, and an upper endpoint function, the interval-valued random set assigns to every sample outcome the set of real numbers that are at least its lower-endpoint value and at most its upper-endpoint value.
For a sample space equipped with a measurable structure, a lower endpoint function, an upper endpoint function, and a real-valued function on the sample space, the everywhere measurable-selection condition holds precisely when the function is measurable and at every sample outcome its value lies in the closed interval between the endpoint values.
Definition (Lean source)
For a sample space equipped with a measurable structure, a lower endpoint function, an upper endpoint function, and a measure on the sample space, the everywhere-selection expectation contains exactly the integrals of integrable measurable functions that belong to the endpoint interval at every sample outcome.
Definition (Lean source)
Everywhere-selection expectation equals [∫L, ∫U]. For measurable lower and upper endpoint functions L, U that are integrable and satisfy L pointwise at most U, the integrals of all integrable measurable everywhere-selections of [L, U] form the closed interval [∫L dμ, ∫U dμ]. The forward inclusion is integral monotonicity; the reverse inclusion realizes every intermediate value with a constant mixing weight, so no atomlessness is needed.
Formal statement
Proof (Lean source)
For measurable lower and upper endpoint functions L, U that are integrable and satisfy L pointwise at most U, the sharp lower endpoint of the identified set — the infimum of the everywhere-selection expectation over all measurable selections of the interval-valued random set [L, U] — equals the expectation of the lower endpoint L: sInf (selectionExpectation L U μ) = ∫ L dμ.
Formal statement
Proof (Lean source)
For measurable lower and upper endpoint functions L, U that are integrable and satisfy L pointwise at most U, the sharp upper endpoint of the identified set — the supremum of the everywhere-selection expectation over all measurable selections of the interval-valued random set [L, U] — equals the expectation of the upper endpoint U: sSup (selectionExpectation L U μ) = ∫ U dμ.
Formal statement
Proof (Lean source)
3 supporting declarations (lemmas, instances)
-
isSelection_lefttheorem — A measurable lower endpoint is an everywhere-selection whenever it is pointwise no larger than the upper endpoint, so the interval has a measurable everywhere-selection.hypothesesconclusionIsSelection L U LProof (Lean source)
theorem isSelection_left (hL : Measurable L) (hLU : ∀ ω, L ω ≤ U ω) : IsSelection L U L := ⟨hL, fun ω => ⟨le_rfl, hLU ω⟩⟩ -
isSelection_iff_exists_paramtheorem — Measurable everywhere-selection of an interval random set. Under measurable endpoints with pointwise ordering, a function belongs to [L,U] at every outcome exactly when it has the form L + t·(U − L) for a measurable weight between zero and one.hypothesesconclusionIsSelection L U f↔ ∃ t : Ω → ℝ, Measurable t ∧ (∀ ω, t ω ∈ Icc (0 : ℝ) 1) ∧ ∀ ω, f ω = L ω+ t ω * (U ω - L ω)Proof (Lean source)
theorem isSelection_iff_exists_param (hL : Measurable L) (hU : Measurable U) (hLU : ∀ ω, L ω ≤ U ω) (f : Ω → ℝ) : IsSelection L U f ↔ ∃ t : Ω → ℝ, Measurable t ∧ (∀ ω, t ω ∈ Icc (0 : ℝ) 1) ∧ ∀ ω, f ω = L ω + t ω * (U ω - L ω) := by constructor · rintro ⟨hf, hmem⟩ refine ⟨fun ω => (f ω - L ω) * (U ω - L ω)⁻¹, (hf.sub hL).mul (hU.sub hL).inv, ?_, ?_⟩ · intro ω simp only [Set.mem_Icc, ← div_eq_mul_inv] obtain ⟨hlf, hfu⟩ := hmem ω rcases (hLU ω).lt_or_eq with hlt | heq · have hw : (0 : ℝ) < U ω - L ω := by linarith refine ⟨div_nonneg (by linarith) (le_of_lt hw), ?_⟩ rw [div_le_one hw]; linarith · have hw : U ω - L ω = 0 := by rw [heq]; ring rw [hw, div_zero] exact ⟨le_rfl, zero_le_one⟩ · intro ω obtain ⟨hlf, hfu⟩ := hmem ω rcases (hLU ω).lt_or_eq with hlt | heq · have hw : (U ω - L ω) ≠ 0 := by have : (0 : ℝ) < U ω - L ω := by linarith exact ne_of_gt this field_simp ring · have hwL : L ω = U ω := heq have : f ω = L ω := le_antisymm (by rw [hwL]; exact hfu) hlf rw [this, ← heq]; ring · rintro ⟨t, ht, htmem, hfeq⟩ have hfm : f = fun ω => L ω + t ω * (U ω - L ω) := funext hfeq refine ⟨by rw [hfm]; exact hL.add (ht.mul (hU.sub hL)), ?_⟩ intro ω obtain ⟨ht0, ht1⟩ := htmem ω rw [hfeq ω] constructor · nlinarith [hLU ω] · nlinarith [hLU ω] -
integral_le_integral_of_letheorem — Monotonicity of the endpoint integrals (used to order the reported bounds).hypothesesconclusion(∫ ω, L ω ∂μ) ≤ ∫ ω, U ω ∂μProof (Lean source)
theorem integral_le_integral_of_le (hLint : Integrable L μ) (hUint : Integrable U μ) (hLU : ∀ ω, L ω ≤ U ω) : (∫ ω, L ω ∂μ) ≤ ∫ ω, U ω ∂μ := integral_mono_ae hLint hUint (ae_of_all _ hLU)
IntervalCLT 7 core · 14 supporting This file derives the central limit theorem for the Hausdorff distance between a sample-mean interval and the interval formed by the two population endpoint means. ★ maxAbs_normalizedSum_eq★ interval_data_clt★ interval_data_clt_of_memLp
Scalar Interval-Data Central Limit Theorem
This file derives the central limit theorem for the Hausdorff distance between a sample-mean interval and the interval formed by the two population endpoint means. It reduces the interval statistic to the maximum absolute value of the bivariate endpoint process. This is the symmetric Hausdorff-limit component of Beresteanu–Molinari Theorem 3.2(ii); the file does not formalize Theorem 3.1, almost-sure consistency, or the directed limit.
Main declarations:
* maxAbs, continuous_maxAbs, and measurable_maxAbs define the endpoint
functional for symmetric Hausdorff distance.
* normalizedSum_maxAbs_clt is the abstract continuous-mapping CLT for
maxAbs of a normalized vector sum.
* sampleMean, intervalIFVec, and maxAbs_normalizedSum_eq connect endpoint
sums to sqrt n * hausdorffDist.
* interval_data_clt states the scalar interval-data CLT from explicit CLT
hypotheses.
* interval_data_clt_of_memLp discharges those hypotheses from measurable
endpoints with MemLp 2.
For a pair of real endpoint deviations, the associated two-dimensional Euclidean vector is that pair viewed as a vector in Euclidean space.
For a two-dimensional endpoint-deviation vector, the maximum-absolute-deviation functional is . In the scalar random-set setting, this is the Hausdorff distance between intervals whose lower- and upper-endpoint gaps are the two coordinates.
Definition (Lean source)
For a measurable sample space with sampling measure, a measurable outcome space with outcome measure, an independent and identically distributed sample, a real-valued outcome function, a nonnegative sample size, and a realized sample point, the sample mean is the arithmetic average of the first observed outcome values, with the empty sum divided by zero interpreted by the library's real-number convention.
For a measurable outcome space, a lower-endpoint outcome function, an upper-endpoint outcome function, and a measure on that outcome space, the centered interval-endpoint influence function maps each observation to its lower and upper endpoints less their respective population means, viewed as a two-dimensional Euclidean vector.
Definition (Lean source)
Deterministic Hausdorff bridge. For an i.i.d. sample with interval endpoints yL, yU satisfying the lower endpoint pointwise at most the upper endpoint and both integrable, the max-abs functional applied to the centered endpoint normalised sum equals the scaled Hausdorff distance √n · H(Ȳₙ, E[Y]) between the sample-mean interval Ȳₙ = [ȳ_{nL}, ȳ_{nU}] and the population identified interval E[Y] = [E y_L, E y_U].
Formal statement
Proof (Lean source)
Symmetric Hausdorff-limit component of Beresteanu–Molinari Theorem 3.2(ii). For an i.i.d. sample of interval data Yᵢ = [y_{iL}, y_{iU}] with the lower endpoint pointwise at most the upper endpoint and both endpoints integrable, assume the centered endpoint influence function is measurable, has finite second moment, is centered, and its normalized partial sums and the resulting scaled Hausdorff statistic are almost-everywhere measurable at every sample size. Then the scaled Hausdorff distance between the sample-mean interval Ȳₙ and the population identified interval E[Y] = [E y_L, E y_U] converges in distribution to the max-abs of the bivariate Gaussian limit of the influence function:
Formal statement
Proof (Lean source)
Symmetric component of Theorem 3.2(ii), in a self-contained MemLp 2 form. For an i.i.d. sample of interval data Yᵢ = [y_{iL}, y_{iU}] with the lower endpoint pointwise at most the upper endpoint, measurable endpoints, and finite second moments (MemLp 2) for both endpoints, the scaled Hausdorff distance between the sample-mean interval and the population identified interval E[Y] = [E y_L, E y_U] converges in distribution to the max-abs of the bivariate Gaussian limit of the endpoint influence function. All four multivariate-CLT hypotheses of interval_data_clt are discharged from these clean moment conditions on yL, yU.
Formal statement
Proof (Lean source)
14 supporting declarations (lemmas, instances)
-
continuous_maxAbslemma — The max-absolute-value functional on endpoint deviations is continuous.conclusionContinuous maxAbsProof (Lean source)
@[fun_prop] lemma continuous_maxAbs : Continuous maxAbs := by unfold maxAbs; fun_prop -
measurable_maxAbslemma — The max-absolute-value functional on endpoint deviations is measurable.conclusionMeasurable maxAbsProof (Lean source)
@[fun_prop] lemma measurable_maxAbs : Measurable maxAbs := continuous_maxAbs.measurable -
instIsProbabilityMeasureRealMapEuclideanSpaceFinOfNatNatMaxAbsGaussianLimitinstance — For a measurable sample space equipped with a measure and a two-dimensional vector-valued process on that space that is measurable and has an integrable squared norm under the measure, the law obtained by applying the maximum absolute endpoint-deviation statistic to its Gaussian limit is a probability measure. This follows from taking the measurable pushforward of that Gaussian limit.parametersinstanceinstIsProbabilityMeasureRealMapEuclideanSpaceFinOfNatNatMaxAbsGaussianLimit hψ hvar :given byMeasure.isProbabilityMeasure_map measurable_maxAbs.aemeasurable -
normalizedSum_maxAbs_clttheorem — Abstract continuous-mapping CLT. maxAbs of the vector normalised sum converges in distribution to the pushforward (gaussianLimit ψ).map maxAbs — the law of max(|z_L|, |z_U|) for the bivariate Gaussian limit. Immediate from the multivariate CLT (clt_normalizedSum_vec) and the continuous-mapping theorem (Modes.TendstoInLaw.map_continuous).hypothesesΩ :sharedType u_1X :sharedType u_2S :IIDSample Ω X μ Phmean :∫ x, ψ x ∂P = 0hSum_meas :∀ n, AEMeasurable (IsAsymLinearVec.normalizedSum S ψ (fun m => range m) n) μconclusionModes.TendstoInLaw (fun _ : ℕ => μ) (fun n ω => maxAbs (IsAsymLinearVec.normalizedSum S ψ (fun m => range m) n ω)) atTop ((gaussianLimit hψ hvar).map maxAbs)Proof (Lean source)
theorem normalizedSum_maxAbs_clt (S : IIDSample Ω X μ P) (hmean : ∫ x, ψ x ∂P = 0) (hSum_meas : ∀ n, AEMeasurable (IsAsymLinearVec.normalizedSum S ψ (fun m => range m) n) μ) : Modes.TendstoInLaw (fun _ : ℕ => μ) (fun n ω => maxAbs (IsAsymLinearVec.normalizedSum S ψ (fun m => range m) n ω)) atTop ((gaussianLimit hψ hvar).map maxAbs) := by apply (Tendsto_dist_vec_iff _ _ _ (fun n => continuous_maxAbs.measurable.comp_aemeasurable (hSum_meas n))).2 exact Modes.TendstoInLaw.map_continuous (S.clt_normalizedSum_vec hψ hvar hmean) continuous_maxAbs -
sqrt_inv_centeredlemma — The centered-sum / √n identity (√n)⁻¹·(s − n·c) = √n·(s/n − c), the algebra turning a normalised centered sum into √n × (sample mean − population mean).Proof (Lean source)
lemma sqrt_inv_centered (n : ℕ) (s c : ℝ) : (Real.sqrt n)⁻¹ * (s - n * c) = Real.sqrt n * (s / n - c) := by rcases Nat.eq_zero_or_pos n with hn | hn · subst hn; simp · have hnpos : (0 : ℝ) < n := by exact_mod_cast hn set r := Real.sqrt n with hr have hr0 : r ≠ 0 := ne_of_gt (Real.sqrt_pos.mpr hnpos) have hsq : r * r = (n : ℝ) := Real.mul_self_sqrt (le_of_lt hnpos) rw [← hsq] field_simp -
sampleMean_lelemma — The sample-mean interval is well-ordered (lower ≤ upper) when y_L ≤ y_U.hypothesesΩ :sharedType u_1X :sharedType u_2S :IIDSample Ω X μ PyL yU :X → ℝhLU :∀ z, yL z ≤ yU zn :ℕω :ΩconclusionsampleMean S yL n ω ≤ sampleMean S yU n ωProof (Lean source)
lemma sampleMean_le (S : IIDSample Ω X μ P) (yL yU : X → ℝ) (hLU : ∀ z, yL z ≤ yU z) (n : ℕ) (ω : Ω) : sampleMean S yL n ω ≤ sampleMean S yU n ω := by unfold sampleMean gcongr with i _ exact hLU _ -
norm_sq_intervalIFVeclemma — Pointwise squared norm of the endpoint influence function as the sum of the two squared centered endpoints.hypothesesconclusion‖intervalIFVec yL yU P x‖ ^ 2 = (yL x - ∫ z, yL z ∂P) ^ 2 + (yU x - ∫ z, yU z ∂P) ^ 2Proof (Lean source)
lemma norm_sq_intervalIFVec (yL yU : X → ℝ) (x : X) : ‖intervalIFVec yL yU P x‖ ^ 2 = (yL x - ∫ z, yL z ∂P) ^ 2 + (yU x - ∫ z, yU z ∂P) ^ 2 := by unfold intervalIFVec rw [EuclideanSpace.norm_eq, Real.sq_sqrt (Finset.sum_nonneg fun j _ => sq_nonneg _)] rw [Fin.sum_univ_two] rw [Real.norm_eq_abs, Real.norm_eq_abs, sq_abs, sq_abs, eucl₂_apply, eucl₂_apply] rw [Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val_zero] -
measurable_intervalIFVeclemma — intervalIFVec is measurable from measurability of the two endpoint maps.hypothesesconclusionMeasurable (intervalIFVec yL yU P)Proof (Lean source)
@[fun_prop] lemma measurable_intervalIFVec (yL yU : X → ℝ) (hLmeas : Measurable yL) (hUmeas : Measurable yU) : Measurable (intervalIFVec yL yU P) := by unfold intervalIFVec eucl₂ refine ((EuclideanSpace.equiv (Fin 2) ℝ).symm.continuous.measurable).comp ?_ refine measurable_pi_lambda _ (fun j => ?_) fin_cases j · exact (hLmeas.sub measurable_const) · exact (hUmeas.sub measurable_const) -
intervalIFVec_var_integrablelemma — The variance term ‖ψ‖² ∈ L¹(P), from MemLp 2 of the two endpoints.hypothesesconclusionIntegrable (fun x => ‖intervalIFVec yL yU P x‖ ^ 2) PProof (Lean source)
lemma intervalIFVec_var_integrable (yL yU : X → ℝ) (hLsq : MemLp yL 2 P) (hUsq : MemLp yU 2 P) : Integrable (fun x => ‖intervalIFVec yL yU P x‖ ^ 2) P := by have hL2 : MemLp (fun x => yL x - ∫ z, yL z ∂P) 2 P := hLsq.sub (memLp_const _) have hU2 : MemLp (fun x => yU x - ∫ z, yU z ∂P) 2 P := hUsq.sub (memLp_const _) have hLi : Integrable (fun x => (yL x - ∫ z, yL z ∂P) ^ 2) P := (memLp_two_iff_integrable_sq hL2.aestronglyMeasurable).1 hL2 have hUi : Integrable (fun x => (yU x - ∫ z, yU z ∂P) ^ 2) P := (memLp_two_iff_integrable_sq hU2.aestronglyMeasurable).1 hU2 have heq : (fun x => ‖intervalIFVec yL yU P x‖ ^ 2) = fun x => (yL x - ∫ z, yL z ∂P) ^ 2 + (yU x - ∫ z, yU z ∂P) ^ 2 := by funext x; exact norm_sq_intervalIFVec yL yU x rw [heq] exact hLi.add hUi -
intervalIFVec_integrablelemma — intervalIFVec is Bochner-integrable, from MemLp 2 ⇒ Integrable of the endpoints on a probability measure.hypothesesconclusionIntegrable (intervalIFVec yL yU P) PProof (Lean source)
lemma intervalIFVec_integrable (yL yU : X → ℝ) (hLsq : MemLp yL 2 P) (hUsq : MemLp yU 2 P) : Integrable (intervalIFVec yL yU P) P := by have hLi : Integrable yL P := hLsq.integrable (by norm_num) have hUi : Integrable yU P := hUsq.integrable (by norm_num) unfold intervalIFVec eucl₂ apply (ContinuousLinearEquiv.integrable_comp_iff (EuclideanSpace.equiv (Fin 2) ℝ).symm).2 refine (integrable_pi_iff).2 (fun j => ?_) fin_cases j · exact hLi.sub (integrable_const _) · exact hUi.sub (integrable_const _) -
intervalIFVec_mean_zerolemma — The endpoint influence function is centered: ∫ ψ dP = 0.hypothesesconclusion∫ x, intervalIFVec yL yU P x ∂P = 0Proof (Lean source)
lemma intervalIFVec_mean_zero (yL yU : X → ℝ) (hLsq : MemLp yL 2 P) (hUsq : MemLp yU 2 P) : ∫ x, intervalIFVec yL yU P x ∂P = 0 := by have hLi : Integrable yL P := hLsq.integrable (by norm_num) have hUi : Integrable yU P := hUsq.integrable (by norm_num) change ∫ x, eucl₂ ![yL x - ∫ z, yL z ∂P, yU x - ∫ z, yU z ∂P] ∂P = 0 unfold eucl₂ set g : X → (Fin 2 → ℝ) := fun x => ![yL x - ∫ z, yL z ∂P, yU x - ∫ z, yU z ∂P] with hg rw [ContinuousLinearEquiv.integral_comp_comm (EuclideanSpace.equiv (Fin 2) ℝ).symm g] have hint : Integrable g P := by refine (integrable_pi_iff).2 (fun j => ?_) fin_cases j · exact hLi.sub (integrable_const _) · exact hUi.sub (integrable_const _) have hzero : (∫ x, g x ∂P) = 0 := by funext j have hproj := ContinuousLinearMap.integral_comp_comm (ContinuousLinearMap.proj (R := ℝ) (φ := fun _ : Fin 2 => ℝ) j) hint simp only [ContinuousLinearMap.proj_apply] at hproj rw [Pi.zero_apply, ← hproj] fin_cases j · have heq : (fun x => g x ((fun i => i) (⟨0, by omega⟩ : Fin 2))) = fun x => yL x - ∫ z, yL z ∂P := by funext x; simp only [hg]; rfl rw [heq, integral_sub hLi (integrable_const _), integral_const, probReal_univ, one_smul, sub_self] · have heq : (fun x => g x ((fun i => i) (⟨1, by omega⟩ : Fin 2))) = fun x => yU x - ∫ z, yU z ∂P := by funext x; simp only [hg]; rfl rw [heq, integral_sub hUi (integrable_const _), integral_const, probReal_univ, one_smul, sub_self] rw [hzero, map_zero] -
intervalIFVec_sum_aemeasurablelemma — The vector normalised sum of intervalIFVec is AEMeasurable for each n, from measurability of the endpoints and of the sample coordinates S.Z i.hypothesesΩ :sharedType u_1X :sharedType u_2S :IIDSample Ω X μ PyL yU :X → ℝhLmeas :Measurable yLhUmeas :Measurable yUn :conclusionProof (Lean source)
@[fun_prop] lemma intervalIFVec_sum_aemeasurable (S : IIDSample Ω X μ P) (yL yU : X → ℝ) (hLmeas : Measurable yL) (hUmeas : Measurable yU) : ∀ n, AEMeasurable (IsAsymLinearVec.normalizedSum S (intervalIFVec yL yU P) (fun m => range m) n) μ := by intro n unfold IsAsymLinearVec.normalizedSum refine (aemeasurable ?_) refine (measurable_const_smul _).comp ?_ refine Finset.measurable_sum _ (fun i _ => ?_) exact (measurable_intervalIFVec yL yU hLmeas hUmeas).comp (S.meas i) -
intervalIFVec_hHmeaslemma — The scaled Hausdorff statistic is AEMeasurable for each n. It equals maxAbs ∘ (normalised sum) everywhere by maxAbs_normalizedSum_eq.hypothesesΩ :sharedType u_1X :sharedType u_2S :IIDSample Ω X μ PyL yU :X → ℝhLU :∀ z, yL z ≤ yU zhLmeas :Measurable yLhUmeas :Measurable yUhLint :Integrable yL PhUint :Integrable yU Pn :ℕconclusionAEMeasurable (fun ω => sqrt n * hausdorffDist (Icc (sampleMean S yL n ω) (sampleMean S yU n ω)) (Icc (∫ x, yL x ∂P) (∫ x, yU x ∂P))) μProof (Lean source)
lemma intervalIFVec_hHmeas (S : IIDSample Ω X μ P) (yL yU : X → ℝ) (hLU : ∀ z, yL z ≤ yU z) (hLmeas : Measurable yL) (hUmeas : Measurable yU) (hLint : Integrable yL P) (hUint : Integrable yU P) : ∀ n : ℕ, AEMeasurable (fun ω => sqrt n * hausdorffDist (Icc (sampleMean S yL n ω) (sampleMean S yU n ω)) (Icc (∫ x, yL x ∂P) (∫ x, yU x ∂P))) μ := by intro n refine (measurable_maxAbs.comp_aemeasurable (intervalIFVec_sum_aemeasurable S yL yU hLmeas hUmeas n)).congr ?_ exact Filter.Eventually.of_forall fun ω => maxAbs_normalizedSum_eq S yL yU hLU hLint hUint n ω
SetValued 3 core · 4 supporting This file develops the convex-geometric substrate for random closed sets whose values are nonempty compact convex subsets of an inner-product space. ★ supportFn_minkowskiMean
Set-Valued Random Variables and Minkowski Means
This file develops the convex-geometric substrate for random closed sets whose values are nonempty compact convex subsets of an inner-product space. Its main role in the library is to identify the support function of an empirical Minkowski average with the ordinary average of scalar support functions.
Main declarations:
* IsBody is a local predicate on raw sets asserting nonemptiness, compactness,
and convexity.
* isBody_finsetSum shows that finite Minkowski sums preserve bodies.
* supportFn_finsetSum makes support functions commute with finite Minkowski
sums.
* minkowskiMean and supportFn_minkowskiMean identify the support function
of an empirical Minkowski average with the average of support functions.
The local body predicate requires a raw subset to be nonempty, compact, and convex.
For an inner-product outcome space, an index population, a finite index set, and a family of subsets of that space, the empirical Minkowski average is the Minkowski sum of the selected sets, scaled by the reciprocal of the number of selected indices.
Keystone — Minkowski-mean support bridge. Given a finite index set s all of whose values F i are bodies — nonempty, compact, convex subsets, the support function of the empirical Minkowski average (1/|s|) · ∑ᵢ Fᵢ in a direction d equals the arithmetic average of the individual support functions: s(d, F̄ₙ) = (1/|s|) · ∑ᵢ s(d, Fᵢ). This is the identity that turns the support process into an ordinary sample mean, so the multivariate CLT applies.
Formal statement
Proof (Lean source)
4 supporting declarations (lemmas, instances)
-
bddAbove_inner_imagelemma — On a compact set the linear functional ⟪d, ·⟫ is bounded above.hypothesesconclusionBddAbove ((fun x => ⟪d, x⟫) '' C)Proof (Lean source)
lemma bddAbove_inner_image {C : Set E} (hC : IsCompact C) (d : E) : BddAbove ((fun x => ⟪d, x⟫) '' C) := by obtain ⟨R, hR⟩ := hC.isBounded.subset_closedBall (0 : E) refine ⟨‖d‖ * R, ?_⟩ rintro _ ⟨x, hx, rfl⟩ have hxR : ‖x‖ ≤ R := by simpa [Metric.mem_closedBall, dist_zero_right] using hR hx calc ⟪d, x⟫ ≤ ‖d‖ * ‖x‖ := real_inner_le_norm d x _ ≤ ‖d‖ * R := mul_le_mul_of_nonneg_left hxR (norm_nonneg d) -
bddAbovelemma — The support function of a body is bounded above, hence meaningful.Proof (Lean source)
lemma IsBody.bddAbove {C : Set E} (h : IsBody C) (d : E) : BddAbove ((fun x => ⟪d, x⟫) '' C) := bddAbove_inner_image h.isCompact d -
isBody_finsetSumlemma — A finite Minkowski sum of bodies is a body.hypothesesconclusionIsBody (∑ i ∈ s, F i)Proof (Lean source)
lemma isBody_finsetSum {ι : Type*} (s : Finset ι) (F : ι → Set E) (h : ∀ i ∈ s, IsBody (F i)) : IsBody (∑ i ∈ s, F i) := by classical induction s using Finset.induction with | empty => rw [Finset.sum_empty, ← Set.singleton_zero] exact ⟨Set.singleton_nonempty 0, isCompact_singleton, convex_singleton 0⟩ | @insert a s ha ih => rw [Finset.sum_insert ha] have ha := h a (Finset.mem_insert_self a s) have hr := ih (fun i hi => h i (Finset.mem_insert_of_mem hi)) exact ⟨ha.nonempty.add hr.nonempty, ha.isCompact.add hr.isCompact, ha.convex.add hr.convex⟩ -
supportFn_finsetSumtheorem — Support function commutes with finite Minkowski sums: s(∑ᵢ Fᵢ, d) = ∑ᵢ s(Fᵢ, d).hypothesesProof (Lean source)
theorem supportFn_finsetSum {ι : Type*} (s : Finset ι) (F : ι → Set E) (d : E) (h : ∀ i ∈ s, IsBody (F i)) : supportFn (∑ i ∈ s, F i) d = ∑ i ∈ s, supportFn (F i) d := by classical induction s using Finset.induction with | empty => rw [Finset.sum_empty, Finset.sum_empty, ← Set.singleton_zero, supportFn, Set.image_singleton, inner_zero_right, csSup_singleton] | @insert a s ha ih => rw [Finset.sum_insert ha, Finset.sum_insert ha] have ha := h a (Finset.mem_insert_self a s) have hr := fun i hi => h i (Finset.mem_insert_of_mem hi) have hbody := isBody_finsetSum s F hr rw [supportFn_minkowski ha.nonempty hbody.nonempty (ha.bddAbove d) (hbody.bddAbove d), ih hr]
SupportProcess 4 core · 5 supporting This file proves a finite-dimensional central limit theorem for support-function deviations evaluated on a fixed grid. ★ supportProcess_sup_clt★ setValued_supportProcess_clt
Finite-Direction Support-Process Central Limit Theorem
This file proves a finite-dimensional central limit theorem for support-function deviations evaluated on a fixed grid. Its main limit theorem assumes measurability, a finite second moment, and mean zero for the resulting vector. A separate coordinate lemma connects normalized sums to empirical Minkowski averages for nonempty compact convex values. No theorem here identifies the grid statistic with a Hausdorff distance or requires unit directions.
For a nonempty grid containing directions and a vector of support-process deviations over that grid, the grid supremum statistic is the largest absolute coordinate of the vector.
Definition (Lean source)
For a centered support process ψ on k fixed directions observed via an IID sample S, if ψ is measurable, its squared norm is integrable, ψ is mean zero, E[ψ] = 0, and the normalized partial sums built from S are almost-everywhere measurable at every sample size, then the grid supremum statistic maxAbsK applied to those normalized sums converges in distribution to maxAbsK applied to the Gaussian limit of ψ.
Formal statement
Proof (Lean source)
For an observation space, a nonempty grid containing directions, an inner-product outcome space, a set-valued outcome function, a proposed center set, and a grid of directions, the centered support process maps each observation to the vector whose coordinate in each direction is the support value of its realized set minus the support value of the proposed center set.
For a set-valued random variable F with center EF, observed via an IID sample on a finite grid of directions p, if the centered support process is measurable, it has finite second moment, it is mean zero, E[ψ] = 0, and the normalized partial sums of the process are almost-everywhere measurable at every sample size, then the grid supremum statistic applied to those normalized sums converges in distribution to the corresponding supremum functional of the process's Gaussian limit.
Formal statement
Proof (Lean source)
5 supporting declarations (lemmas, instances)
-
continuous_maxAbsKlemma — The grid supremum statistic is continuous.Proof (Lean source)
-
measurable_maxAbsKlemma — The grid supremum statistic is measurable.Proof (Lean source)
@[fun_prop] lemma measurable_maxAbsK : Measurable (maxAbsK (k := k)) := continuous_maxAbsK.measurable -
instIsProbabilityMeasureRealMapEuclideanSpaceFinMaxAbsKGaussianLimitinstance — For a measurable sample space equipped with a measure, a positive number of grid directions, and a vector-valued process on that space that is measurable and has an integrable squared norm under the measure, the law obtained by applying the grid supremum statistic to its Gaussian limit is a probability measure. This follows from taking the measurable pushforward of that Gaussian limit.parametersinstanceinstIsProbabilityMeasureRealMapEuclideanSpaceFinMaxAbsKGaussianLimit hψ hvar :given byMeasure.isProbabilityMeasure_map measurable_maxAbsK.aemeasurable -
supportProcess_ofLplemma — Each coordinate of the centered support process is the corresponding support deviation.hypothesesX :sharedType u_2k :sharedℕV :sharedType u_3F :X → Set VEF :Set Vp :Fin k → Vx :Xj :Fin kconclusionProof (Lean source)
@[simp] lemma supportProcess_ofLp (F : X → Set V) (EF : Set V) (p : Fin k → V) (x : X) (j : Fin k) : (supportProcess F EF p x).ofLp j = supportFn (F x) (p j) - supportFn EF (p j) := rfl -
supportProcess_normalizedSum_applylemma — Each coordinate of the normalized support-process sum is the rescaled support deviation of the empirical Minkowski average.hypothesesΩ :sharedType u_1X :sharedType u_2k :sharedℕV :sharedType u_3S :IIDSample Ω X μ PF :X → Set VEF :Set Vp :Fin k → Vhbody :∀ x, IsBody (F x)n :ℕω :Ωj :Fin kconclusionIsAsymLinearVec.normalizedSum S (supportProcess F EF p) (fun m => range m) n ω j= sqrt (n : ℝ) * (supportFn (minkowskiMean (range n) (fun i => F (S.Z i ω))) (p j) - supportFn EF (p j))Proof (Lean source)
lemma supportProcess_normalizedSum_apply (S : IIDSample Ω X μ P) (F : X → Set V) (EF : Set V) (p : Fin k → V) (hbody : ∀ x, IsBody (F x)) (n : ℕ) (ω : Ω) (j : Fin k) : IsAsymLinearVec.normalizedSum S (supportProcess F EF p) (fun m => range m) n ω j = sqrt (n : ℝ) * (supportFn (minkowskiMean (range n) (fun i => F (S.Z i ω))) (p j) - supportFn EF (p j)) := by rw [IsAsymLinearVec.normalizedSum] simp only [PiLp.smul_apply, smul_eq_mul, WithLp.ofLp_sum, Finset.sum_apply, supportProcess_ofLp] rw [supportFn_minkowskiMean (range n) (fun i => F (S.Z i ω)) (p j) (fun i _ => hbody (S.Z i ω)), Finset.sum_sub_distrib, Finset.sum_const, Finset.card_range, nsmul_eq_mul] rcases Nat.eq_zero_or_pos n with hn | hn · subst hn; simp · have hnpos : (n : ℝ) ≠ 0 := by exact_mod_cast hn.ne' field_simp rw [Real.sq_sqrt (by positivity : (0 : ℝ) ≤ (n : ℝ))]
Aumann 3 core · 2 supporting This file connects the interval produced by the everywhere-selection expectation with support functions in the two unit directions on the real line. ★ hausdorffDist_Icc_eq_supportFn★ artstein_supportFn_one★ artstein_supportFn_neg_one
The One-Dimensional Everywhere-Selection Support Bridge
This file connects the interval produced by the everywhere-selection
expectation with support functions in the two unit directions on the real line.
The support function of [a,b] at +1 is b, and at -1 is -a; these
endpoint formulas yield scalar support-expectation identities and the interval
Hausdorff identity. The selection interface used here requires membership at
every outcome, not merely almost surely.
Main declarations:
* supportFn_Icc_one and supportFn_Icc_neg_one compute support functions of
real intervals at the two unit directions.
* hausdorffDist_Icc_eq_supportFn rewrites interval Hausdorff distance in the
d = 1 support-function form.
* artstein_supportFn_one and artstein_supportFn_neg_one prove endpoint
support-expectation identities for selectionExpectation.
The d = 1 Hörmander identity (Beresteanu–Molinari eq. (A.1)). For real numbers a ≤ b and c ≤ d forming two well-ordered closed intervals, the Hausdorff distance between the intervals [a,b] and [c,d] equals the largest, over the two unit directions +1 and −1, of the absolute difference between their support functions in that direction.
Formal statement
Proof (Lean source)
Endpoint support identity in direction +1. For measurable lower and upper endpoint functions L, U of an interval-valued random set that are integrable and satisfy L pointwise at most U, the support function of the everywhere-selection expectation of [L, U] in direction +1 equals the expected support function of the realized interval in that direction: s(+1, E[F]) = E[s(+1, F)].
Formal statement
Proof (Lean source)
Endpoint support identity in direction −1. For measurable lower and upper endpoint functions L, U of an interval-valued random set that are integrable and satisfy L pointwise at most U, the support function of the everywhere-selection expectation of [L, U] in direction −1 equals the expected support function of the realized interval in that direction: s(−1, E[F]) = E[s(−1, F)].
Formal statement
Proof (Lean source)
2 supporting declarations (lemmas, instances)
-
supportFn_Icc_onetheorem — Support function of a real interval at +1: the upper endpoint.Proof (Lean source)
theorem supportFn_Icc_one {a b : ℝ} (hab : a ≤ b) : supportFn (Icc a b) (1 : ℝ) = b := by rw [supportFn_eq_iSup_image] simp only [inner_one_left, Set.image_id'] exact csSup_Icc hab -
supportFn_Icc_neg_onetheorem — Support function of a real interval at −1: the negated lower endpoint.Proof (Lean source)
theorem supportFn_Icc_neg_one {a b : ℝ} (hab : a ≤ b) : supportFn (Icc a b) (-1 : ℝ) = -a := by rw [supportFn_eq_iSup_image] simp only [inner_neg_one_left] rw [Set.image_neg_Icc] exact csSup_Icc (by linarith)
GridTest 3 core · 1 supporting This file defines a gridwise supremum statistic for the normalized sum of a centered support process and proves its Gaussian limit and limiting upper-tail probability. ★ gridTestStat_clt
Finite-Grid Support-Process Tail Statistics
This file defines a gridwise supremum statistic for the normalized sum of a centered support process and proves its Gaussian limit and limiting upper-tail probability. The declarations do not identify the statistic with an empirical Minkowski or Hausdorff statistic, and they do not derive the mean-zero condition from a set-equality null.
Main declarations:
* gridTestStat is the finite-grid l^\infty statistic applied to the
normalized centered support-process sum.
* gridTestReject is the rejection region {T_n > c}.
* gridTestStat_clt transports the support-process CLT through the grid
supremum functional.
* gridTest_tail_probability_limit identifies the limiting upper-tail probability at
continuity points of the Gaussian limit law.
For a measurable sample space with sampling measure, a measurable outcome space with outcome measure, a nonempty grid containing directions, an inner-product outcome space, an independent and identically distributed sample, a set-valued outcome function, its proposed center set, and a grid of directions, the finite-grid test statistic, at every nonnegative sample size and sample point, is the largest absolute coordinate of the normalized centered support-process sum.
For a measurable sample space with sampling measure, a measurable outcome space with outcome measure, a nonempty grid containing directions, an inner-product outcome space, an independent and identically distributed sample, a set-valued outcome function, its proposed center set, a grid of directions, a nonnegative sample size, and a real critical value, the rejection region is the set of sample points at which the finite-grid statistic exceeds the critical value.
Definition (Lean source)
For an IID sample and set-valued support process, if the support process is measurable, its squared norm is integrable, its mean is zero, and all normalized sums are almost-everywhere measurable, then the normalized finite-grid support-process statistic converges in distribution to the grid supremum of its Gaussian limit.
Formal statement
Proof (Lean source)
1 supporting declaration (lemmas, instances)
-
gridTest_tail_probability_limittheorem — Limit of the finite-grid upper-tail probability. At any continuity point c of the Gaussian limit law of the grid test statistic — i.e. the limit law assigns zero mass to {c} — the tail (rejection) probability of the normalized finite-grid support-process statistic converges to the corresponding tail mass of the Gaussian limit law: μ (gridTestReject … c) → L(c, ∞).hypothesesΩ :sharedType u_1X :sharedType u_2k :sharedℕV :sharedType u_3hSum_meas :shared∀ (n : ℕ),c :ℝhfront :conclusionTendsto (fun n => μ (gridTestReject S F EF p n c)) atTop (𝓝 (((gaussianLimit hψ hvar).map maxAbsK) (Ioi c)))Proof (Lean source)
theorem gridTest_tail_probability_limit {c : ℝ} (hfront : ((gaussianLimit hψ hvar).map maxAbsK) {c} = 0) : Tendsto (fun n => μ (gridTestReject S F EF p n c)) atTop (𝓝 (((gaussianLimit hψ hvar).map maxAbsK) (Ioi c))) := by have hclt := gridTestStat_clt S F EF p hψ hvar hmean hSum_meas have hclt' := (Tendsto_dist_vec_iff _ _ _ (fun n => measurable_maxAbsK.comp_aemeasurable (hSum_meas n))).1 hclt have hport := MeasureTheory.ProbabilityMeasure.tendsto_measure_of_null_frontier_of_tendsto' hclt' (E := Ioi c) (by rw [frontier_Ioi]; exact hfront) refine hport.congr' ?_ filter_upwards with n -- the per-`n` rejection probability equals the pushforward mass of `Ioi c` change (μ.map (gridTestStat S F EF p n)) (Ioi c) = μ (gridTestReject S F EF p n c) have hmeas : AEMeasurable (gridTestStat S F EF p n) μ := measurable_maxAbsK.comp_aemeasurable (hSum_meas n) rw [Measure.map_apply_of_aemeasurable hmeas measurableSet_Ioi] rfl
IntervalInference 5 core · 7 supporting This file gives the deterministic geometry behind confidence regions for an interval identified set estimated by a sample-mean interval. ★ subset_dilate_iff_directedHausdorff_le★ coverage_event_eq★ directedRegion_coverage_at_fixed_cutoff
Confidence Regions for Scalar Interval Data
This file gives the deterministic geometry behind confidence regions for an interval identified set estimated by a sample-mean interval. It characterizes Minkowski dilations of intervals and relates coverage of the population interval to directed Hausdorff distance and the scalar interval-data central limit theorem.
Main declarations:
* dilate is Minkowski dilation by [-r,r], and dilate_Icc computes it for
closed intervals.
* subset_dilate_iff_directedHausdorff_le is the one-sided coverage geometry
for Beresteanu-Molinari confidence regions.
* subset_dilate_iff_hausdorff_le is the symmetric two-sided analogue.
* coverage_event_eq rewrites the random coverage event as an event on
sqrt n * directedHausdorff.
* dirStat, normalizedSum_dirStat_clt, dirStat_normalizedSum_eq, and
directedRegion_coverage_at_fixed_cutoff provide the directed CLT and the coverage
limit at a fixed population cutoff.
For a set of real numbers and a real radius, the Minkowski dilation is the set of all sums such that belongs to the original set and .
Deterministic directed-coverage characterization. For real numbers with μL ≤ μU and yl ≤ yu forming two closed intervals, and a nonnegative dilation radius r, the population identified interval [μL, μU] lies inside the dilated estimate [yl, yu] ⊕ [−r, r] if and only if the directed Hausdorff distance from [μL,μU] to [yl,yu] is at most r. This is the one-sided coverage event of the Beresteanu–Molinari confidence region.
Formal statement
Proof (Lean source)
Coverage event identity (Beresteanu–Molinari coverage corollary). Fix the population identified interval E[Y] = [μL, μU] with μL ≤ μU, the sample-mean interval Ȳₙ(ω) = [yl(ω), yu(ω)] with yl(ω) ≤ yu(ω) for every ω, a sample size of at least one, and a nonnegative critical value c. With the BM bandwidth r = c/√n, the (one-sided) coverage event {E[Y] ⊆ Uₙ} equals the event {√n · dᴴ(E[Y], Ȳₙ) ≤ c} on the directed Hausdorff statistic. Hence the coverage probability is μ {ω | √n · dᴴ(E[Y], Ȳₙ(ω)) ≤ c}.
Formal statement
Proof (Lean source)
For a two-dimensional endpoint-deviation vector, the directed-Hausdorff functional is . On the centered and normalized endpoint sum, it equals times the directed Hausdorff distance from the population interval to the sample-mean interval.
Definition (Lean source)
Coverage limit at a fixed population cutoff. For an i.i.d. sample with interval endpoints yL, yU satisfying the lower endpoint pointwise at most the upper endpoint and both integrable, assume the centered endpoint influence function is measurable with finite second moment and mean zero, its normalized partial sums are almost-everywhere measurable at every sample size, and fix a nonnegative bandwidth constant c that is a continuity point of the directed-Hausdorff Gaussian limit law. With population identified interval E[Y] = [E y_L, E y_U], sample-mean interval Ȳₙ, and the BM bandwidth c/√n, the coverage probability of the whole identified set converges to the limit-law mass of (-∞, c]:
Formal statement
Proof (Lean source)
7 supporting declarations (lemmas, instances)
-
dilate_Icctheorem — Dilation of an interval. For r ≥ 0, [a,b] ⊕ [−r,r] = [a−r, b+r]: every endpoint is pushed out by the radius.Proof (Lean source)
theorem dilate_Icc {a b r : ℝ} (hab : a ≤ b) (hr : 0 ≤ r) : dilate (Icc a b) r = Icc (a - r) (b + r) := by ext x constructor · rintro ⟨a', ⟨ha1, ha2⟩, t, ht, rfl⟩ rw [abs_le] at ht exact ⟨by linarith [ht.1], by linarith [ht.2]⟩ · rintro ⟨hx1, hx2⟩ -- clamp the chosen point of `[a,b]` to be `max a (min x b)` rcases le_total x a with hxa | hax · -- x ≤ a: pick a' = a, t = x − a ∈ [−r, 0] refine ⟨a, ⟨le_rfl, hab⟩, x - a, ?_, by ring⟩ rw [abs_le]; constructor <;> linarith · rcases le_total x b with hxb | hbx · -- a ≤ x ≤ b: pick a' = x, t = 0 exact ⟨x, ⟨hax, hxb⟩, 0, by simpa using hr, by ring⟩ · -- x ≥ b: pick a' = b, t = x − b ∈ [0, r] refine ⟨b, ⟨hab, le_rfl⟩, x - b, ?_, by ring⟩ rw [abs_le]; constructor <;> linarith -
subset_dilate_iff_hausdorff_letheorem — Symmetric (two-sided) dilation geometry. For real numbers with μL ≤ μU and yl ≤ yu forming two closed intervals, and a nonnegative dilation radius r, each interval lies inside the other's dilation by r if and only if the symmetric Hausdorff distance between [μL,μU] and [yl,yu] is at most r. The mutual containment [μL,μU] ⊆ Uᵧ ∧ [yl,yu] ⊆ Uᵤ is exactly the two-sided event H ≤ r. This elementary equivalence does not define Beresteanu–Molinari's confidence collection or prove Theorem 2.4's characterization of its union.hypothesesμL μU yl yu r :ℝhμ :μL ≤ μUhy :yl ≤ yuhr :0 ≤ rProof (Lean source)
theorem subset_dilate_iff_hausdorff_le {μL μU yl yu r : ℝ} (hμ : μL ≤ μU) (hy : yl ≤ yu) (hr : 0 ≤ r) : (Icc μL μU ⊆ dilate (Icc yl yu) r ∧ Icc yl yu ⊆ dilate (Icc μL μU) r) ↔ hausdorffDist (Icc μL μU) (Icc yl yu) ≤ r := by rw [subset_dilate_iff_directedHausdorff_le hμ hy hr, subset_dilate_iff_directedHausdorff_le hy hμ hr, hausdorffDist, max_le_iff] -
continuous_dirStatlemma — The directed-Hausdorff endpoint functional is continuous.conclusionProof (Lean source)
-
measurable_dirStatlemma — The directed-Hausdorff endpoint functional is measurable.conclusionProof (Lean source)
@[fun_prop] lemma measurable_dirStat : Measurable dirStat := continuous_dirStat.measurable -
instIsProbabilityMeasureRealMapEuclideanSpaceFinOfNatNatDirStatGaussianLimitinstance — For a measurable sample space equipped with a measure and a two-dimensional vector-valued process on that space that is measurable and has an integrable squared norm under the measure, the law obtained by applying the directed-Hausdorff functional to its Gaussian limit is a probability measure. This follows from taking the measurable pushforward of that Gaussian limit.parametersinstanceinstIsProbabilityMeasureRealMapEuclideanSpaceFinOfNatNatDirStatGaussianLimit hψ hvar :given byMeasure.isProbabilityMeasure_map measurable_dirStat.aemeasurable -
normalizedSum_dirStat_clttheorem — Directed continuous-mapping CLT. dirStat of the vector normalised sum converges in distribution to (gaussianLimit ψ).map dirStat.hypothesesΩ :sharedType u_1X :sharedType u_2S :IIDSample Ω X μ Phmean :∫ x, ψ x ∂P = 0hSum_meas :∀ n, AEMeasurable (IsAsymLinearVec.normalizedSum S ψ (fun m => range m) n) μProof (Lean source)
theorem normalizedSum_dirStat_clt (S : IIDSample Ω X μ P) (hmean : ∫ x, ψ x ∂P = 0) (hSum_meas : ∀ n, AEMeasurable (IsAsymLinearVec.normalizedSum S ψ (fun m => range m) n) μ) : Modes.TendstoInLaw (fun _ : ℕ => μ) (fun n ω => dirStat (IsAsymLinearVec.normalizedSum S ψ (fun m => range m) n ω)) atTop ((gaussianLimit hψ hvar).map dirStat) := by apply (Tendsto_dist_vec_iff _ _ _ (fun n => continuous_dirStat.measurable.comp_aemeasurable (hSum_meas n))).2 exact Modes.TendstoInLaw.map_continuous (S.clt_normalizedSum_vec hψ hvar hmean) continuous_dirStat -
dirStat_normalizedSum_eqtheorem — Directed Hausdorff bridge. dirStat of the centered endpoint normalised sum equals √n · dᴴ(E[Y], Ȳₙ).hypothesesΩ :sharedType u_1X :sharedType u_2S :IIDSample Ω X μ PyL yU :X → ℝhLU :∀ z, yL z ≤ yU zhLint :Integrable yL PhUint :Integrable yU Pn :ℕω :Ωconclusion= sqrt n * directedHausdorff (Icc (∫ x, yL x ∂P) (∫ x, yU x ∂P)) (Icc (sampleMean S yL n ω) (sampleMean S yU n ω))Proof (Lean source)
theorem dirStat_normalizedSum_eq (S : IIDSample Ω X μ P) (yL yU : X → ℝ) (hLU : ∀ z, yL z ≤ yU z) (hLint : Integrable yL P) (hUint : Integrable yU P) (n : ℕ) (ω : Ω) : dirStat (IsAsymLinearVec.normalizedSum S (intervalIFVec yL yU P) (fun m => range m) n ω) = sqrt n * directedHausdorff (Icc (∫ x, yL x ∂P) (∫ x, yU x ∂P)) (Icc (sampleMean S yL n ω) (sampleMean S yU n ω)) := by obtain ⟨h0, h1⟩ := nsCoord S yL yU n ω unfold dirStat rw [h0, h1, show -(sqrt n * (sampleMean S yU n ω - ∫ x, yU x ∂P)) = sqrt n * ((∫ x, yU x ∂P) - sampleMean S yU n ω) by ring, ← mul_max_of_nonneg _ _ (Real.sqrt_nonneg (n : ℝ)), show (0 : ℝ) = sqrt n * 0 by ring, ← mul_max_of_nonneg _ _ (Real.sqrt_nonneg (n : ℝ)), directedHausdorff_Icc (integral_mono hLint hUint hLU) (sampleMean_le S yL yU hLU n ω)]