Score, Wald and likelihood-ratio tests

11 fully proved

Probability Theory

TheoremSquared normalized Gaussian is chi-square with one degree of freedom#✓fully proved

If Y ~ N(0, v) with v ≠ 0, then Y² / v ~ χ²₁.

theorem gaussianReal_map_sq_div {v : ℝ≥0} (hv : v ≠ 0) :
    (gaussianReal 0 v).map (fun x : ℝ => x ^ 2 / v) = chiSquareMeasure 1

Uses 2 · Used by 4

Statement usesChi-square distribution

Proof usesThe square of a standard normal variable is chi-square with one degree of freedom

Used byRao's score test, known information · Rao's score test with an estimated information · Wald's test · Wald's test with an estimated information

TheoremLaw of the positive part squared of a standard normal variable#✓fully proved

max(Z, 0)² has the mixture law ½ δ₀ + ½ χ²₁ (chi-bar-square with weights ½, ½).

theorem gaussianReal_map_max_zero_sq :
    (gaussianReal 0 1).map (fun x : ℝ => max x 0 ^ 2) =
      (2⁻¹ : ℝ≥0∞) • Measure.dirac 0 + (2⁻¹ : ℝ≥0∞) • chiSquareMeasure 1

Uses 2 · Used by 1

Statement usesChi-square distribution

Proof usesThe square of a standard normal variable is chi-square with one degree of freedom

Used byLikelihood ratio on the boundary

Likelihood Ratio Tests

TheoremRao's score test, known information#✓fully proved

Under the conditions of tendstoInDistribution_score and 0 < I(θ₀), the score statistic (n^{-1/2} ∑_{i<n} score p θ₀ (X i))² / I(θ₀) converges in distribution to χ²₁.

theorem tendstoInDistribution_scoreStatistic {ν : 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)
    (hI_pos : 0 < fisherInformation ν p θ₀)
    {Z : Ω' → ℝ} (hZ : HasLaw Z (chiSquareMeasure 1) P') :
    TendstoInDistribution
      (fun (n : ℕ) ω => ((√n)⁻¹ * ∑ i ∈ Finset.range n, score p θ₀ (X i ω)) ^ 2 /
        fisherInformation ν p θ₀) atTop Z (fun _ => P) P'

Sources

• Rao (1948), one-parameter case; the central limit theorem for the score as in Lehmann & Casella (1998), §6.3.

Uses 6

Statement usesFisher information · Probability law of a density family member · Score function · Chi-square distribution

Proof usesCentral limit theorem for the score · Squared normalized Gaussian is chi-square with one degree of freedom

TheoremRao's score test with an estimated information#✓fully proved

As tendstoInDistribution_scoreStatistic, with I(θ₀) replaced by any estimators Î n converging to I(θ₀) in probability. Where Î n ω = 0 the statistic takes Lean's value x / 0 = 0; this event has probability tending to 0 because 0 < I(θ₀).

theorem tendstoInDistribution_scoreStatistic_of_estimator {ν : 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)
    (hI_pos : 0 < fisherInformation ν p θ₀)
    {Ihat : ℕ → Ω → ℝ} (hIhat_meas : ∀ n, AEMeasurable (Ihat n) P)
    (hIhat : TendstoInMeasure P Ihat atTop (fun _ => fisherInformation ν p θ₀))
    {Z : Ω' → ℝ} (hZ : HasLaw Z (chiSquareMeasure 1) P') :
    TendstoInDistribution
      (fun (n : ℕ) ω => ((√n)⁻¹ * ∑ i ∈ Finset.range n, score p θ₀ (X i ω)) ^ 2 / Ihat n ω)
      atTop Z (fun _ => P) P'

Uses 7

Statement usesFisher information · Probability law of a density family member · Score function · Chi-square distribution

Proof usesCentral limit theorem for the score · Convergence to zero in probability by domination on likely events · Squared normalized Gaussian is chi-square with one degree of freedom

TheoremConsistency of the observed information#✓fully proved

For i.i.d. observations with law p θ₀ ν, if ∂_θ score p θ₀ is measurable and integrable with E ∂_θ score p θ₀ = -I(θ₀) (the information identity), then -(1/n) ∑_{i<n} ∂_θ score p θ₀ (X i) → I(θ₀) in probability.

