Asymptotic normality of maximum likelihood

7 fully proved

Measure Theory

TheoremProduct of a distributionally convergent and a vanishing sequence#✓fully proved

A sequence A i converging in distribution, times a sequence η i converging in probability to 0, converges in probability to 0 (a consequence of Slutsky's theorem).

theorem TendstoInDistribution.mul_tendstoInMeasure_zero [IsProbabilityMeasure P]
    [IsProbabilityMeasure P'] [l.IsCountablyGenerated] {A η : ι → Ω → ℝ} {Z : Ω' → ℝ}
    (hA : TendstoInDistribution A l Z (fun _ => P) P') (hη : TendstoInMeasure P η l 0)
    (hη_meas : ∀ i, AEMeasurable (η i) P) :
    TendstoInMeasure P (fun i ω => A i ω * η i ω) l 0

Uses 1 · Used by 3

Proof usesConvergence in distribution to a constant implies convergence in probability

Used byWilks' expansion for a triangular array · Quadratic expansion of the log-likelihood ratio · Asymptotic normality of a consistent root of an estimating equation

TheoremConvergence to zero in probability by domination on likely events#✓fully proved

If |W i| ≤ V i on events G i whose complements have probability tending to 0, and V i tends to 0 in probability, then W i tends to 0 in probability.

theorem tendstoInMeasure_zero_of_abs_le {W V : ι → Ω → ℝ} {G : ι → Set Ω}
    (hV : TendstoInMeasure P V l 0) (hG : Tendsto (fun i => P (G i)ᶜ) l (𝓝 0))
    (hle : ∀ i, ∀ ω ∈ G i, |W i ω| ≤ V i ω) :
    TendstoInMeasure P W l 0

Used by 5

Used byWilks' expansion for a triangular array · Rao's score test with an estimated information · Likelihood ratio on the boundary · Quadratic expansion of the log-likelihood ratio · Asymptotic normality of a consistent root of an estimating equation

Asymptotic normality of the MLE

DefinitionScore function#✓fully proved

The score ∂_θ log p θ x of a one-parameter family of densities p.

noncomputable def score (p : ℝ → 𝓧 → ℝ) (θ : ℝ) (x : 𝓧) : ℝ :=
  deriv (fun t => Real.log (p t x)) θ

Used by 15

Used byWilks' expansion for a triangular array · Local power of the likelihood-ratio test · Local asymptotic normality of the log-likelihood ratio · Rao's score test, known information · Rao's score test with an estimated information · Wilks' theorem, supremum form · Wilks' theorem (simple null) · Likelihood ratio on the boundary · Wald's test · Wald's test with an estimated information · Consistency of the observed information · Quadratic expansion of the log-likelihood ratio · Fisher information is the second moment of the score · Central limit theorem for the score · Asymptotic normality of consistent roots of the likelihood equation

TheoremFisher information is the second moment of the score#✓fully proved

For a positive density family, E_θ [score²] = I(θ): the Fisher information of FisherInformation.fisherInformation is the second moment of the score under p θ ν.

theorem integral_score_sq {ν : Measure 𝓧} {p : ℝ → 𝓧 → ℝ} {θ : ℝ}
    (hp_pos : ∀ x, 0 < p θ x) (hp_meas : Measurable (p θ))
    (hp_diff : ∀ x, DifferentiableAt ℝ (fun t => p t x) θ) :
    ∫ x, score p θ x ^ 2 ∂lawOf ν p θ = fisherInformation ν p θ

Uses 3 · Used by 6

Statement usesFisher information · Probability law of a density family member · Score function

Used byWilks' theorem (simple null) · Likelihood ratio on the boundary · Wald's test · Wald's test with an estimated information · Central limit theorem for the score · Asymptotic normality of consistent roots of the likelihood equation

TheoremCentral limit theorem for the score#✓fully proved

For i.i.d. observations with law p θ₀ ν, a positive density family differentiable in θ at θ₀, a measurable score with mean zero and ∫ score² d(p θ₀ ν) < ∞, the normalized score n^{-1/2} ∑_{i<n} score p θ₀ (X i) converges in distribution to N(0, I(θ₀)).

theorem tendstoInDistribution_score {ν : Measure 𝓧} {p : ℝ → 𝓧 → ℝ} {θ₀ : ℝ}
    (hp_pos : ∀ x, 0 < p θ₀ x) (hp_meas : Measurable (p θ₀))
    (hp_diff : ∀ x, DifferentiableAt ℝ (fun t => p t x) θ₀)
    {X : ℕ → Ω → 𝓧} (hX_law : ∀ i, HasLaw (X i) (lawOf ν p θ₀) P) (hX_indep : iIndepFun X P)
    (hs_meas : Measurable (score p θ₀))
    (hs_sq : Integrable (fun x => score p θ₀ x ^ 2) (lawOf ν p θ₀))
    (hs_mean : ∫ x, score p θ₀ x ∂lawOf ν p θ₀ = 0)
    {Y : Ω' → ℝ} (hY : HasLaw Y (gaussianReal 0 (fisherInformation ν p θ₀).toNNReal) P') :
    TendstoInDistribution
      (fun (n : ℕ) ω => (√n)⁻¹ * ∑ i ∈ Finset.range n, score p θ₀ (X i ω)) atTop Y
      (fun _ => P) P'

Sources

• Lehmann & Casella (1998), §6.3; van der Vaart (1998), ch. 5.

Uses 4 · Used by 3

Statement usesFisher information · Probability law of a density family member · Score function

Proof usesFisher information is the second moment of the score

Used byLocal power of the likelihood-ratio test · Rao's score test, known information · Rao's score test with an estimated information

TheoremAsymptotic normality of a consistent root of an estimating equation#✓fully proved

Asymptotic normality of a consistent root of an estimating equation (one-dimensional Z-estimator under Cramér-type conditions). Let X 0, X 1, … be i.i.d. with law μX and let ψ θ x satisfy, for every x and every θ in the ball of radius δ > 0 about θ₀: ψ · x and ∂_θ ψ · x are differentiable at θ, and |∂²_θ ψ θ x| ≤ M x with M integrable. Assume E ψ θ₀ = 0, E ψ θ₀² < ∞, ∂_θ ψ θ₀ integrable with E ∂_θ ψ θ₀ ≠ 0. Let θhat n be estimators that solve ∑_{i<n} ψ θ (X i) = 0 with probability tending to one and converge to θ₀ in probability. Then √n (θhat n - θ₀) converges in distribution to N(0, E ψ θ₀² / (E ∂_θ ψ θ₀)²).

MathlibExt.Probability.Statistics.MLEAsymptoticNormality.tendstoInDistribution_sqrt_mul_sub_of_estimatingEquation · 23 lines

theorem tendstoInDistribution_sqrt_mul_sub_of_estimatingEquation
    {μX : Measure 𝓧} {X : ℕ → Ω → 𝓧} (hX_law : ∀ i, HasLaw (X i) μX P)
    (hX_indep : iIndepFun X P)
    {ψ : ℝ → 𝓧 → ℝ} {θ₀ δ : ℝ} (hδ : 0 < δ)
    (hψ_diff : ∀ x, ∀ θ ∈ Metric.ball θ₀ δ, DifferentiableAt ℝ (fun t => ψ t x) θ)
    (hψ'_diff : ∀ x, ∀ θ ∈ Metric.ball θ₀ δ,
      DifferentiableAt ℝ (fun t => deriv (fun s => ψ s x) t) θ)
    {M : 𝓧 → ℝ} (hM_meas : Measurable M) (hM_int : Integrable M μX)
    (hM : ∀ x, ∀ θ ∈ Metric.ball θ₀ δ,
      |deriv (fun t => deriv (fun s => ψ s x) t) θ| ≤ M x)
    (hψ_meas : Measurable (ψ θ₀)) (hψ_sq : Integrable (fun x => ψ θ₀ x ^ 2) μX)
    (hψ_mean : ∫ x, ψ θ₀ x ∂μX = 0)
    (hψ'_meas : Measurable fun x => deriv (fun t => ψ t x) θ₀)
    (hψ'_int : Integrable (fun x => deriv (fun t => ψ t x) θ₀) μX)
    (hJ : ∫ x, deriv (fun t => ψ t x) θ₀ ∂μX ≠ 0)
    {θhat : ℕ → Ω → ℝ} (hθ_meas : ∀ n, AEMeasurable (θhat n) P)
    (hroot : Tendsto (fun n => P {ω | ∑ i ∈ Finset.range n, ψ (θhat n ω) (X i ω) ≠ 0})
      atTop (𝓝 0))
    (hcons : TendstoInMeasure P θhat atTop (fun _ => θ₀))
    {Y : Ω' → ℝ}
    (hY : HasLaw Y (gaussianReal 0 ((∫ x, ψ θ₀ x ^ 2 ∂μX) /
      (∫ x, deriv (fun t => ψ t x) θ₀ ∂μX) ^ 2).toNNReal) P') :
    TendstoInDistribution (fun (n : ℕ) ω => √n * (θhat n ω - θ₀)) atTop Y (fun _ => P) P'

Sources

• van der Vaart (1998), Theorem 5.41 (one-dimensional case, with the third-derivative envelope of Cramér (1946), §33.3); Lehmann & Casella (1998), §6.3.

Uses 2 · Used by 5

Proof usesProduct of a distributionally convergent and a vanishing sequence · Convergence to zero in probability by domination on likely events

Used byWilks' theorem (simple null) · Likelihood ratio on the boundary · Wald's test · Wald's test with an estimated information · Asymptotic normality of consistent roots of the likelihood equation

TheoremAsymptotic normality of consistent roots of the likelihood equation#✓fully proved

Asymptotic normality of consistent roots of the likelihood equation (Cramér's conditions). Let p θ be positive densities with respect to ν, and on the ball of radius δ > 0 about θ₀ let each p θ be measurable with ∫ p θ dν = 1, so that the family is a statistical model there (as in FisherInformation.cramerRao). The proof uses measurability only at θ₀ and does not use the normalization _hp_int: the limit theorem holds for roots of any criterion with these derivatives. Let X 0, X 1, … be i.i.d. with law p θ₀ ν. Assume that on the same ball the log-likelihood log p θ x is differentiable in θ for every x (so that score p θ x is its true derivative there, not Lean's junk value 0 of deriv at a nondifferentiable point) and the score ∂_θ log p θ x is twice differentiable in θ for every x, with |∂³_θ log p θ x| ≤ M x for an integrable M; that the score ∂_θ log p θ₀ is measurable and square integrable with mean zero; that ∂²_θ log p θ₀ is measurable and integrable with E ∂²_θ log p θ₀ = -I(θ₀) (the information identity); and that 0 < I(θ₀). The two moment identities are what differentiating ∫ p θ dν = 1 twice under the integral sign gives; they are assumed directly. Let θhat n be estimators that solve the likelihood equation ∑_{i<n} ∂_θ log p θ (X i) = 0 with probability tending to one and converge to θ₀ in probability. Then √n (θhat n - θ₀) → N(0, 1 / I(θ₀)) in distribution. The roots need not maximize the likelihood; for a maximum-likelihood estimator, consistency and the likelihood equation must be established separately (for example, from an interior maximum of a differentiable likelihood).

MathlibExt.Probability.Statistics.MLEAsymptoticNormality.tendstoInDistribution_sqrt_mul_sub_of_likelihoodEquation · 25 lines

theorem tendstoInDistribution_sqrt_mul_sub_of_likelihoodEquation
    {ν : Measure 𝓧} {p : ℝ → 𝓧 → ℝ} {θ₀ δ : ℝ} (hδ : 0 < δ)
    (hp_pos : ∀ θ x, 0 < p θ x) (hp_meas : ∀ θ ∈ Metric.ball θ₀ δ, Measurable (p θ))
    (_hp_int : ∀ θ ∈ Metric.ball θ₀ δ, ∫ x, p θ x ∂ν = 1)
    {X : ℕ → Ω → 𝓧} (hX_law : ∀ i, HasLaw (X i) (lawOf ν p θ₀) P) (hX_indep : iIndepFun X P)
    (hℓ_diff : ∀ x, ∀ θ ∈ Metric.ball θ₀ δ, DifferentiableAt ℝ (fun t => Real.log (p t x)) θ)
    (hs_diff : ∀ x, ∀ θ ∈ Metric.ball θ₀ δ, DifferentiableAt ℝ (fun t => score p t x) θ)
    (hs'_diff : ∀ x, ∀ θ ∈ Metric.ball θ₀ δ,
      DifferentiableAt ℝ (fun t => deriv (fun s => score p s x) t) θ)
    {M : 𝓧 → ℝ} (hM_meas : Measurable M) (hM_int : Integrable M (lawOf ν p θ₀))
    (hM : ∀ x, ∀ θ ∈ Metric.ball θ₀ δ,
      |deriv (fun t => deriv (fun s => score p s x) t) θ| ≤ M x)
    (hs_meas : Measurable (score p θ₀))
    (hs_sq : Integrable (fun x => score p θ₀ x ^ 2) (lawOf ν p θ₀))
    (hs_mean : ∫ x, score p θ₀ x ∂lawOf ν p θ₀ = 0)
    (hs'_meas : Measurable fun x => deriv (fun t => score p t x) θ₀)
    (hs'_int : Integrable (fun x => deriv (fun t => score p t x) θ₀) (lawOf ν p θ₀))
    (h_info : ∫ x, deriv (fun t => score p t x) θ₀ ∂lawOf ν p θ₀ = -fisherInformation ν p θ₀)
    (hI_pos : 0 < fisherInformation ν p θ₀)
    {θhat : ℕ → Ω → ℝ} (hθ_meas : ∀ n, AEMeasurable (θhat n) P)
    (hroot : Tendsto (fun n => P {ω | ∑ i ∈ Finset.range n, score p (θhat n ω) (X i ω) ≠ 0})
      atTop (𝓝 0))
    (hcons : TendstoInMeasure P θhat atTop (fun _ => θ₀))
    {Y : Ω' → ℝ} (hY : HasLaw Y (gaussianReal 0 (fisherInformation ν p θ₀)⁻¹.toNNReal) P') :
    TendstoInDistribution (fun (n : ℕ) ω => √n * (θhat n ω - θ₀)) atTop Y (fun _ => P) P'

Sources

• Cramér (1946), §33.3; Lehmann & Casella (1998), Theorem 6.3.10; van der Vaart (1998), Theorem 5.41.

Uses 5

Statement usesFisher information · Probability law of a density family member · Score function

Proof usesFisher information is the second moment of the score · Asymptotic normality of a consistent root of an estimating equation

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.