Local power of the likelihood-ratio test

TheoremReweighting an infinite product measure by a product density#✓fully proved

If μ.withDensity r is a probability measure, then reweighting the product measure μ^ℕ by ∏_{i<n} r (xᵢ) and projecting onto the first n coordinates gives the product measure (μ.withDensity r)^n.

theorem map_withDensity_infinitePi_prod {μ : Measure 𝓧} [IsProbabilityMeasure μ]
    {r : 𝓧 → ℝ≥0∞} (hr : Measurable r) [IsProbabilityMeasure (μ.withDensity r)] (n : ℕ) :
    ((Measure.infinitePi fun _ : ℕ => μ).withDensity
        fun x => ∏ i ∈ Finset.range n, r (x i)).map (fun x (i : Fin n) => x i) =
      Measure.pi fun _ : Fin n => μ.withDensity r

Used by 1

Used byLocal power of the likelihood-ratio test

TheoremLocal asymptotic normality of the log-likelihood ratio#✓fully proved

Suppose that on the ball of radius δ > 0 about θ₀ the log-likelihood log p θ x is differentiable in θ, the score ∂_θ log p θ x is twice differentiable in θ, and |∂³_θ log p θ x| ≤ M x. Let Y 0, Y 1, … be random variables such that -(n⁻¹ ∑_{i<n} ∂²_θ log p θ₀ (Y i)) → I and n⁻¹ ∑_{i<n} M (Y i) → c in probability (laws of large numbers). Then, for the local parameters θₙ = θ₀ + h / √n, ∑_{i<n} (log p θₙ (Y i) - log p θ₀ (Y i)) - h n^{-1/2} ∑_{i<n} ∂_θ log p θ₀ (Y i) converges to -h² I / 2 in probability.

MathlibExt.Probability.Statistics.LikelihoodRatioLocalPower.tendstoInMeasure_logLikelihoodRatio_sub · 19 lines

theorem tendstoInMeasure_logLikelihoodRatio_sub {p : ℝ → 𝓧 → ℝ} {θ₀ δ h I c : ℝ}
    (hδ : 0 < δ)
    (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 : ∀ x, ∀ θ ∈ Metric.ball θ₀ δ,
      |deriv (fun t => deriv (fun s => score p s x) t) θ| ≤ M x)
    {Y : ℕ → Ω → 𝓧}
    (hB : TendstoInMeasure P
      (fun (n : ℕ) ω => -((∑ i ∈ Finset.range n, deriv (fun t => score p t (Y i ω)) θ₀) / n))
      atTop (fun _ => I))
    (hMb : TendstoInMeasure P (fun (n : ℕ) ω => (∑ i ∈ Finset.range n, M (Y i ω)) / n)
      atTop (fun _ => c)) :
    TendstoInMeasure P
      (fun (n : ℕ) ω => ∑ i ∈ Finset.range n,
          (Real.log (p (θ₀ + h / √n) (Y i ω)) - Real.log (p θ₀ (Y i ω))) -
        h * ((√n)⁻¹ * ∑ i ∈ Finset.range n, score p θ₀ (Y i ω)))
      atTop (fun _ => -(h ^ 2 * I / 2))

Sources

• van der Vaart (1998), Theorem 7.2 (local asymptotic normality), here under Cramér's third-derivative envelope instead of differentiability in quadratic mean.

Uses 1 · Used by 1

Statement usesScore function

Used byLocal power of the likelihood-ratio test

TheoremWilks' expansion for a triangular array#✓fully proved

Let X n i be random variables (row n is the sample of size n) and θ̂ₙ estimators that solve the likelihood equation ∑_{i<n} ∂_θ log p θ (X n i) = 0 with probability tending to one and converge to θ₀ in probability. Suppose that on the ball of radius δ > 0 about θ₀ the log-likelihood is differentiable in θ, the score is twice differentiable, and |∂³_θ log p θ x| ≤ M x. Assume the laws of large numbers -(n⁻¹ ∑_{i<n} ∂²_θ log p θ₀ (X n i)) → I with I > 0 and n⁻¹ ∑_{i<n} M (X n i) → c in probability, and that the normalized score n^{-1/2} ∑_{i<n} ∂_θ log p θ₀ (X n i) converges in distribution to Y. Then 2 (ℓₙ(θ̂ₙ) - ℓₙ(θ₀)) → Y² / I in distribution, where ℓₙ θ = ∑_{i<n} log p θ (X n i).

No independence or distributional assumption on the rows is made: they enter only through the three limit hypotheses. The positivity of p is not used either: the expansion holds for any criterion log p θ x with these derivatives. For i.i.d. rows with law p θ₀ ν this is Wilks' theorem; under local alternatives it gives the local power (tendstoInDistribution_two_mul_logLikelihood_sub_local).

MathlibExt.Probability.Statistics.LikelihoodRatioLocalPower.tendstoInDistribution_two_mul_logLikelihood_sub_of_triangular · 30 lines