theorem tendstoInMeasure_observedInformation {ν : Measure 𝓧} {p : ℝ → 𝓧 → ℝ} {θ₀ : ℝ}
    {X : ℕ → Ω → 𝓧} (hX_law : ∀ i, HasLaw (X i) (lawOf ν p θ₀) P) (hX_indep : iIndepFun X P)
    (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 θ₀) :
    TendstoInMeasure P
      (fun (n : ℕ) ω => -((∑ i ∈ Finset.range n, deriv (fun t => score p t (X i ω)) θ₀) / n))
      atTop (fun _ => fisherInformation ν p θ₀)

Uses 3 · Used by 2

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

Used byLocal power of the likelihood-ratio test · Quadratic expansion of the log-likelihood ratio

TheoremWald's test#✓fully proved

Under the conditions of tendstoInDistribution_sqrt_mul_sub_of_likelihoodEquation (without the normalization ∫ p θ dν = 1, which that proof does not use), the Wald statistic n (θ̂ₙ - θ₀)² I(θ₀) of a consistent root θ̂ₙ of the likelihood equation converges in distribution to χ²₁.

MathlibExt.Probability.Statistics.LikelihoodRatioTests.tendstoInDistribution_waldStatistic · 26 lines

theorem tendstoInDistribution_waldStatistic
    {ν : Measure 𝓧} {p : ℝ → 𝓧 → ℝ} {θ₀ δ : ℝ} (hδ : 0 < δ)
    (hp_pos : ∀ θ x, 0 < p θ x) (hp_meas : Measurable (p θ₀))
    {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 _ => θ₀))
    {Z : Ω' → ℝ} (hZ : HasLaw Z (chiSquareMeasure 1) P') :
    TendstoInDistribution
      (fun (n : ℕ) ω => (n : ℝ) * (θhat n ω - θ₀) ^ 2 * fisherInformation ν p θ₀)
      atTop Z (fun _ => P) P'

Sources

• Wald (1943), one-parameter case; the asymptotic normality of θ̂ₙ as in Lehmann & Casella (1998), §6.3.

Uses 7 · Used by 1

Statement usesFisher information · Probability law of a density family member · Score function · Chi-square distribution

Proof usesFisher information is the second moment of the score · Asymptotic normality of a consistent root of an estimating equation · Squared normalized Gaussian is chi-square with one degree of freedom

Used byWilks' theorem (simple null)

TheoremWald's test with an estimated information#✓fully proved

As tendstoInDistribution_waldStatistic, with I(θ₀) replaced by any estimators Î n → I(θ₀) in probability (for example the observed information of tendstoInMeasure_observedInformation; I(θ̂ₙ) also qualifies when θ ↦ I(θ) is continuous at θ₀, by the continuous mapping theorem).

MathlibExt.Probability.Statistics.LikelihoodRatioTests.tendstoInDistribution_waldStatistic_of_estimator · 28 lines

theorem tendstoInDistribution_waldStatistic_of_estimator
    {ν : Measure 𝓧} {p : ℝ → 𝓧 → ℝ} {θ₀ δ : ℝ} (hδ : 0 < δ)
    (hp_pos : ∀ θ x, 0 < p θ x) (hp_meas : Measurable (p θ₀))
    {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 _ => θ₀))
    {Ihat : ℕ → Ω → ℝ} (hIhat_meas : ∀ n, AEMeasurable (Ihat n) P)
    (hIhat : TendstoInMeasure P Ihat atTop (fun _ => fisherInformation ν p θ₀))
    {Z : Ω' → ℝ} (hZ : HasLaw Z (chiSquareMeasure 1) P') :
    TendstoInDistribution
      (fun (n : ℕ) ω => (n : ℝ) * (θhat n ω - θ₀) ^ 2 * Ihat n ω)
      atTop Z (fun _ => P) P'

Uses 7

Statement usesFisher information · Probability law of a density family member · Score function · Chi-square distribution

Proof usesFisher information is the second moment of the score · Asymptotic normality of a consistent root of an estimating equation · Squared normalized Gaussian is chi-square with one degree of freedom

TheoremQuadratic expansion of the log-likelihood ratio#✓fully proved

Let θ̂ₙ be √n-consistent (√n (θ̂ₙ - θ₀) converges in distribution) and solve the likelihood equation with probability tending to one. If on the ball of radius δ > 0 about θ₀ the log-likelihood is twice differentiable in θ with |∂³_θ log p θ x| ≤ M x for an integrable M, and ∂²_θ log p θ₀ is integrable with mean -I(θ₀), then 2 (ℓₙ(θ̂ₙ) - ℓₙ(θ₀)) - n (θ̂ₙ - θ₀)² I(θ₀) → 0 in probability, where ℓₙ θ = ∑_{i<n} log p θ (X i).

