Chapter 6: A Review of Large Sample Asymptotics
This page is generated from the canonical Chapter 6 inventory and the compiled Lean environment. It contains 18 textbook result groups and 66 selected Lean endpoints. When an inventory row links a large proof surface, this page shows at most six theorem-facing endpoints. The inventory remains the source of truth for all supporting links, qualifications, and open gaps.
Theorem 6.1 Weak Law of Large Numbers1 endpoint
If Y_i \in \mathbb{R}^k are i.i.d. and \mathbb{E}\lVert Y \rVert \lt \infty, then \bar{Y} = \frac{1}{n} \sum_{i=1}^n Y_i \xrightarrow{p} \mathbb{E}[Y]
theorem HansenEconometrics.tendstoInMeasure_wlln
Weak law of large numbers (Banach-valued, pairwise-independent form).
If X : ℕ → Ω → E is a sequence of pairwise-independent, identically distributed, integrable E-valued random variables on a finite-measure space, then the sample mean (1/n) ∑_{i<n} X i converges in probability to 𝔼[X 0].
This is the direct composition of Mathlib’s strong_law_ae with tendstoInMeasure_of_tendsto_ae. Provided here as a named lemma to match the econometrics literature’s WLLN statement.
Formal statement
∀ {Ω : Type u_4} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {E : Type u_5} [inst : NormedAddCommGroup E]
[inst_1 : NormedSpace Real E] [CompleteSpace E] [inst_3 : MeasurableSpace E] [BorelSpace E]
[MeasureTheory.IsFiniteMeasure μ] (X : Nat → Ω → E),
MeasureTheory.Integrable (X 0) μ →
Pairwise (Function.onFun (fun x1 x2 => ProbabilityTheory.IndepFun x1 x2 μ) X) →
(∀ (i : Nat), ProbabilityTheory.IdentDistrib (X i) (X 0) μ μ) →
MeasureTheory.TendstoInMeasure μ
(fun n ω => instHSMul.hSMul (Real.instInv.inv n.cast) ((Finset.range n).sum fun i => X i ω)) Filter.atTop
fun x => MeasureTheory.integral μ fun x => X 0 xTheorem 6.2 transformed WLLN1 endpoint
If Y_i \in \mathbb{R}^k are i.i.d., h : \mathbb{R}^k \to \mathbb{R}^q, and \mathbb{E}\lVert h(Y) \rVert \lt \infty, then \hat{\mu} = \frac{1}{n} \sum_{i=1}^n h(Y_i) \xrightarrow{p} \mu = \mathbb{E}[h(Y)]
theorem HansenEconometrics.tendstoInMeasure_transformed_wlln
Hansen Theorem 6.2, transformed WLLN.
If X i are pairwise-independent and identically distributed and h (X 0) is integrable, then the sample mean of the transformed variables h (X i) converges in probability to 𝔼[h (X 0)]. This is the textbook transformed WLLN packaged as composition of the Banach-valued WLLN with measurable-map preservation of independence and identical distribution.
Formal statement
∀ {Ω : Type u_4} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {E : Type u_5} {F : Type u_6}
[inst : MeasurableSpace E] [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace Real F] [CompleteSpace F]
[inst_4 : MeasurableSpace F] [BorelSpace F] [MeasureTheory.IsFiniteMeasure μ] (X : Nat → Ω → E) (h : E → F),
Measurable h →
MeasureTheory.Integrable (fun ω => h (X 0 ω)) μ →
Pairwise (Function.onFun (fun x1 x2 => ProbabilityTheory.IndepFun x1 x2 μ) X) →
(∀ (i : Nat), ProbabilityTheory.IdentDistrib (X i) (X 0) μ μ) →
MeasureTheory.TendstoInMeasure μ
(fun n ω => instHSMul.hSMul (Real.instInv.inv n.cast) ((Finset.range n).sum fun i => h (X i ω)))
Filter.atTop fun x => MeasureTheory.integral μ fun x => (fun ω => h (X 0 ω)) xDefinition 6.3 consistency1 endpoint
\hat{\theta} is consistent for \theta if \hat{\theta} \xrightarrow{p} \theta
def HansenEconometrics.Consistent
Hansen Definition 6.3, consistency.
An estimator sequence is consistent for θ when it converges to the constant limit θ in measure. This is a chapter-facing name for the Mathlib TendstoInMeasure idiom used throughout the asymptotic files.
Formal statement
{Ω : Type u_1} →
{E : Type u_2} →
{mΩ : MeasurableSpace Ω} → [PseudoEMetricSpace E] → MeasureTheory.Measure Ω → (Nat → Ω → E) → E → PropTheorem 6.3 multivariate Lindeberg-Lévy CLT2 endpoints
If Y_i \in \mathbb{R}^k are i.i.d. and \mathbb{E}\lVert Y \rVert^2 \lt \infty, then \sqrt{n}(\bar{Y} - \mu) \xrightarrow{d} N(0,V) where \mu = \mathbb{E}[Y] and V = \mathbb{E}[(Y-\mu)(Y-\mu)']
theorem HansenEconometrics.iidScalarCLT_tendstoInDistribution_gaussian
Hansen Theorem 6.3, scalar iid CLT wrapper.
For iid real random variables with finite second moment, the centered sample sum scaled by 1 / sqrt n converges in distribution to the Gaussian with the matching variance. This is a chapter-facing name for Mathlib’s scalar CLT.
Formal statement
∀ {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {μ : MeasureTheory.Measure Ω}
[inst : MeasureTheory.IsProbabilityMeasure μ] {ν : MeasureTheory.Measure Ω'}
[inst_1 : MeasureTheory.IsProbabilityMeasure ν] {Y : Nat → Ω → Real} {Z : Ω' → Real},
ProbabilityTheory.HasLaw Z (ProbabilityTheory.gaussianReal 0 (ProbabilityTheory.variance (Y 0) μ).toNNReal) ν →
MeasureTheory.MemLp (Y 0) 2 μ →
ProbabilityTheory.iIndepFun Y μ →
(∀ (i : Nat), ProbabilityTheory.IdentDistrib (Y i) (Y 0) μ μ) →
MeasureTheory.TendstoInDistribution
(fun n ω =>
instHMul.hMul (Real.instInv.inv n.cast.sqrt)
(instHSub.hSub ((Finset.range n).sum fun i => Y i ω)
(instHMul.hMul n.cast (MeasureTheory.integral μ fun x => Y 0 x))))
Filter.atTop Z (fun x => μ) ν
theorem HansenEconometrics.iidVectorCLT_tendstoInDistribution_multivariateGaussian
Hansen Theorem 6.3, finite-dimensional iid vector CLT.
For iid k-vectors with finite second moment, the centered sample sum scaled by 1 / sqrt n converges in distribution to the centered multivariate Gaussian with covariance matrix covMat μ (Y 0). The theorem is stated in EuclideanSpace form so it can be consumed directly by Cramer-Wold and Gaussian law infrastructure.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_3} [inst : Fintype k] [inst_1 : DecidableEq k]
{μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsProbabilityMeasure μ] {Y : Nat → Ω → k → Real},
MeasureTheory.MemLp (Y 0) 2 μ →
ProbabilityTheory.iIndepFun Y μ →
(∀ (i : Nat), ProbabilityTheory.IdentDistrib (Y i) (Y 0) μ μ) →
MeasureTheory.TendstoInDistribution
(fun n ω =>
{
ofLp :=
instHSMul.hSMul (Real.instInv.inv n.cast.sqrt)
(instHSub.hSub ((Finset.range n).sum fun i => Y i ω)
(instHSMul.hSMul n.cast (HansenEconometrics.meanVec μ (Y 0)))) })
Filter.atTop (fun z => z) (fun x => μ)
(ProbabilityTheory.multivariateGaussian 0 (HansenEconometrics.covMat μ (Y 0)))Direct statement dependencies (2)
-
HansenEconometrics.covMat -
HansenEconometrics.meanVec
Theorem 6.4 multivariate Lindeberg CLT6 endpoints
If Y_{ni} are independent with \mathbb{E}[Y_{ni}] = 0, variance matrices V_{ni}, \nu_n^2 = \lambda_{\min}(V_n) \gt 0, and the Lindeberg condition \nu_n^{-2} \sum_i \mathbb{E}[\lVert Y_{ni} \rVert^2 1\{\lVert Y_{ni} \rVert^2 \ge \epsilon \nu_n^2\}] \to 0, then V_n^{-1/2} \sum_i Y_{ni} \xrightarrow{d} N(0,I_k)
theorem HansenEconometrics.multivariateLindebergCLT_tendstoInDistribution
Hansen Theorem 6.4, multivariate Lindeberg CLT endpoint.
Once scalar projection Lindeberg CLTs are available for a normalized triangular array statistic, Cramér-Wold gives the corresponding multivariate Gaussian limit. The textbook normalization V_n^{-1/2} ∑ᵢ Y_{ni} is represented by the user-supplied statistic T.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_2} [inst : Fintype k] [inst_1 : DecidableEq k]
{μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsProbabilityMeasure μ] {T : Nat → Ω → k → Real}
{S : Matrix k k Real},
HansenEconometrics.MultivariateLindebergCLTConditions μ T S →
MeasureTheory.TendstoInDistribution (fun n ω => { ofLp := T n ω }) Filter.atTop (fun z => z) (fun x => μ)
(ProbabilityTheory.multivariateGaussian 0 S)Direct statement dependencies (1)
-
HansenEconometrics.MultivariateLindebergCLTConditions
theorem HansenEconometrics.multivariateIndexedLindebergCLT_tendstoInDistribution
Indexed multivariate Lindeberg CLT endpoint.
Once scalar projection Lindeberg CLTs are available for an indexed normalized array statistic, indexed Cramér-Wold gives the corresponding multivariate Gaussian limit. This is the source-space-varying analogue of multivariateLindebergCLT_tendstoInDistribution.
Formal statement
∀ {k : Type u_2} [inst : Fintype k] [inst_1 : DecidableEq k] {Ωrow : Nat → Type u_3}
[inst_2 : (n : Nat) → MeasurableSpace (Ωrow n)] {P : (n : Nat) → MeasureTheory.Measure (Ωrow n)}
[inst_3 : ∀ (n : Nat), MeasureTheory.IsProbabilityMeasure (P n)] {T : (n : Nat) → Ωrow n → k → Real}
{S : Matrix k k Real},
HansenEconometrics.MultivariateIndexedLindebergCLTConditions Ωrow P T S →
MeasureTheory.TendstoInDistribution (fun n ω => { ofLp := T n ω }) Filter.atTop (fun z => z) P
(ProbabilityTheory.multivariateGaussian 0 S)Direct statement dependencies (1)
-
HansenEconometrics.MultivariateIndexedLindebergCLTConditions
theorem HansenEconometrics.sq_tail_indicator_le_even_moment_div_threshold
Indicator form of sq_le_even_moment_div_threshold, matching the Lindeberg tail summand.
Formal statement
∀ (x c : Real) (m : Nat),
Real.instLT.lt 0 c →
Real.instLE.le ((setOf fun y => Real.instLE.le c (instHPow.hPow y 2)).indicator (fun y => instHPow.hPow y 2) x)
(instHDiv.hDiv (instHPow.hPow (abs x) (instHAdd.hAdd 2 (instHMul.hMul 2 m))) (instHPow.hPow c m))
theorem HansenEconometrics.integral_sq_tail_le_integral_even_moment_div_threshold
Expected-tail form of the even-moment Lyapunov bound. This is the scalar estimate used to turn a higher even moment into a Lindeberg tail bound once the array normalization supplies the threshold c.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} (μ : MeasureTheory.Measure Ω) (X : Ω → Real) (c : Real) (m : Nat),
Real.instLT.lt 0 c →
MeasureTheory.Integrable
(fun ω => (setOf fun y => Real.instLE.le c (instHPow.hPow y 2)).indicator (fun y => instHPow.hPow y 2) (X ω))
μ →
MeasureTheory.Integrable (fun ω => instHPow.hPow (abs (X ω)) (instHAdd.hAdd 2 (instHMul.hMul 2 m))) μ →
Real.instLE.le
(MeasureTheory.integral μ fun ω =>
(setOf fun y => Real.instLE.le c (instHPow.hPow y 2)).indicator (fun y => instHPow.hPow y 2) (X ω))
(instHDiv.hDiv
(MeasureTheory.integral μ fun ω => instHPow.hPow (abs (X ω)) (instHAdd.hAdd 2 (instHMul.hMul 2 m)))
(instHPow.hPow c m))
theorem HansenEconometrics.sum_integral_sq_tail_le_sum_integral_even_moment_div_threshold
Finite-row version of the expected Lyapunov tail bound, matching the finite sums in triangular-array Lindeberg conditions.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {ι : Type u_3} [inst : Fintype ι] (μ : MeasureTheory.Measure Ω)
(X : ι → Ω → Real) (c : Real) (m : Nat),
Real.instLT.lt 0 c →
(∀ (i : ι),
MeasureTheory.Integrable
(fun ω =>
(setOf fun y => Real.instLE.le c (instHPow.hPow y 2)).indicator (fun y => instHPow.hPow y 2) (X i ω))
μ) →
(∀ (i : ι),
MeasureTheory.Integrable (fun ω => instHPow.hPow (abs (X i ω)) (instHAdd.hAdd 2 (instHMul.hMul 2 m))) μ) →
Real.instLE.le
(Finset.univ.sum fun i =>
MeasureTheory.integral μ fun ω =>
(setOf fun y => Real.instLE.le c (instHPow.hPow y 2)).indicator (fun y => instHPow.hPow y 2) (X i ω))
(Finset.univ.sum fun i =>
instHDiv.hDiv
(MeasureTheory.integral μ fun ω => instHPow.hPow (abs (X i ω)) (instHAdd.hAdd 2 (instHMul.hMul 2 m)))
(instHPow.hPow c m))
theorem HansenEconometrics.normalized_sum_integral_sq_tail_le_normalized_even_moment_bound
Normalized finite-row Lyapunov tail bound. This is the direct algebraic shape of the scalar Lindeberg expression once the normalization is fixed.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {ι : Type u_3} [inst : Fintype ι] (μ : MeasureTheory.Measure Ω)
(X : ι → Ω → Real) (c scale : Real) (m : Nat),
Real.instLT.lt 0 c →
Real.instLE.le 0 scale →
(∀ (i : ι),
MeasureTheory.Integrable
(fun ω =>
(setOf fun y => Real.instLE.le c (instHPow.hPow y 2)).indicator (fun y => instHPow.hPow y 2) (X i ω))
μ) →
(∀ (i : ι),
MeasureTheory.Integrable (fun ω => instHPow.hPow (abs (X i ω)) (instHAdd.hAdd 2 (instHMul.hMul 2 m))) μ) →
Real.instLE.le
(instHMul.hMul scale
(Finset.univ.sum fun i =>
MeasureTheory.integral μ fun ω =>
(setOf fun y => Real.instLE.le c (instHPow.hPow y 2)).indicator (fun y => instHPow.hPow y 2) (X i ω)))
(instHMul.hMul scale
(Finset.univ.sum fun i =>
instHDiv.hDiv
(MeasureTheory.integral μ fun ω => instHPow.hPow (abs (X i ω)) (instHAdd.hAdd 2 (instHMul.hMul 2 m)))
(instHPow.hPow c m)))Theorem 6.5 heterogeneous-array CLT6 of 7 linked endpoints
If Y_{ni} are independent with \mathbb{E}[Y_{ni}] = 0, n^{-1}\sum_i V_{ni} \to V \gt 0, and \sup_{n,i} \mathbb{E}\lVert Y_{ni} \rVert^{2+\delta} \lt \infty for some \delta \gt 0, then \sqrt{n}\,\bar{Y} \xrightarrow{d} N(0,V)
theorem HansenEconometrics.heterogeneousArrayCLT_tendstoInDistribution
Hansen Theorem 6.5, heterogeneous-array CLT endpoint.
This is the multivariate Cramér-Wold assembly for the heterogeneous-array CLT: scalar projection CLTs for the normalized sample average imply convergence to the centered Gaussian with covariance V.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {k : Type u_2} [inst : Fintype k] [inst_1 : DecidableEq k]
{μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsProbabilityMeasure μ] {T : Nat → Ω → k → Real}
{V : Matrix k k Real},
HansenEconometrics.HeterogeneousArrayCLTConditions μ T V →
MeasureTheory.TendstoInDistribution (fun n ω => { ofLp := T n ω }) Filter.atTop (fun z => z) (fun x => μ)
(ProbabilityTheory.multivariateGaussian 0 V)Direct statement dependencies (1)
-
HansenEconometrics.HeterogeneousArrayCLTConditions
theorem HansenEconometrics.sq_le_even_moment_div_threshold
Even-moment Lyapunov tail bound for scalar triangular arrays.
On the tail event c ≤ x^2, the squared summand is bounded by the (2 + 2m)-moment scaled by c^m. This is the deterministic scalar inequality behind an even-moment Lyapunov discharge of Hansen’s Lindeberg condition.
Formal statement
∀ (x c : Real) (m : Nat),
Real.instLT.lt 0 c →
Real.instLE.le c (instHPow.hPow x 2) →
Real.instLE.le (instHPow.hPow x 2)
(instHDiv.hDiv (instHPow.hPow (abs x) (instHAdd.hAdd 2 (instHMul.hMul 2 m))) (instHPow.hPow c m))
theorem HansenEconometrics.sq_tail_indicator_le_even_moment_div_threshold
Indicator form of sq_le_even_moment_div_threshold, matching the Lindeberg tail summand.
Formal statement
∀ (x c : Real) (m : Nat),
Real.instLT.lt 0 c →
Real.instLE.le ((setOf fun y => Real.instLE.le c (instHPow.hPow y 2)).indicator (fun y => instHPow.hPow y 2) x)
(instHDiv.hDiv (instHPow.hPow (abs x) (instHAdd.hAdd 2 (instHMul.hMul 2 m))) (instHPow.hPow c m))
theorem HansenEconometrics.integral_sq_tail_le_integral_even_moment_div_threshold
Expected-tail form of the even-moment Lyapunov bound. This is the scalar estimate used to turn a higher even moment into a Lindeberg tail bound once the array normalization supplies the threshold c.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} (μ : MeasureTheory.Measure Ω) (X : Ω → Real) (c : Real) (m : Nat),
Real.instLT.lt 0 c →
MeasureTheory.Integrable
(fun ω => (setOf fun y => Real.instLE.le c (instHPow.hPow y 2)).indicator (fun y => instHPow.hPow y 2) (X ω))
μ →
MeasureTheory.Integrable (fun ω => instHPow.hPow (abs (X ω)) (instHAdd.hAdd 2 (instHMul.hMul 2 m))) μ →
Real.instLE.le
(MeasureTheory.integral μ fun ω =>
(setOf fun y => Real.instLE.le c (instHPow.hPow y 2)).indicator (fun y => instHPow.hPow y 2) (X ω))
(instHDiv.hDiv
(MeasureTheory.integral μ fun ω => instHPow.hPow (abs (X ω)) (instHAdd.hAdd 2 (instHMul.hMul 2 m)))
(instHPow.hPow c m))
theorem HansenEconometrics.sum_integral_sq_tail_le_sum_integral_even_moment_div_threshold
Finite-row version of the expected Lyapunov tail bound, matching the finite sums in triangular-array Lindeberg conditions.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {ι : Type u_3} [inst : Fintype ι] (μ : MeasureTheory.Measure Ω)
(X : ι → Ω → Real) (c : Real) (m : Nat),
Real.instLT.lt 0 c →
(∀ (i : ι),
MeasureTheory.Integrable
(fun ω =>
(setOf fun y => Real.instLE.le c (instHPow.hPow y 2)).indicator (fun y => instHPow.hPow y 2) (X i ω))
μ) →
(∀ (i : ι),
MeasureTheory.Integrable (fun ω => instHPow.hPow (abs (X i ω)) (instHAdd.hAdd 2 (instHMul.hMul 2 m))) μ) →
Real.instLE.le
(Finset.univ.sum fun i =>
MeasureTheory.integral μ fun ω =>
(setOf fun y => Real.instLE.le c (instHPow.hPow y 2)).indicator (fun y => instHPow.hPow y 2) (X i ω))
(Finset.univ.sum fun i =>
instHDiv.hDiv
(MeasureTheory.integral μ fun ω => instHPow.hPow (abs (X i ω)) (instHAdd.hAdd 2 (instHMul.hMul 2 m)))
(instHPow.hPow c m))
theorem HansenEconometrics.normalized_sum_integral_sq_tail_le_normalized_even_moment_bound
Normalized finite-row Lyapunov tail bound. This is the direct algebraic shape of the scalar Lindeberg expression once the normalization is fixed.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {ι : Type u_3} [inst : Fintype ι] (μ : MeasureTheory.Measure Ω)
(X : ι → Ω → Real) (c scale : Real) (m : Nat),
Real.instLT.lt 0 c →
Real.instLE.le 0 scale →
(∀ (i : ι),
MeasureTheory.Integrable
(fun ω =>
(setOf fun y => Real.instLE.le c (instHPow.hPow y 2)).indicator (fun y => instHPow.hPow y 2) (X i ω))
μ) →
(∀ (i : ι),
MeasureTheory.Integrable (fun ω => instHPow.hPow (abs (X i ω)) (instHAdd.hAdd 2 (instHMul.hMul 2 m))) μ) →
Real.instLE.le
(instHMul.hMul scale
(Finset.univ.sum fun i =>
MeasureTheory.integral μ fun ω =>
(setOf fun y => Real.instLE.le c (instHPow.hPow y 2)).indicator (fun y => instHPow.hPow y 2) (X i ω)))
(instHMul.hMul scale
(Finset.univ.sum fun i =>
instHDiv.hDiv
(MeasureTheory.integral μ fun ω => instHPow.hPow (abs (X i ω)) (instHAdd.hAdd 2 (instHMul.hMul 2 m)))
(instHPow.hPow c m)))Theorem 6.6 Continuous Mapping Theorem in probability6 of 7 linked endpoints
If Z_n \xrightarrow{p} c and g is continuous at c, then g(Z_n) \xrightarrow{p} g(c)
theorem HansenEconometrics.tendstoInMeasure_pi
Coordinatewise ⇒ joint TendstoInMeasure for Pi types over a Fintype: if every coordinate sequence converges in measure, so does the joint sequence.
Formal statement
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_4} [inst : Fintype β]
{X : β → Type u_5} [inst_1 : (b : β) → EDist (X b)] {f : Nat → α → (b : β) → X b} {g : α → (b : β) → X b},
(∀ (b : β), MeasureTheory.TendstoInMeasure μ (fun n ω => f n ω b) Filter.atTop fun ω => g ω b) →
MeasureTheory.TendstoInMeasure μ f Filter.atTop g
theorem HansenEconometrics.tendstoInMeasure_add
Additive CMT for TendstoInMeasure. If f n →ₚ finf and g n →ₚ ginf in a pseudo-metrizable additive topological group, then f n + g n →ₚ finf + ginf. Mathlib lacks a named additive glue for TendstoInMeasure; we assemble it from the product CMT and continuity of +.
Formal statement
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {E : Type u_4}
[inst : PseudoEMetricSpace E] [TopologicalSpace.PseudoMetrizableSpace E] [inst_2 : Add E] [ContinuousAdd E]
{f g : Nat → α → E} {finf ginf : α → E},
(∀ (n : Nat), MeasureTheory.AEStronglyMeasurable (f n) μ) →
(∀ (n : Nat), MeasureTheory.AEStronglyMeasurable (g n) μ) →
MeasureTheory.TendstoInMeasure μ f Filter.atTop finf →
MeasureTheory.TendstoInMeasure μ g Filter.atTop ginf →
MeasureTheory.TendstoInMeasure μ (fun n ω => instHAdd.hAdd (f n ω) (g n ω)) Filter.atTop fun ω =>
instHAdd.hAdd (finf ω) (ginf ω)
theorem HansenEconometrics.tendstoInMeasure_prodMk
Joint TendstoInMeasure on a product. If f n →ₚ finf and g n →ₚ ginf, then (f n, g n) →ₚ (finf, ginf) in the product E-metric.
Formal statement
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_4} {F : Type u_5}
[inst : PseudoEMetricSpace E] [inst_1 : PseudoEMetricSpace F] {f : Nat → α → E} {finf : α → E} {g : Nat → α → F}
{ginf : α → F},
MeasureTheory.TendstoInMeasure μ f Filter.atTop finf →
MeasureTheory.TendstoInMeasure μ g Filter.atTop ginf →
MeasureTheory.TendstoInMeasure μ (fun n ω => { fst := f n ω, snd := g n ω }) Filter.atTop fun ω =>
{ fst := finf ω, snd := ginf ω }
theorem HansenEconometrics.tendstoInMeasure_mulVec
Matrix-vector multiplication CMT. If A n →ₚ Ainf (matrix in measure) and v n →ₚ vinf (vector in measure), then A n ᵥ v n →ₚ Ainf ᵥ vinf.
Formal statement
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {k : Type u_4}
[inst : Fintype k] {A : Nat → α → Matrix k k Real} {Ainf : α → Matrix k k Real} {v : Nat → α → k → Real}
{vinf : α → k → Real},
(∀ (n : Nat), MeasureTheory.AEStronglyMeasurable (A n) μ) →
(∀ (n : Nat), MeasureTheory.AEStronglyMeasurable (v n) μ) →
MeasureTheory.TendstoInMeasure μ A Filter.atTop Ainf →
MeasureTheory.TendstoInMeasure μ v Filter.atTop vinf →
MeasureTheory.TendstoInMeasure μ (fun n ω => (A n ω).mulVec (v n ω)) Filter.atTop fun ω =>
(Ainf ω).mulVec (vinf ω)
theorem HansenEconometrics.tendstoInMeasure_matrix_inv
CMT for matrix inversion. If A n →ₚ A’ in measure and A’ ω is nonsingular for every ω, then (A n)⁻¹ →ₚ (A’)⁻¹ in measure.
Pointwise a.s. convergence follows from Mathlib’s continuousAt_matrix_inv, which gives continuity of matrix inversion at each nonsingular limit point. Measurability of the inverse sequence reuses aestronglyMeasurable_matrix_inv.
Formal statement
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {k : Type u_4} [inst : Fintype k]
[inst_1 : DecidableEq k] [MeasureTheory.IsFiniteMeasure μ] {A : Nat → α → Matrix k k Real} {A' : α → Matrix k k Real},
(∀ (n : Nat), MeasureTheory.AEStronglyMeasurable (A n) μ) →
MeasureTheory.TendstoInMeasure μ A Filter.atTop A' →
(∀ (ω : α), IsUnit (A' ω).det) →
MeasureTheory.TendstoInMeasure μ (fun n ω => Matrix.inv.inv (A n ω)) Filter.atTop fun ω => Matrix.inv.inv (A' ω)
theorem HansenEconometrics.tendstoInMeasure_matrix_mul
Matrix multiplication CMT. If A n →ₚ Ainf and B n →ₚ Binf in measure, then A n * B n →ₚ Ainf * Binf.
Formal statement
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {k : Type u_4}
[inst : Fintype k] {A B : Nat → α → Matrix k k Real} {Ainf Binf : α → Matrix k k Real},
(∀ (n : Nat), MeasureTheory.AEStronglyMeasurable (A n) μ) →
(∀ (n : Nat), MeasureTheory.AEStronglyMeasurable (B n) μ) →
MeasureTheory.TendstoInMeasure μ A Filter.atTop Ainf →
MeasureTheory.TendstoInMeasure μ B Filter.atTop Binf →
MeasureTheory.TendstoInMeasure μ
(fun n ω => Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul (A n ω) (B n ω)) Filter.atTop fun ω =>
Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul (Ainf ω) (Binf ω)Theorem 6.7 Continuous Mapping Theorem in distribution3 endpoints
If Z_n \xrightarrow{d} Z and g is continuous Z-a.s., then g(Z_n) \xrightarrow{d} g(Z)
theorem HansenEconometrics.tendstoInDistribution_ae_continuous_comp
Hansen Theorem 6.7, a.s.-continuity CMT in distribution.
If Xₙ ⇒ Z and a measurable map g is continuous off a set with zero limit-law probability, then g(Xₙ) ⇒ g(Z). This is the textbook a.s.-continuity face of the continuous-mapping theorem; the null set is stated on the law of Z, i.e. (ν.map Z) D = 0.
Formal statement
∀ {Ω : Type u_4} {Ω' : Type u_5} {E : Type u_6} {F : Type u_7} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'}
{P : Nat → MeasureTheory.Measure Ω} [inst : ∀ (n : Nat), MeasureTheory.IsProbabilityMeasure (P n)]
{ν : MeasureTheory.Measure Ω'} [inst_1 : MeasureTheory.IsProbabilityMeasure ν] [inst_2 : TopologicalSpace E]
[inst_3 : MeasurableSpace E] [inst_4 : OpensMeasurableSpace E] [HasOuterApproxClosed E] [inst_6 : TopologicalSpace F]
[inst_7 : MeasurableSpace F] [inst_8 : BorelSpace F] {X : Nat → Ω → E} {Z : Ω' → E} {g : E → F},
MeasureTheory.TendstoInDistribution X Filter.atTop Z P ν →
Measurable g →
∀ {D : Set E},
Eq (MeasureTheory.Measure.instFunLike.coe (MeasureTheory.Measure.map Z ν) D) 0 →
(∀ (x : E), Not (Set.instMembership.mem D x) → ContinuousAt g x) →
MeasureTheory.TendstoInDistribution (fun n ω => g (X n ω)) Filter.atTop (fun ω => g (Z ω)) P ν
theorem HansenEconometrics.probabilityMeasure_tendsto_map_of_tendsto_of_ae_continuous
Push-forward CMT for maps continuous outside a limit-null set.
If probability laws νs converge weakly to ν, and a measurable map g is continuous away from a ν-null set D, then the push-forward laws converge weakly. This is the probability-measure core of Hansen’s a.s.-continuity continuous-mapping theorem.
The proof is the standard Portmanteau closed-set argument: for closed C, the closure of g ⁻¹’ C is contained in g ⁻¹’ C ∪ D; weak convergence controls the closed closure, and the null set removes the discontinuity contribution.
Formal statement
∀ {ι : Type u_4} {E : Type u_5} {F : Type u_6} {L : Filter ι} [L.IsCountablyGenerated] [inst : TopologicalSpace E]
[inst_1 : MeasurableSpace E] [inst_2 : OpensMeasurableSpace E] [HasOuterApproxClosed E] [inst_4 : TopologicalSpace F]
[inst_5 : MeasurableSpace F] [inst_6 : BorelSpace F] {νs : ι → MeasureTheory.ProbabilityMeasure E}
{ν : MeasureTheory.ProbabilityMeasure E},
Filter.Tendsto νs L (nhds ν) →
∀ {g : E → F} (hg : Measurable g) {D : Set E},
Eq (MeasureTheory.Measure.instFunLike.coe ν.toMeasure D) 0 →
(∀ (x : E), Not (Set.instMembership.mem D x) → ContinuousAt g x) →
Filter.Tendsto (fun i => (νs i).map ⋯) L (nhds (ν.map ⋯))
theorem HansenEconometrics.tendstoInDistribution_continuous_comp
Hansen Theorem 6.7, global continuous-mapping theorem in distribution.
If Xₙ ⇒ Z and g is globally continuous, then g(Xₙ) ⇒ g(Z). This is the Mathlib-backed global-continuity face of Hansen’s distributional CMT; see tendstoInDistribution_ae_continuous_comp for the textbook a.s.-continuity form.
Formal statement
∀ {Ω : Type u_4} {Ω' : Type u_5} {E : Type u_6} {F : Type u_7} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'}
{P : Nat → MeasureTheory.Measure Ω} [inst : ∀ (n : Nat), MeasureTheory.IsProbabilityMeasure (P n)]
{ν : MeasureTheory.Measure Ω'} [inst_1 : MeasureTheory.IsProbabilityMeasure ν] [inst_2 : TopologicalSpace E]
[inst_3 : MeasurableSpace E] [inst_4 : OpensMeasurableSpace E] [inst_5 : TopologicalSpace F]
[inst_6 : MeasurableSpace F] [inst_7 : BorelSpace F] {X : Nat → Ω → E} {Z : Ω' → E} {g : E → F},
MeasureTheory.TendstoInDistribution X Filter.atTop Z P ν →
Continuous g → MeasureTheory.TendstoInDistribution (fun n ω => g (X n ω)) Filter.atTop (fun ω => g (Z ω)) P νTheorem 6.8 Delta Method6 of 7 linked endpoints
If p_n(\hat{\mu} - \mu) \xrightarrow{d} \xi and g is continuously differentiable near \mu, then p_n(g(\hat{\mu}) - g(\mu)) \xrightarrow{d} G' \xi where G = \partial g(\mu)'/\partial u
theorem HansenEconometrics.deltaMethod_remainder_isLittleO
Deterministic Delta-method remainder from Mathlib’s Fréchet derivative API.
This is the analytic core of Hansen Theorem 6.8: after subtracting the linear approximation, the remainder is little-o of the input displacement.
Formal statement
∀ {E : Type u_3} {F : Type u_4} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace Real E]
[inst_2 : SeminormedAddCommGroup F] [inst_3 : NormedSpace Real F] {g : E → F}
{G : ContinuousLinearMap (RingHom.id Real) E F} {θ : E},
HasFDerivAt g G θ →
Asymptotics.IsLittleO (nhds θ)
(fun x => instHSub.hSub (instHSub.hSub (g x) (g θ)) (ContinuousLinearMap.funLike.coe G (instHSub.hSub x θ)))
fun x => instHSub.hSub x θ
theorem HansenEconometrics.deltaMethod_tendstoInDistribution
Delta-method Slutsky wrapper.
If the linearized statistic Tₙ converges in distribution and the nonlinear statistic differs from G Tₙ by an oₚ(1) remainder, then the nonlinear statistic has the linear image of the limit. The deterministic source of the remainder is deltaMethod_remainder_isLittleO.
Formal statement
∀ {Ω : Type u_1} {Ω' : Type u_2} {E : Type u_3} {F : Type u_4} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'}
{μ : MeasureTheory.Measure Ω} {ν : MeasureTheory.Measure Ω'} [inst : SeminormedAddCommGroup E]
[inst_1 : NormedSpace Real E] [inst_2 : MeasurableSpace E] [inst_3 : BorelSpace E] [inst_4 : SeminormedAddCommGroup F]
[inst_5 : NormedSpace Real F] [SecondCountableTopology F] [inst_7 : MeasurableSpace F] [inst_8 : BorelSpace F]
[inst_9 : MeasureTheory.IsProbabilityMeasure μ] [inst_10 : MeasureTheory.IsProbabilityMeasure ν] {T : Nat → Ω → E}
{Z : Ω' → E} {R : Nat → Ω → F} {G : ContinuousLinearMap (RingHom.id Real) E F},
MeasureTheory.TendstoInDistribution T Filter.atTop Z (fun x => μ) ν →
(MeasureTheory.TendstoInMeasure μ R Filter.atTop fun x => 0) →
(∀ (n : Nat), AEMeasurable (R n) μ) →
MeasureTheory.TendstoInDistribution
(fun n ω => instHAdd.hAdd (ContinuousLinearMap.funLike.coe G (T n ω)) (R n ω)) Filter.atTop
(fun ω => ContinuousLinearMap.funLike.coe G (Z ω)) (fun x => μ) ν
theorem HansenEconometrics.coordinateInv_deltaMethod_remainder_isLittleO
Coordinate-reciprocal Delta-method remainder.
Formal statement
∀ {k : Type u_5} [inst : Fintype k] (j : k) {β : k → Real},
Ne (β j) 0 →
Asymptotics.IsLittleO (nhds β)
(fun b =>
instHSub.hSub (instHSub.hSub (Real.instInv.inv (b j)) (Real.instInv.inv (β j)))
(ContinuousLinearMap.funLike.coe
((ContinuousLinearMap.toSpanSingleton Real
(Real.instNeg.neg (Real.instInv.inv (instHPow.hPow (β j) 2)))).comp
(ContinuousLinearMap.proj j))
(instHSub.hSub b β)))
fun b => instHSub.hSub b β
theorem HansenEconometrics.coordinateRatio_deltaMethod_remainder_isLittleO
Coordinate-ratio Delta-method remainder.
Formal statement
∀ {k : Type u_5} [inst : Fintype k] (j l : k) {β : k → Real},
Ne (β l) 0 →
Asymptotics.IsLittleO (nhds β)
(fun b =>
instHSub.hSub
(instHSub.hSub (instHMul.hMul (b j) (Real.instInv.inv (b l))) (instHMul.hMul (β j) (Real.instInv.inv (β l))))
(ContinuousLinearMap.funLike.coe
(instHAdd.hAdd
(instHSMul.hSMul (β j)
((ContinuousLinearMap.toSpanSingleton Real
(Real.instNeg.neg (Real.instInv.inv (instHPow.hPow (β l) 2)))).comp
(ContinuousLinearMap.proj l)))
(instHSMul.hSMul (Real.instInv.inv (β l)) (ContinuousLinearMap.proj j)))
(instHSub.hSub b β)))
fun b => instHSub.hSub b β
theorem HansenEconometrics.coordinateSquare_deltaMethod_remainder_isLittleO
Coordinate-square Delta-method remainder.
This is the transform-specific Fréchet remainder for the nonlinear coefficient map β ↦ β_j².
Formal statement
∀ {k : Type u_5} [inst : Fintype k] (j : k) (β : k → Real),
Asymptotics.IsLittleO (nhds β)
(fun b =>
instHSub.hSub (instHSub.hSub (instHPow.hPow (b j) 2) (instHPow.hPow (β j) 2))
(ContinuousLinearMap.funLike.coe (instHSMul.hSMul (instHMul.hMul 2 (β j)) (ContinuousLinearMap.proj j))
(instHSub.hSub b β)))
fun b => instHSub.hSub b β
theorem HansenEconometrics.coordinateProduct_deltaMethod_remainder_isLittleO
Coordinate-product Delta-method remainder.
Formal statement
∀ {k : Type u_5} [inst : Fintype k] (j l : k) (β : k → Real),
Asymptotics.IsLittleO (nhds β)
(fun b =>
instHSub.hSub (instHSub.hSub (instHMul.hMul (b j) (b l)) (instHMul.hMul (β j) (β l)))
(ContinuousLinearMap.funLike.coe
(instHAdd.hAdd (instHSMul.hSMul (β j) (ContinuousLinearMap.proj l))
(instHSMul.hSMul (β l) (ContinuousLinearMap.proj j)))
(instHSub.hSub b β)))
fun b => instHSub.hSub b βTheorem 6.9 smooth-function consistency2 endpoints
If Y_i \in \mathbb{R}^m are i.i.d., h : \mathbb{R}^m \to \mathbb{R}^k, \mathbb{E}\lVert h(Y) \rVert \lt \infty, and g : \mathbb{R}^k \to \mathbb{R}^q is continuous at \mu, then \hat{\theta} \xrightarrow{p} \theta
theorem HansenEconometrics.smoothFunction_consistency
Hansen Theorem 6.9: smooth-function consistency from input consistency and continuity at the target.
Formal statement
∀ {Ω : Type u_1} {E : Type u_3} {F : Type u_4} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ] [inst : PseudoEMetricSpace E] [inst_1 : PseudoEMetricSpace F]
[TopologicalSpace.PseudoMetrizableSpace F] {θhat : Nat → Ω → E} {θ : E} {g : E → F},
(∀ (n : Nat), MeasureTheory.AEStronglyMeasurable (θhat n) μ) →
(∀ (n : Nat), MeasureTheory.AEStronglyMeasurable (fun ω => g (θhat n ω)) μ) →
(MeasureTheory.TendstoInMeasure μ θhat Filter.atTop fun x => θ) →
ContinuousAt g θ → MeasureTheory.TendstoInMeasure μ (fun n ω => g (θhat n ω)) Filter.atTop fun x => g θ
theorem HansenEconometrics.tendstoInMeasure_continuousAt_const_comp
Measurable-space compatibility form of the local continuous mapping theorem.
If f n →ₚ x and h is continuous at x, then h (f n) →ₚ h x, provided the input and composed sequences are a.e. strongly measurable. The stronger metric-space theorem tendstoInMeasure_continuousAt_const_comp_without_measurability is preferred when those technical premises are not part of the mathematical statement.
Formal statement
∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ] [inst : PseudoEMetricSpace E] [inst_1 : PseudoEMetricSpace F]
[TopologicalSpace.PseudoMetrizableSpace F] {f : Nat → α → E} {x : E} {h : E → F},
(∀ (n : Nat), MeasureTheory.AEStronglyMeasurable (f n) μ) →
(∀ (n : Nat), MeasureTheory.AEStronglyMeasurable (fun ω => h (f n ω)) μ) →
(MeasureTheory.TendstoInMeasure μ f Filter.atTop fun x_1 => x) →
ContinuousAt h x → MeasureTheory.TendstoInMeasure μ (fun n ω => h (f n ω)) Filter.atTop fun x_1 => h xTheorem 6.10 smooth-function asymptotic normality2 endpoints
If Y_i \in \mathbb{R}^m are i.i.d., \mathbb{E}\lVert h(Y) \rVert^2 \lt \infty, and g is continuously differentiable near \mu, then \sqrt{n}(\hat{\theta} - \theta) \xrightarrow{d} N(0,V_\theta) where V_\theta = G' V G
theorem HansenEconometrics.smoothFunction_asymptoticNormality_gaussian
Hansen Theorem 6.10, Gaussian Delta-method wrapper.
The input statistic converges to a centered multivariate Gaussian. The nonlinear statistic is represented as its matrix-linear Delta-method image plus an oₚ(1) remainder. The conclusion is stated directly with the named Gaussian law of the image, using hasLaw_multivariateGaussian_zero_linearMap.
Formal statement
∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {k : Type u_5} {q : Type u_6} [inst : Fintype k]
[inst_1 : Fintype q] [inst_2 : DecidableEq k] [inst_3 : DecidableEq q] {S : Matrix k k Real} {R : Matrix q k Real}
{T : Nat → Ω → EuclideanSpace Real k} {Y : Nat → Ω → EuclideanSpace Real q}
[inst_4 : MeasureTheory.IsProbabilityMeasure μ],
S.PosSemidef →
MeasureTheory.TendstoInDistribution T Filter.atTop (fun z => z) (fun x => μ)
(ProbabilityTheory.multivariateGaussian 0 S) →
(MeasureTheory.TendstoInMeasure μ
(instHSub.hSub Y fun n ω =>
ContinuousLinearMap.funLike.coe (HansenEconometrics.matrixContinuousLinearMap R) (T n ω))
Filter.atTop fun x => 0) →
(∀ (n : Nat), AEMeasurable (Y n) μ) →
MeasureTheory.TendstoInDistribution Y Filter.atTop (fun z => z) (fun x => μ)
(ProbabilityTheory.multivariateGaussian 0
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul R S)
R.transpose))Direct statement dependencies (1)
-
HansenEconometrics.matrixContinuousLinearMap
theorem HansenEconometrics.hasLaw_multivariateGaussian_zero_linearMap
A fixed matrix image of a centered multivariate Gaussian is a centered multivariate Gaussian with covariance R S Rᵀ.
Formal statement
∀ {n : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] {q : Type u_4} [inst_2 : Fintype q]
[inst_3 : DecidableEq q] {S : Matrix n n Real},
S.PosSemidef →
∀ (R : Matrix q n Real),
ProbabilityTheory.HasLaw (fun z => { ofLp := R.mulVec z.ofLp })
(ProbabilityTheory.multivariateGaussian 0
(Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul (Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.hMul R S)
R.transpose))
(ProbabilityTheory.multivariateGaussian 0 S)Theorem 6.11 best unbiased estimation of the mean6 of 10 linked endpoints
If \tilde{\mu} is unbiased for \mu = \mathbb{E}[h(Y)] and \mathbb{E}\lVert h(Y) \rVert^2 \lt \infty, then \operatorname{Var}(\tilde{\mu}) \ge n^{-1} V where V = \mathbb{E}[(h(Y)-\mu)(h(Y)-\mu)']
theorem HansenEconometrics.iidSampleMean_covMat_eq_inv_card_smul
Hansen Theorem 6.11, covariance-matrix sample-mean sharpness face.
For finite-dimensional square-integrable observations whose coordinates are pairwise independent across distinct observations and whose one-draw covariance matrix is common across observations, the covariance matrix of the sample mean is exactly 1 / n times that one-draw covariance matrix. This is the matrix-valued version of the sample-mean sharpness identity around Hansen’s best-unbiased-estimation theorem.
Formal statement
∀ {Ω : Type u_1} {ι : Type u_2} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {k : Type u_3}
[MeasureTheory.IsProbabilityMeasure μ] [inst : Fintype ι] [Nonempty ι] {Z : ι → Ω → k → Real} (j : ι),
(∀ (i : ι) (a : k), MeasureTheory.MemLp (fun ω => Z i ω a) 2 μ) →
(∀ (a b : k), Pairwise fun i l => ProbabilityTheory.IndepFun (fun ω => Z i ω a) (fun ω => Z l ω b) μ) →
(∀ (i : ι) (a b : k),
Eq (ProbabilityTheory.covariance (fun ω => Z i ω a) (fun ω => Z i ω b) μ)
(ProbabilityTheory.covariance (fun ω => Z j ω a) (fun ω => Z j ω b) μ)) →
Eq
(HansenEconometrics.covMat μ fun ω a =>
instHMul.hMul (Real.instInv.inv (Fintype.card ι).cast) (Finset.univ.sum fun i => Z i ω a))
(instHSMul.hSMul (Real.instInv.inv (Fintype.card ι).cast) (HansenEconometrics.covMat μ (Z j)))Direct statement dependencies (1)
-
HansenEconometrics.covMat
theorem HansenEconometrics.iidSampleMean_variance_eq_inv_card_mul
Hansen Theorem 6.11, sample-mean sharpness face.
For pairwise independent identically distributed square-integrable scalar observations, the variance of the finite-sample average is 1 / n times the variance of one draw. This formalizes the sharp sample-mean variance identity around Hansen’s best-unbiased-estimation theorem; the full lower bound for arbitrary unbiased estimators is a separate efficiency statement.
Formal statement
∀ {Ω : Type u_1} {ι : Type u_2} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ] [inst : Fintype ι] [Nonempty ι] {Z : ι → Ω → Real} (j : ι),
(∀ (i : ι), MeasureTheory.MemLp (Z i) 2 μ) →
(Pairwise fun i j => ProbabilityTheory.IndepFun (Z i) (Z j) μ) →
(∀ (i : ι), ProbabilityTheory.IdentDistrib (Z i) (Z j) μ μ) →
Eq
(ProbabilityTheory.variance
(fun ω => instHMul.hMul (Real.instInv.inv (Fintype.card ι).cast) (Finset.univ.sum fun i => Z i ω)) μ)
(instHMul.hMul (Real.instInv.inv (Fintype.card ι).cast) (ProbabilityTheory.variance (Z j) μ))
theorem HansenEconometrics.iidLinearUnbiasedEstimator_variance_ge_sampleMean
Hansen Theorem 6.11, scalar best-linear-unbiased face.
Among linear unbiased estimators ∑ᵢ wᵢ Zᵢ with weights summing to one, the equal-weight sample mean has minimal variance under iid square-integrable scalar observations. This is a linear-estimator lower-bound face of Hansen’s best-unbiased-estimation theorem; the arbitrary-estimator lower bound remains a separate efficiency statement.
Formal statement
∀ {Ω : Type u_1} {ι : Type u_2} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ] [inst : Fintype ι] [Nonempty ι] {Z : ι → Ω → Real} (j : ι) (w : ι → Real),
(∀ (i : ι), MeasureTheory.MemLp (Z i) 2 μ) →
(Pairwise fun i l => ProbabilityTheory.IndepFun (Z i) (Z l) μ) →
(∀ (i : ι), ProbabilityTheory.IdentDistrib (Z i) (Z j) μ μ) →
Eq (Finset.univ.sum fun i => w i) 1 →
Real.instLE.le (instHMul.hMul (Real.instInv.inv (Fintype.card ι).cast) (ProbabilityTheory.variance (Z j) μ))
(ProbabilityTheory.variance (fun ω => Finset.univ.sum fun i => instHMul.hMul (w i) (Z i ω)) μ)
theorem HansenEconometrics.iidLinearUnbiasedEstimator_covMat_sub_sampleMean_posSemidef
Hansen Theorem 6.11, vector best-linear-unbiased face.
For scalar weights summing to one, the covariance matrix of the weighted linear estimator ∑ᵢ wᵢ Zᵢ dominates the covariance matrix of the equal-weight sample mean. The proof applies the scalar best-linear-unbiased theorem to every fixed linear projection and then repackages the result as a positive-semidefinite matrix inequality.
Formal statement
∀ {Ω : Type u_1} {ι : Type u_2} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {k : Type u_3} [inst : Fintype k]
[MeasureTheory.IsProbabilityMeasure μ] [inst_2 : Fintype ι] [Nonempty ι] {Z : ι → Ω → k → Real} (j : ι)
(w : ι → Real),
(∀ (i : ι), MeasureTheory.MemLp (Z i) 2 μ) →
(Pairwise fun i l => ProbabilityTheory.IndepFun (Z i) (Z l) μ) →
(∀ (i : ι), ProbabilityTheory.IdentDistrib (Z i) (Z j) μ μ) →
Eq (Finset.univ.sum fun i => w i) 1 →
(instHSub.hSub (HansenEconometrics.covMat μ fun ω a => Finset.univ.sum fun i => instHMul.hMul (w i) (Z i ω a))
(instHSMul.hSMul (Real.instInv.inv (Fintype.card ι).cast) (HansenEconometrics.covMat μ (Z j)))).PosSemidefDirect statement dependencies (1)
-
HansenEconometrics.covMat
Theorem 6.12 moment bound implies stochastic boundedness6 of 14 linked endpoints
If \mathbb{E}\lVert Z_n \rVert^\delta = O(a_n) for some \delta \gt 0, then Z_n = O_p(a_n^{1/\delta}); if \mathbb{E}\lVert Z_n \rVert^\delta = o(a_n), then Z_n = o_p(a_n^{1/\delta})
theorem HansenEconometrics.BoundedInProbability.of_eventually_integral_norm_bound
A uniform eventual first absolute-moment bound implies scalar Oₚ(1).
This is the Markov-inequality face of Hansen Theorem 6.12 for the case aₙ = 1 and moment exponent one. Higher-moment statements reduce to this after applying the theorem to the nonnegative transformed sequence.
Formal statement
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
{X : Nat → α → Real} {C : Real},
Real.instLE.le 0 C →
(∀ (n : Nat), MeasureTheory.Integrable (fun ω => Real.norm.norm (X n ω)) μ) →
Filter.Eventually (fun n => Real.instLE.le (MeasureTheory.integral μ fun ω => Real.norm.norm (X n ω)) C)
Filter.atTop →
HansenEconometrics.BoundedInProbability μ XDirect statement dependencies (1)
-
HansenEconometrics.BoundedInProbability
theorem HansenEconometrics.BoundedInProbability.of_eventually_integral_norm_pow_bound
An eventual higher natural-moment bound implies scalar Oₚ(1).
This is the natural-power Markov-inequality face of Hansen Theorem 6.12. The positive-real-exponent face is BoundedInProbability.of_eventually_integral_norm_rpow_bound; this wrapper keeps the common integer-moment cases convenient.
Formal statement
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
{X : Nat → α → Real} {C : Real} {r : Nat},
Ne r 0 →
Real.instLE.le 0 C →
(∀ (n : Nat), MeasureTheory.Integrable (fun ω => instHPow.hPow (Real.norm.norm (X n ω)) r) μ) →
Filter.Eventually
(fun n => Real.instLE.le (MeasureTheory.integral μ fun ω => instHPow.hPow (Real.norm.norm (X n ω)) r) C)
Filter.atTop →
HansenEconometrics.BoundedInProbability μ XDirect statement dependencies (1)
-
HansenEconometrics.BoundedInProbability
theorem HansenEconometrics.TendstoInMeasure.of_integral_norm_rpow_scaled_tendsto_zero
Scaled positive-real moments tending to zero imply scaled oₚ(1).
This is the little-oₚ Markov-inequality face of Hansen Theorem 6.12: if E|Xₙ|^p / aₙ^p → 0 for a positive deterministic scale aₙ and p > 0, then aₙ⁻¹ Xₙ →ₚ 0.
Formal statement
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
{X : Nat → α → Real} {a : Nat → Real} {p : Real},
Real.instLT.lt 0 p →
Filter.Eventually (fun n => Real.instLT.lt 0 (a n)) Filter.atTop →
(∀ (n : Nat), MeasureTheory.Integrable (fun ω => instHPow.hPow (Real.norm.norm (X n ω)) p) μ) →
Filter.Tendsto
(fun n =>
instHDiv.hDiv (MeasureTheory.integral μ fun ω => instHPow.hPow (Real.norm.norm (X n ω)) p)
(instHPow.hPow (a n) p))
Filter.atTop (nhds 0) →
MeasureTheory.TendstoInMeasure μ (fun n ω => instHMul.hMul (Real.instInv.inv (a n)) (X n ω)) Filter.atTop
fun x => 0
theorem HansenEconometrics.BoundedInProbability.of_eventually_integral_norm_rpow_bound
An eventual positive-real moment bound implies scalar Oₚ(1).
This is the arbitrary positive-real-exponent Markov-inequality face of Hansen Theorem 6.12 for the unit scale: if E|Xₙ|^p is eventually bounded for some p > 0, then Xₙ = Oₚ(1).
Formal statement
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
{X : Nat → α → Real} {C p : Real},
Real.instLT.lt 0 p →
Real.instLE.le 0 C →
(∀ (n : Nat), MeasureTheory.Integrable (fun ω => instHPow.hPow (Real.norm.norm (X n ω)) p) μ) →
Filter.Eventually
(fun n => Real.instLE.le (MeasureTheory.integral μ fun ω => instHPow.hPow (Real.norm.norm (X n ω)) p) C)
Filter.atTop →
HansenEconometrics.BoundedInProbability μ XDirect statement dependencies (1)
-
HansenEconometrics.BoundedInProbability
theorem HansenEconometrics.BoundedInProbability.of_eventually_integral_norm_scaled_bound
Scaled first absolute-moment bounds imply scaled scalar Oₚ(1).
This is the δ = 1 scaled face of Hansen Theorem 6.12: if the first absolute moment of Xₙ is eventually bounded by a positive deterministic scale aₙ, then aₙ⁻¹ Xₙ is bounded in probability.
Formal statement
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
{X : Nat → α → Real} {a : Nat → Real} {C : Real},
Real.instLE.le 0 C →
Filter.Eventually (fun n => Real.instLT.lt 0 (a n)) Filter.atTop →
(∀ (n : Nat), MeasureTheory.Integrable (fun ω => Real.norm.norm (X n ω)) μ) →
Filter.Eventually
(fun n => Real.instLE.le (MeasureTheory.integral μ fun ω => Real.norm.norm (X n ω)) (instHMul.hMul C (a n)))
Filter.atTop →
HansenEconometrics.BoundedInProbability μ fun n ω => instHMul.hMul (Real.instInv.inv (a n)) (X n ω)Direct statement dependencies (1)
-
HansenEconometrics.BoundedInProbability
theorem HansenEconometrics.BoundedInProbability.of_eventually_integral_norm_pow_scaled_bound
Scaled natural-moment bounds imply scaled scalar Oₚ(1).
If E|Xₙ|^m is eventually bounded by C aₙ^m for a positive deterministic scale aₙ, then aₙ⁻¹ Xₙ is bounded in probability. This is the integer-power scaled version of Hansen Theorem 6.12; see BoundedInProbability.of_eventually_integral_norm_rpow_scaled_bound for the positive-real-exponent version.
Formal statement
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
{X : Nat → α → Real} {a : Nat → Real} {C : Real} {r : Nat},
Ne r 0 →
Real.instLE.le 0 C →
Filter.Eventually (fun n => Real.instLT.lt 0 (a n)) Filter.atTop →
(∀ (n : Nat), MeasureTheory.Integrable (fun ω => instHPow.hPow (Real.norm.norm (X n ω)) r) μ) →
Filter.Eventually
(fun n =>
Real.instLE.le (MeasureTheory.integral μ fun ω => instHPow.hPow (Real.norm.norm (X n ω)) r)
(instHMul.hMul C (instHPow.hPow (a n) r)))
Filter.atTop →
HansenEconometrics.BoundedInProbability μ fun n ω => instHMul.hMul (Real.instInv.inv (a n)) (X n ω)Direct statement dependencies (1)
-
HansenEconometrics.BoundedInProbability
Theorem 6.13 bounded first moments pass to the limit6 of 7 linked endpoints
If Z_n \xrightarrow{d} Z and \mathbb{E}\lVert Z_n \rVert \le C, then \mathbb{E}\lVert Z \rVert \le C
theorem HansenEconometrics.eLpNorm_one_limit_le_of_tendstoInMeasure_bound
Hansen Theorem 6.13, convergence-in-measure bounded-moment wrapper.
If a real sequence converges in measure and has eventually bounded L¹ seminorm, the limit has the same L¹ bound. This is the convergence-in-measure face of Hansen’s bounded-first-moment passage to the limit; the textbook weak-convergence statement is stronger.
Formal statement
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {Z : Nat → α → Real} {Zlim : α → Real}
{C : ENNReal},
Filter.Eventually (fun n => ENNReal.instPartialOrder.le (MeasureTheory.eLpNorm (Z n) 1 μ) C) Filter.atTop →
MeasureTheory.TendstoInMeasure μ Z Filter.atTop Zlim →
(∀ (n : Nat), MeasureTheory.AEStronglyMeasurable (Z n) μ) →
ENNReal.instPartialOrder.le (MeasureTheory.eLpNorm Zlim 1 μ) C
theorem HansenEconometrics.TendstoInDistribution.integrable_norm_limit_of_eventually_integral_norm_bound
Hansen Theorem 6.13, limit-integrability weak-moment face.
If Xₙ ⇒ Z and the expected norms of Xₙ are eventually bounded by C, then the limit-law norm is integrable. The proof bounds all bounded continuous norm truncations and passes to the monotone limit at the lintegral level.
Formal statement
∀ {Ω : Type u_4} {Ω' : Type u_5} {E : Type u_6} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'}
{μ : MeasureTheory.Measure Ω} [inst : MeasureTheory.IsProbabilityMeasure μ] {ν : MeasureTheory.Measure Ω'}
[inst_1 : MeasureTheory.IsProbabilityMeasure ν] [inst_2 : SeminormedAddCommGroup E] [inst_3 : MeasurableSpace E]
[inst_4 : OpensMeasurableSpace E] [BorelSpace E] [HasOuterApproxClosed E] {X : Nat → Ω → E} {Z : Ω' → E},
MeasureTheory.TendstoInDistribution X Filter.atTop Z (fun x => μ) ν →
∀ {C : Real},
Filter.Eventually
(fun n =>
And (MeasureTheory.Integrable (fun ω => inst_2.norm (X n ω)) μ)
(Real.instLE.le (MeasureTheory.integral μ fun ω => inst_2.norm (X n ω)) C))
Filter.atTop →
MeasureTheory.Integrable (fun ω => inst_2.norm (Z ω)) ν
theorem HansenEconometrics.TendstoInDistribution.integral_norm_limit_le_of_eventually_integral_norm_bound
Hansen Theorem 6.13, weak-convergence bounded first moments pass to the limit.
If Xₙ ⇒ Z and the expected norms of Xₙ are eventually bounded by C, then the limit-law expected norm is at most C.
Formal statement
∀ {Ω : Type u_4} {Ω' : Type u_5} {E : Type u_6} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'}
{μ : MeasureTheory.Measure Ω} [inst : MeasureTheory.IsProbabilityMeasure μ] {ν : MeasureTheory.Measure Ω'}
[inst_1 : MeasureTheory.IsProbabilityMeasure ν] [inst_2 : SeminormedAddCommGroup E] [inst_3 : MeasurableSpace E]
[inst_4 : OpensMeasurableSpace E] [BorelSpace E] [HasOuterApproxClosed E] {X : Nat → Ω → E} {Z : Ω' → E},
MeasureTheory.TendstoInDistribution X Filter.atTop Z (fun x => μ) ν →
∀ {C : Real},
Filter.Eventually
(fun n =>
And (MeasureTheory.Integrable (fun ω => inst_2.norm (X n ω)) μ)
(Real.instLE.le (MeasureTheory.integral μ fun ω => inst_2.norm (X n ω)) C))
Filter.atTop →
Real.instLE.le (MeasureTheory.integral ν fun ω => inst_2.norm (Z ω)) C
theorem HansenEconometrics.TendstoInDistribution.integral_normTrunc_limit_le_of_eventually_integral_norm_bound
Hansen Theorem 6.13, norm-truncation weak-moment layer.
If Xₙ ⇒ Z and the expected norms of Xₙ are eventually bounded by C, then every bounded continuous norm truncation of the limit has expectation at most C. This is the reusable truncation step toward the textbook unbounded norm statement.
Formal statement
∀ {Ω : Type u_4} {Ω' : Type u_5} {E : Type u_6} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'}
{μ : MeasureTheory.Measure Ω} [inst : MeasureTheory.IsProbabilityMeasure μ] {ν : MeasureTheory.Measure Ω'}
[inst_1 : MeasureTheory.IsProbabilityMeasure ν] [inst_2 : SeminormedAddCommGroup E] [inst_3 : MeasurableSpace E]
[inst_4 : OpensMeasurableSpace E] [BorelSpace E] [HasOuterApproxClosed E] {X : Nat → Ω → E} {Z : Ω' → E},
MeasureTheory.TendstoInDistribution X Filter.atTop Z (fun x => μ) ν →
∀ {C R : Real} (hR : Real.instLE.le 0 R),
Filter.Eventually
(fun n =>
And (MeasureTheory.Integrable (fun ω => inst_2.norm (X n ω)) μ)
(Real.instLE.le (MeasureTheory.integral μ fun ω => inst_2.norm (X n ω)) C))
Filter.atTop →
Real.instLE.le
(MeasureTheory.integral ν fun ω =>
BoundedContinuousFunction.instFunLike.coe (HansenEconometrics.normTruncBoundedContinuousFunction E R hR)
(Z ω))
CDirect statement dependencies (1)
-
HansenEconometrics.normTruncBoundedContinuousFunction
theorem HansenEconometrics.TendstoInDistribution.integral_boundedContinuous_nonneg_limit_le_of_eventually_bound
Hansen Theorem 6.13, bounded continuous weak-moment face.
If Xₙ ⇒ Z and the expectations of a nonnegative bounded continuous transform are eventually bounded by C, then the limit-law expectation of the same transform is bounded by C. This is the direct bounded-continuous Portmanteau face of bounded first moments passing to the weak limit.
Formal statement
∀ {Ω : Type u_4} {Ω' : Type u_5} {E : Type u_6} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'}
{μ : MeasureTheory.Measure Ω} [inst : MeasureTheory.IsProbabilityMeasure μ] {ν : MeasureTheory.Measure Ω'}
[inst_1 : MeasureTheory.IsProbabilityMeasure ν] [inst_2 : TopologicalSpace E] [inst_3 : MeasurableSpace E]
[inst_4 : OpensMeasurableSpace E] [HasOuterApproxClosed E] {X : Nat → Ω → E} {Z : Ω' → E},
MeasureTheory.TendstoInDistribution X Filter.atTop Z (fun x => μ) ν →
∀ (f : BoundedContinuousFunction E Real),
BoundedContinuousFunction.instPartialOrder.le 0 f →
∀ {C : Real},
Filter.Eventually
(fun n =>
Real.instLE.le (MeasureTheory.integral μ fun ω => BoundedContinuousFunction.instFunLike.coe f (X n ω))
C)
Filter.atTop →
Real.instLE.le (MeasureTheory.integral ν fun ω => BoundedContinuousFunction.instFunLike.coe f (Z ω)) C
def HansenEconometrics.normTruncBoundedContinuousFunction
Bounded continuous truncation of the norm: x ↦ min ‖x‖ R.
The nonnegative bound hR is included so the function has range in [0, R]. This is the truncation used for the weak-convergence-facing bounded-moment layer in Hansen Theorem 6.13.
Formal statement
(E : Type u_4) → [inst : SeminormedAddCommGroup E] → (R : Real) → Real.instLE.le 0 R → BoundedContinuousFunction E RealDefinition 6.4 uniform integrability3 endpoints
Z_n is uniformly integrable if \lim_{M \to \infty} \limsup_{n \to \infty} \mathbb{E}[\lVert Z_n \rVert 1\{\lVert Z_n \rVert \gt M\}] = 0
theorem HansenEconometrics.uniformIntegrable_tail_eLpNorm_one
Uniform integrability gives uniform control of large-tail L¹ seminorms.
This is the Mathlib-backed UI layer used by Hansen Theorem 6.16. The result is for a real-valued sequence Z; in the textbook application Z i is the nonnegative power variable |Y_i|^r.
Formal statement
∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {Z : Nat → Ω → Real},
MeasureTheory.UniformIntegrable Z 1 μ →
∀ {ε : Real},
Real.instLT.lt 0 ε →
Exists fun C =>
∀ (i : Nat),
ENNReal.instPartialOrder.le
(MeasureTheory.eLpNorm
((setOf fun ω => NNReal.instPartialOrder.le C (SeminormedAddGroup.toNNNorm.nnnorm (Z i ω))).indicator
(Z i))
1 μ)
(ENNReal.ofReal ε)
theorem HansenEconometrics.uniformIntegrable_one_of_tail_eLpNorm
Tail L¹ control gives Mathlib’s probability-theory uniform integrability.
This is the converse of uniformIntegrable_tail_eLpNorm_one, stated as a chapter-facing Definition 6.4 bridge.
Formal statement
∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ]
{Z : Nat → Ω → Real},
(∀ (i : Nat), MeasureTheory.AEStronglyMeasurable (Z i) μ) →
(∀ (ε : Real),
Real.instLT.lt 0 ε →
Exists fun C =>
∀ (i : Nat),
ENNReal.instPartialOrder.le
(MeasureTheory.eLpNorm
((setOf fun ω => NNReal.instPartialOrder.le C (SeminormedAddGroup.toNNNorm.nnnorm (Z i ω))).indicator
(Z i))
1 μ)
(ENNReal.ofReal ε)) →
MeasureTheory.UniformIntegrable Z 1 μ
theorem HansenEconometrics.uniformIntegrable_one_iff_tail_eLpNorm
Two-sided tail characterization of L¹ uniform integrability for real sequences, with measurability supplied explicitly for the converse direction.
Formal statement
∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ]
{Z : Nat → Ω → Real},
(∀ (i : Nat), MeasureTheory.AEStronglyMeasurable (Z i) μ) →
Iff (MeasureTheory.UniformIntegrable Z 1 μ)
(∀ (ε : Real),
Real.instLT.lt 0 ε →
Exists fun C =>
∀ (i : Nat),
ENNReal.instPartialOrder.le
(MeasureTheory.eLpNorm
((setOf fun ω => NNReal.instPartialOrder.le C (SeminormedAddGroup.toNNNorm.nnnorm (Z i ω))).indicator
(Z i))
1 μ)
(ENNReal.ofReal ε))Theorem 6.14 primitive condition for uniform integrability2 endpoints
If for some \delta \gt 0, \mathbb{E}\lVert Z_n \rVert^{1+\delta} \le C \lt \infty, then Z_n is uniformly integrable
theorem HansenEconometrics.uniformIntegrable_one_of_eLpNorm_bdd_gt_one
Hansen Theorem 6.14, uniform higher-moment UI wrapper.
If the sequence is uniformly bounded in Lᵖ for some finite exponent p > 1, then it is uniformly integrable in L¹. This is the broader textbook sufficient condition behind the iid finite-first-moment face above.
Formal statement
∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ]
{Z : Nat → Ω → Real} {p : ENNReal},
ENNReal.instPartialOrder.lt 1 p →
Ne p instTopENNReal.top →
(∀ (i : Nat), MeasureTheory.AEStronglyMeasurable (Z i) μ) →
(Exists fun B =>
∀ (i : Nat), ENNReal.instPartialOrder.le (MeasureTheory.eLpNorm (Z i) p μ) (ENNReal.ofNNReal B)) →
MeasureTheory.UniformIntegrable Z 1 μ
theorem HansenEconometrics.uniformIntegrable_one_of_identDistrib_memLp
Hansen Theorem 6.14, identically distributed L¹ UI wrapper.
An identically distributed real sequence with a finite first moment is uniformly integrable in L¹. This is the primitive moment-to-UI bridge used to feed Hansen’s maximum theorem when the power variables are iid.
Formal statement
∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ]
{Z : Nat → Ω → Real},
MeasureTheory.MemLp (Z 0) 1 μ →
(∀ (i : Nat), ProbabilityTheory.IdentDistrib (Z i) (Z 0) μ μ) → MeasureTheory.UniformIntegrable Z 1 μTheorem 6.15 convergence of moments under uniform integrability2 endpoints
If Z_n \xrightarrow{d} Z and Z_n is uniformly integrable, then \mathbb{E}[Z_n] \to \mathbb{E}[Z]
theorem HansenEconometrics.TendstoInDistribution.integral_tendsto_of_uniformIntegrable
Hansen Theorem 6.15, weak-convergence UI moment wrapper.
If Xₙ ⇒ Z and the source sequence is uniformly integrable in L¹, then the real expectations converge. The proof derives the explicit clipping-tail premise from Mathlib’s UniformIntegrable tail characterization and the limit-law integrability supplied by the bounded-first-moment weak-convergence wrapper above.
Formal statement
∀ {Ω : Type u_4} {Ω' : Type u_5} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {μ : MeasureTheory.Measure Ω}
[inst : MeasureTheory.IsProbabilityMeasure μ] {ν : MeasureTheory.Measure Ω'}
[inst_1 : MeasureTheory.IsProbabilityMeasure ν] {X : Nat → Ω → Real} {Z : Ω' → Real},
MeasureTheory.TendstoInDistribution X Filter.atTop Z (fun x => μ) ν →
MeasureTheory.UniformIntegrable X 1 μ →
Filter.Tendsto (fun n => MeasureTheory.integral μ fun ω => X n ω) Filter.atTop
(nhds (MeasureTheory.integral ν fun ω => Z ω))
theorem HansenEconometrics.tendsto_integral_of_tendstoInMeasure_uniformIntegrable
Hansen Theorem 6.15, convergence-in-measure UI moment wrapper.
If real random variables are uniformly integrable and converge in measure, then their expectations converge. This is the Vitali/convergence-in-measure face of Hansen’s moment-convergence theorem; the textbook weak-convergence version has a stronger mode-of-convergence premise than this wrapper exposes.
Formal statement
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
{Z : Nat → α → Real} {Zlim : α → Real},
MeasureTheory.UniformIntegrable Z 1 μ →
MeasureTheory.TendstoInMeasure μ Z Filter.atTop Zlim →
Filter.Tendsto (fun n => MeasureTheory.integral μ fun ω => Z n ω) Filter.atTop
(nhds (MeasureTheory.integral μ fun ω => Zlim ω))Theorem 6.16 uniform stochastic bounds for maxima5 endpoints
If \lvert Y_i \rvert^r is uniformly integrable, then n^{-1/r} \max_{1 \le i \le n} \lvert Y_i \rvert \xrightarrow{p} 0
def HansenEconometrics.maxNNNorm
Finite-sample maximum of the norms of a real-valued sequence.
Formal statement
{Ω : Type u_1} → (Nat → Ω → Real) → Nat → Ω → NNReal
def HansenEconometrics.scaledMaxNNNorm
Power-scale version of Hansen’s maximum statistic.
When Z i = |Y i| ^ r, this is n⁻¹ max_i |Y_i|^r, the natural nonnegative-power form of Theorem 6.16 before applying the rth-root CMT.
Formal statement
{Ω : Type u_1} → (Nat → Ω → Real) → Nat → Ω → Real
theorem HansenEconometrics.max_norm_scaled_tendstoInMeasure_zero_of_uniformIntegrable_norm_r
Hansen Theorem 6.16 on the nonnegative power scale.
If Z_i = |Y_i|^r is uniformly integrable in L¹, then n⁻¹ max_{i<n} |Y_i|^r converges to zero in measure. The textbook n^{-1/r} max_i |Y_i| form follows by applying the rth-root continuous mapping theorem to this nonnegative statistic.
Formal statement
∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {Z : Nat → Ω → Real},
MeasureTheory.UniformIntegrable Z 1 μ →
MeasureTheory.TendstoInMeasure μ (HansenEconometrics.scaledMaxNNNorm Z) Filter.atTop fun x => 0Direct statement dependencies (1)
-
HansenEconometrics.scaledMaxNNNorm
theorem HansenEconometrics.max_norm_scaled_tendstoInMeasure_zero_of_identDistrib_memLp
Hansen Theorem 6.16, iid finite-power-moment maximum wrapper.
If the power variables Z_i are identically distributed and Z_0 is in L¹, then n⁻¹ max_{i<n} |Z_i| on the nonnegative-power scale is oₚ(1). For Hansen’s textbook statement, use Z_i = |Y_i|^r.
Formal statement
∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ]
{Z : Nat → Ω → Real},
MeasureTheory.MemLp (Z 0) 1 μ →
(∀ (i : Nat), ProbabilityTheory.IdentDistrib (Z i) (Z 0) μ μ) →
MeasureTheory.TendstoInMeasure μ (HansenEconometrics.scaledMaxNNNorm Z) Filter.atTop fun x => 0Direct statement dependencies (1)
-
HansenEconometrics.scaledMaxNNNorm
theorem HansenEconometrics.TendstoInMeasure.sqrt_nonneg_zero_real
Square-root continuous mapping at zero for nonnegative real-valued sequences.
This avoids any additional measurability side condition by comparing the tail events {sqrt Xₙ ≥ ε} and {Xₙ ≥ ε²} directly.
Formal statement
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {X : Nat → α → Real},
(MeasureTheory.TendstoInMeasure μ X Filter.atTop fun x => 0) →
(∀ (n : Nat) (ω : α), Real.instLE.le 0 (X n ω)) →
MeasureTheory.TendstoInMeasure μ (fun n ω => (X n ω).sqrt) Filter.atTop fun x => 0