theorem tendstoInDistribution_two_mul_logLikelihood_sub_of_triangular
    {p : ℝ → 𝓧 → ℝ} {θ₀ δ I c : ℝ} (hδ : 0 < δ) (hI : 0 < I)
    (hp_meas : Measurable (Function.uncurry 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 : ∀ x, ∀ θ ∈ Metric.ball θ₀ δ,
      |deriv (fun t => deriv (fun s => score p s x) t) θ| ≤ M x)
    {X : ℕ → ℕ → Ω → 𝓧} (hX : ∀ n i, AEMeasurable (X n i) P)
    {θhat : ℕ → Ω → ℝ} (hθ_meas : ∀ n, AEMeasurable (θhat n) P)
    (hroot : Tendsto
      (fun n => P {ω | ∑ i ∈ Finset.range n, score p (θhat n ω) (X n i ω) ≠ 0}) atTop (𝓝 0))
    (hcons : TendstoInMeasure P θhat atTop (fun _ => θ₀))
    {Y : Ω' → ℝ}
    (hA : TendstoInDistribution
      (fun (n : ℕ) ω => (√n)⁻¹ * ∑ i ∈ Finset.range n, score p θ₀ (X n i ω)) atTop Y
      (fun _ => P) P')
    (hB : TendstoInMeasure P
      (fun (n : ℕ) ω => -((∑ i ∈ Finset.range n, deriv (fun t => score p t (X n i ω)) θ₀) / n))
      atTop (fun _ => I))
    (hB_meas : ∀ n : ℕ, AEMeasurable
      (fun ω => -((∑ i ∈ Finset.range n, deriv (fun t => score p t (X n i ω)) θ₀) / n)) P)
    (hMb : TendstoInMeasure P (fun (n : ℕ) ω => (∑ i ∈ Finset.range n, M (X n i ω)) / n)
      atTop (fun _ => c))
    (hMb_meas : ∀ n : ℕ, AEMeasurable (fun ω => (∑ i ∈ Finset.range n, M (X n i ω)) / n) P) :
    TendstoInDistribution
      (fun (n : ℕ) ω => 2 * ∑ i ∈ Finset.range n,
        (Real.log (p (θhat n ω) (X n i ω)) - Real.log (p θ₀ (X n i ω))))
      atTop (fun ω => Y ω ^ 2 / I) (fun _ => P) P'

Sources

• Wilks (1938); van der Vaart (1998), Theorem 5.41 and ch. 16.

Uses 3 · Used by 1

Statement usesScore function

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

Used byLocal power of the likelihood-ratio test

TheoremLocal power of the likelihood-ratio test#✓fully proved

Let row n of the triangular array X n 0, X n 1, … be i.i.d. with law p θₙ ν, θₙ = θ₀ + h / √n, under the Cramér conditions at θ₀ of LikelihoodRatioTests.tendstoInDistribution_two_mul_logLikelihood_sub (all moment and envelope conditions are under the null law p θ₀ ν). If θ̂ₙ solves the likelihood equation for row n with probability tending to one and θ̂ₙ → θ₀ in probability, then 2 (ℓₙ(θ̂ₙ) - ℓₙ(θ₀)) converges in distribution to the law of (Z + h √I(θ₀))², Z ~ N(0, 1) (noncentral χ²₁ with noncentrality h² I(θ₀)). For h = 0 this is Wilks' theorem for a triangular array.

The row n = 0 is irrelevant for the limit; with Lean's h / √0 = 0 its law is p θ₀ ν, which makes p θ₀ ν a probability measure. No normalization ∫ p θ dν = 1 is assumed otherwise: the laws p θₙ ν are probability measures because they are laws of random variables.

MathlibExt.Probability.Statistics.LikelihoodRatioLocalPower.tendstoInDistribution_two_mul_logLikelihood_sub_local · 31 lines

theorem tendstoInDistribution_two_mul_logLikelihood_sub_local
    {ν : Measure 𝓧} {p : ℝ → 𝓧 → ℝ} {θ₀ δ h : ℝ} (hδ : 0 < δ)
    (hp_pos : ∀ θ x, 0 < p θ x) (hp_meas : Measurable (Function.uncurry p))
    {X : ℕ → ℕ → Ω → 𝓧}
    (hX_law : ∀ n i, HasLaw (X n i) (lawOf ν p (θ₀ + h / √n)) P)
    (hX_indep : ∀ n, iIndepFun (X n) 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 n i ω) ≠ 0}) atTop (𝓝 0))
    (hcons : TendstoInMeasure P θhat atTop (fun _ => θ₀))
    {Z : Ω' → ℝ}
    (hZ : HasLaw Z ((gaussianReal (h * √(fisherInformation ν p θ₀)) 1).map
      (fun x : ℝ => x ^ 2)) P') :
    TendstoInDistribution
      (fun (n : ℕ) ω => 2 * ∑ i ∈ Finset.range n,
        (Real.log (p (θhat n ω) (X n i ω)) - Real.log (p θ₀ (X n i ω))))
      atTop Z (fun _ => P) P'

Sources

• van der Vaart (1998), ch. 16 (local power), via local asymptotic normality (ch. 7) and Le Cam's first and third lemmas (ch. 6).

Uses 12

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

Proof usesContiguity of sequences of measures · Contiguity transfers convergence in probability · Le Cam's first lemma · Le Cam's third lemma · Reweighting an infinite product measure by a product density · Wilks' expansion for a triangular array · Local asymptotic normality of the log-likelihood ratio · Consistency of the observed information · Central limit theorem for the score

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.