The positivity of p is not used: the expansion holds for any criterion log p θ x with these derivatives, and the theorems below assume 0 < p θ x.

MathlibExt.Probability.Statistics.LikelihoodRatioTests.tendstoInMeasure_two_mul_logLikelihood_sub_sub · 25 lines

theorem tendstoInMeasure_two_mul_logLikelihood_sub_sub
    {ν : Measure 𝓧} {p : ℝ → 𝓧 → ℝ} {θ₀ δ : ℝ} (hδ : 0 < δ)
    {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 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 θ₀)
    {θ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 : Ω' → ℝ}
    (hT : TendstoInDistribution (fun (n : ℕ) ω => √n * (θhat n ω - θ₀)) atTop Y
      (fun _ => P) P') :
    TendstoInMeasure P
      (fun (n : ℕ) ω => 2 * ∑ i ∈ Finset.range n,
          (Real.log (p (θhat n ω) (X i ω)) - Real.log (p θ₀ (X i ω))) -
        (n : ℝ) * (θhat n ω - θ₀) ^ 2 * fisherInformation ν p θ₀)
      atTop 0

Sources

• the second-order expansion of Wilks (1938); van der Vaart (1998), ch. 16.

Uses 6 · Used by 2

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

Proof usesConsistency of the observed information · Product 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

TheoremWilks' theorem (simple null)#✓fully proved

Under the conditions of tendstoInDistribution_waldStatistic and joint measurability of (θ, x) ↦ p θ x, the log-likelihood-ratio statistic 2 (ℓₙ(θ̂ₙ) - ℓₙ(θ₀)), ℓₙ θ = ∑_{i<n} log p θ (X i), of a consistent root θ̂ₙ of the likelihood equation converges in distribution to χ²₁.

MathlibExt.Probability.Statistics.LikelihoodRatioTests.tendstoInDistribution_two_mul_logLikelihood_sub · 27 lines

theorem tendstoInDistribution_two_mul_logLikelihood_sub
    {ν : Measure 𝓧} {p : ℝ → 𝓧 → ℝ} {θ₀ δ : ℝ} (hδ : 0 < δ)
    (hp_pos : ∀ θ x, 0 < p θ x) (hp_meas : Measurable (Function.uncurry p))
    {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 _ => θ₀))
    {Z : Ω' → ℝ} (hZ : HasLaw Z (chiSquareMeasure 1) P') :
    TendstoInDistribution
      (fun (n : ℕ) ω => 2 * ∑ i ∈ Finset.range n,
        (Real.log (p (θhat n ω) (X i ω)) - Real.log (p θ₀ (X i ω))))
      atTop Z (fun _ => P) P'

Sources

• Wilks (1938), case of a one-dimensional parameter and a simple null hypothesis; van der Vaart (1998), ch. 16.

Uses 8 · Used by 1

Statement usesFisher information · Probability law of a density family member · Score function · Chi-square distribution

Proof usesWald's test · Quadratic expansion of the log-likelihood ratio · Fisher information is the second moment of the score · Asymptotic normality of a consistent root of an estimating equation

Used byWilks' theorem, supremum form

TheoremWilks' theorem, supremum form#✓fully proved

If moreover θ̂ₙ ω maximizes the log-likelihood ℓₙ θ = ∑_{i<n} log p θ (X i ω) over all θ for every n and ω, then the likelihood-ratio statistic 2 (sup_θ ℓₙ θ - ℓₙ θ₀) converges in distribution to χ²₁.

MathlibExt.Probability.Statistics.LikelihoodRatioTests.tendstoInDistribution_two_mul_iSup_logLikelihood_sub · 29 lines

theorem tendstoInDistribution_two_mul_iSup_logLikelihood_sub
    {ν : Measure 𝓧} {p : ℝ → 𝓧 → ℝ} {θ₀ δ : ℝ} (hδ : 0 < δ)
    (hp_pos : ∀ θ x, 0 < p θ x) (hp_meas : Measurable (Function.uncurry p))
    {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 _ => θ₀))
    (hmax : ∀ n ω θ, ∑ i ∈ Finset.range n, Real.log (p θ (X i ω)) ≤
      ∑ i ∈ Finset.range n, Real.log (p (θhat n ω) (X i ω)))
    {Z : Ω' → ℝ} (hZ : HasLaw Z (chiSquareMeasure 1) P') :
    TendstoInDistribution
      (fun (n : ℕ) ω => 2 * ((⨆ θ, ∑ i ∈ Finset.range n, Real.log (p θ (X i ω))) -
        ∑ i ∈ Finset.range n, Real.log (p θ₀ (X i ω))))
      atTop Z (fun _ => P) P'

