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|.
Directed (one-sided) Hausdorff distance from A to B: the supremum over points of A of their distance to B. Real-valued (via Metric.infDist); on the empty image sSup returns 0.
Definition (Lean source)
Symmetric Hausdorff distance H(A,B) = max(dᴴ(A,B), dᴴ(B,A)).
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.
The interval-valued random closed set ω ↦ [L ω, U ω].
Definition (Lean source)
f is a measurable everywhere-selection of the interval random set [L, U]: it is measurable and L ω ≤ f ω ≤ U ω for every ω.
Definition (Lean source)
The selection (Aumann) expectation of the interval random set [L, U]: the set of integrals of integrable measurable selections.
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.Proof (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.
A pair of real endpoint deviations is viewed as a two-dimensional Euclidean vector.
Definition (Lean source)
The max-abs functional w ↦ max(|w₀|, |w₁|) on ℝ². In the d = 1 random-set picture this is the Hausdorff distance between the intervals whose endpoint gaps are w₀ and w₁ (cf. hausdorffDist_Icc).
Definition (Lean source)
Sample mean of y over the first n draws of the i.i.d. sample.
The centered interval-endpoint influence function ψ(z) = (y_L(z) − E y_L, y_U(z) − E y_U), valued in ℝ². Its vector normalised sum is the centered-and-scaled endpoint pair √n((ȳ_{nL}, ȳ_{nU}) − (E y_L, E y_U)).
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)
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)
lemma measurable_maxAbs : Measurable maxAbs := continuous_maxAbs.measurable -
instIsProbabilityMeasureRealMapEuclideanSpaceFinOfNatNatMaxAbsGaussianLimitinstance — The limit law of the Hausdorff statistic is a probability measure (pushforward of the Gaussian limit by the continuous maxAbs).instance : IsProbabilityMeasure ((gaussianLimit hψ hvar).map maxAbs) := Measure.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).hypothesesS :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.hypothesesconclusionsampleMean 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.hypothesesyL yU :X → ℝx :Xconclusion‖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)
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.hypothesesconclusion∀ n,Proof (Lean source)
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.hypothesesS :IIDSample Ω X μ PyL yU :X → ℝhLU :∀ z, yL z ≤ yU zhLmeas :Measurable yLhUmeas :Measurable yUhLint :Integrable yL PhUint :Integrable yU Pconclusion∀ n : ℕ,AEMeasurable (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.
The empirical Minkowski average (1/|s|) • ∑_{i∈s} Fᵢ.
Definition (Lean source)
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.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.
The grid supremum statistic returns the largest absolute support-process deviation across the chosen directions.
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)
The centered support process records each random set's support deviation from its center on a finite grid of directions.
Definition (Lean source)
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.conclusionContinuous (maxAbsK (k := k))Proof (Lean source)
-
measurable_maxAbsKlemma — The grid supremum statistic is measurable.conclusionMeasurable (maxAbsK (k := k))Proof (Lean source)
lemma measurable_maxAbsK : Measurable (maxAbsK (k := k)) := continuous_maxAbsK.measurable -
instIsProbabilityMeasureRealMapEuclideanSpaceFinMaxAbsKGaussianLimitinstance — The finite-grid support statistic has a probability measure as its Gaussian pushforward limit law.instance : IsProbabilityMeasure ((gaussianLimit hψ hvar).map maxAbsK) := Measure.isProbabilityMeasure_map measurable_maxAbsK.aemeasurable -
supportProcess_ofLplemma — Each coordinate of the centered support process is the corresponding support deviation.hypothesesconclusionProof (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.hypothesesS :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.
The finite-grid test statistic is the grid supremum of the normalized centered support-process sum.
Definition (Lean source)
The rejection region of the finite-grid test at critical value c: reject H₀ : E[F] = EF when the statistic Tₙ exceeds c.
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.
Minkowski dilation of a real set by a radius r: A ⊕ [−r, r] = {a + t | a ∈ A, |t| ≤ r}. In Beresteanu–Molinari this is the confidence region Uₙ = Ȳₙ ⊕ B(0, r) built around the estimated interval.
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)
The directed-Hausdorff functional dirStat w = max 0 (max w₀ (−w₁)) on ℝ². On the centered endpoint normalised sum it is √n · dᴴ(E[Y], Ȳₙ).
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)
lemma measurable_dirStat : Measurable dirStat := continuous_dirStat.measurable -
instIsProbabilityMeasureRealMapEuclideanSpaceFinOfNatNatDirStatGaussianLimitinstance — The directed limit law is a probability measure.instance : IsProbabilityMeasure ((gaussianLimit hψ hvar).map dirStat) := Measure.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.hypothesesS :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], Ȳₙ).hypothesesS :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 ω)]