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 its measurable selections. ★ selectionExpectation_eq_Icc★ sInf_selectionExpectation★ sSup_selectionExpectation
Interval Random Sets and Aumann Expectations
This file treats an interval-valued random set as measurable lower and upper endpoint functions and characterizes its measurable selections. It proves that the selection, or Aumann, expectation of the interval random set is the interval whose endpoints are the expectations of the lower and upper endpoint functions.
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 Aumann 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 selection, or Aumann, expectation is the set of real numbers for which there exists a function such that it is an everywhere measurable selection of the endpoint interval, it is integrable under the measure, and its integral under that measure equals the real number.
Definition (Lean source)
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 selection (Aumann) expectation of the interval-valued random set [L, U] — the set of integrals of its integrable measurable selections — equals the closed interval [∫L dμ, ∫U dμ]. The forward inclusion is integral monotonicity; the reverse inclusion realises every intermediate value with a constant mixing weight t ∈ [0,1], 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 selection (Aumann) 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 selection (Aumann) 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 — The lower endpoint is always a selection, so the random set has a measurable 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 selection of an interval random set. A function f is a selection of [L, U] iff f = L + t·(U − L) for some measurable t : Ω → [0,1]. Elementary — no Kuratowski–Ryll-Nardzewski.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 population Aumann expectation interval. ★ 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 population Aumann expectation interval. It reduces the interval statistic to the maximum absolute value of the bivariate endpoint process, allowing the library's multivariate central limit theorem and continuous mapping machinery to apply.
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)
The Hausdorff bridge (Beresteanu–Molinari Theorem 3.2, statistic form). 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)
Beresteanu–Molinari Theorem 3.2 (scalar interval data). 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 and is integrable, 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)
Beresteanu–Molinari Theorem 3.2, 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 (Tendsto_dist_vec.map_continuous).hypothesesΩ :sharedType u_1X :sharedType u_2S :IIDSample Ω X μ P_hψ_int :Integrable ψ Phmean :∫ x, ψ x ∂P = 0hSum_meas :∀ n, AEMeasurable (IsAsymLinearVec.normalizedSum S ψ (fun m => range m) n) μconclusionTendsto_dist_vec (fun n ω => maxAbs (IsAsymLinearVec.normalizedSum S ψ (fun m => range m) n ω)) ((gaussianLimit hψ hvar).map maxAbs) μ (fun n => measurable_maxAbs.comp_aemeasurable (hSum_meas n))Proof (Lean source)
theorem normalizedSum_maxAbs_clt (S : IIDSample Ω X μ P) (_hψ_int : Integrable ψ P) (hmean : ∫ x, ψ x ∂P = 0) (hSum_meas : ∀ n, AEMeasurable (IsAsymLinearVec.normalizedSum S ψ (fun m => range m) n) μ) : Tendsto_dist_vec (fun n ω => maxAbs (IsAsymLinearVec.normalizedSum S ψ (fun m => range m) n ω)) ((gaussianLimit hψ hvar).map maxAbs) μ (fun n => measurable_maxAbs.comp_aemeasurable (hSum_meas n)) := Tendsto_dist_vec.map_continuous continuous_maxAbs hSum_meas (S.clt_normalizedSum_vec hψ hvar hmean) -
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 (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 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. 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 records the nonempty compact convex value type for set-valued random
variables.
* 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.
A body: a nonempty, compact, convex subset of E — the value type 𝒦ₖ(E) of a Beresteanu–Molinari set-valued random variable. Compactness makes supportFn C d well-defined (the linear functional attains its sup); convexity is what lets the support function characterise the set.
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 (mem_insert_self a s) have hr := ih (fun i hi => h i (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 (mem_insert_self a s) have hr := fun i hi => h i (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 the finite-dimensional support-process central limit theorem for random compact convex sets evaluated on a fixed grid of directions. ★ supportProcess_sup_clt★ setValued_supportProcess_clt
Finite-Direction Support-Process Central Limit Theorem
This file proves the finite-dimensional support-process central limit theorem for random compact convex sets evaluated on a fixed grid of directions. It turns support-function deviations into a vector-valued empirical process and applies a continuous mapping theorem to the gridwise sup-norm statistic. This is the honest finite-dimensional projection of Beresteanu--Molinari Theorem A.2; the full continuum Banach-space central limit theorem is deferred.
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 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 interval-valued Aumann expectations 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 Aumann Support Bridge
This file connects interval-valued Aumann expectations 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 turn both the
Hausdorff identity and the Artstein expectation identity into scalar interval
facts.
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 the
one-dimensional Artstein 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)
Artstein identity, d = 1, 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 Aumann (selection) expectation of the random interval [L, U] in the direction +1, namely the upper endpoint, equals the expectation of the support function of the random interval itself in that direction: s(+1, E[F]) = E[s(+1, F)].
Formal statement
Proof (Lean source)
Artstein identity, d = 1, 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 Aumann (selection) expectation of the random interval [L, U] in the direction −1, namely the negated lower endpoint, equals the expectation of the support function of the random interval itself 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 4 core · 0 supporting This file formulates finite-grid specification tests for the Aumann expectation of a set-valued random variable using the normalized centered support process. ★ gridTestStat_clt★ gridTest_asymptotic_level
Finite-Grid Specification Tests for Random Sets
This file formulates finite-grid specification tests for the Aumann expectation of a set-valued random variable using the normalized centered support process. The statistic is the gridwise supremum of that normalized support-process sum, and its asymptotic level follows from the finite-direction support-process central limit theorem.
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_asymptotic_level identifies the limiting rejection 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 test statistic exceeds the critical value.
Definition (Lean source)
The normalized finite-grid support-process statistic converges in distribution to the grid supremum of its Gaussian limit.
Formal statement
Proof (Lean source)
Asymptotic level of the finite-grid tail test. 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, ∞).
Formal statement
Proof (Lean source)
IntervalInference 6 core · 6 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★ subset_dilate_iff_hausdorff_le★ coverage_event_eq★ directedRegion_coverage
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 provide the directed CLT and asymptotic coverage
theorem.
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 .
Coverage characterization (Beresteanu–Molinari Proposition 2.7 core). 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)
Symmetric (two-sided) coverage characterization (Beresteanu–Molinari Uₙ / Theorem 2.4). 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.
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)
Asymptotic coverage of the directed confidence region. 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)
6 supporting declarations (lemmas, instances)
-
dilate_Icctheorem — Dilation of an interval (Beresteanu–Molinari Uₙ). 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 -
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) μconclusionTendsto_dist_vec (fun n ω => dirStat (IsAsymLinearVec.normalizedSum S ψ (fun m => range m) n ω)) ((gaussianLimit hψ hvar).map dirStat) μ (fun n => measurable_dirStat.comp_aemeasurable (hSum_meas 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) μ) : Tendsto_dist_vec (fun n ω => dirStat (IsAsymLinearVec.normalizedSum S ψ (fun m => range m) n ω)) ((gaussianLimit hψ hvar).map dirStat) μ (fun n => measurable_dirStat.comp_aemeasurable (hSum_meas n)) := Tendsto_dist_vec.map_continuous continuous_dirStat hSum_meas (S.clt_normalizedSum_vec hψ hvar hmean) -
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 ω)]