Uses 5

Statement usesFisher information · Probability law of a density family member · Score function · Chi-square distribution

Proof usesWilks' theorem (simple null)

TheoremLikelihood ratio on the boundary#✓fully proved

Likelihood ratio on the boundary (one-sided parameter space θ ∈ [0, ∞), true value θ₀ = 0). Let the model be defined and regular on a ball about 0 as in tendstoInDistribution_two_mul_logLikelihood_sub (so 0 is interior to the domain of the family, though not to the parameter space), and let θ̂ₙ be a consistent root of the likelihood equation. The statistic 2 (ℓₙ(max θ̂ₙ 0) - ℓₙ(0)) of the estimator projected onto [0, ∞) converges in distribution to the mixture ½ δ₀ + ½ χ²₁. The projection max θ̂ₙ 0 is the restricted maximizer when, for example, ℓₙ is concave; that is not assumed here.

MathlibExt.Probability.Statistics.LikelihoodRatioTests.tendstoInDistribution_two_mul_logLikelihood_max_zero_sub · 28 lines

theorem tendstoInDistribution_two_mul_logLikelihood_max_zero_sub
    {ν : Measure 𝓧} {p : ℝ → 𝓧 → ℝ} {δ : ℝ} (hδ : 0 < δ)
    (hp_pos : ∀ θ x, 0 < p θ x) (hp_meas : Measurable (Function.uncurry p))
    {X : ℕ → Ω → 𝓧} (hX_law : ∀ i, HasLaw (X i) (lawOf ν p 0) P) (hX_indep : iIndepFun X P)
    (hℓ_diff : ∀ x, ∀ θ ∈ Metric.ball 0 δ, DifferentiableAt ℝ (fun t => Real.log (p t x)) θ)
    (hs_diff : ∀ x, ∀ θ ∈ Metric.ball 0 δ, DifferentiableAt ℝ (fun t => score p t x) θ)
    (hs'_diff : ∀ x, ∀ θ ∈ Metric.ball 0 δ,
      DifferentiableAt ℝ (fun t => deriv (fun s => score p s x) t) θ)
    {M : 𝓧 → ℝ} (hM_meas : Measurable M) (hM_int : Integrable M (lawOf ν p 0))
    (hM : ∀ x, ∀ θ ∈ Metric.ball 0 δ,
      |deriv (fun t => deriv (fun s => score p s x) t) θ| ≤ M x)
    (hs_meas : Measurable (score p 0))
    (hs_sq : Integrable (fun x => score p 0 x ^ 2) (lawOf ν p 0))
    (hs_mean : ∫ x, score p 0 x ∂lawOf ν p 0 = 0)
    (hs'_meas : Measurable fun x => deriv (fun t => score p t x) 0)
    (hs'_int : Integrable (fun x => deriv (fun t => score p t x) 0) (lawOf ν p 0))
    (h_info : ∫ x, deriv (fun t => score p t x) 0 ∂lawOf ν p 0 = -fisherInformation ν p 0)
    (hI_pos : 0 < fisherInformation ν p 0)
    {θ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 _ => 0))
    {Z : Ω' → ℝ}
    (hZ : HasLaw Z ((2⁻¹ : ℝ≥0∞) • Measure.dirac 0 + (2⁻¹ : ℝ≥0∞) • chiSquareMeasure 1) P') :
    TendstoInDistribution
      (fun (n : ℕ) ω => 2 * ∑ i ∈ Finset.range n,
        (Real.log (p (max (θhat n ω) 0) (X i ω)) - Real.log (p 0 (X i ω))))
      atTop Z (fun _ => P) P'

Sources

• Chernoff (1954); van der Vaart (1998), ch. 16.

Uses 9

Statement usesFisher information · Probability law of a density family member · Score function · Chi-square distribution

Proof usesQuadratic expansion of the log-likelihood ratio · Fisher information is the second moment of the score · Asymptotic normality of a consistent root of an estimating equation · Convergence to zero in probability by domination on likely events · Law of the positive part squared of a standard normal variable

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.