Fisher information and the Cramér–Rao bound

DefinitionFisher information#✓fully proved

The Fisher information at θ of the one-parameter family of densities p θ with respect to ν: ∫ (∂_θ p θ x)² / p θ x dν(x). Points with p θ x = 0 contribute 0 (for a nonnegative family, ∂_θ p θ x = 0 there).

noncomputable def fisherInformation (ν : Measure 𝓧) (p : ℝ → 𝓧 → ℝ) (θ : ℝ) : ℝ :=
  ∫ x, deriv (fun θ' => p θ' x) θ ^ 2 / p θ x ∂ν

Used by 16

Used byLocal power of the likelihood-ratio test · 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 · Cramér–Rao inequality · Cramér–Rao inequality · Cramér–Rao inequality, multiplicative form

DefinitionProbability law of a density family member#✓fully proved

The probability law with density p θ with respect to ν.

noncomputable def lawOf {Θ : Type*} (ν : Measure 𝓧) (p : Θ → 𝓧 → ℝ) (θ : Θ) : Measure 𝓧 :=
  ν.withDensity fun x => ENNReal.ofReal (p θ x)

Used by 14

Used byLocal power of the likelihood-ratio test · 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 · Wald's consistency theorem for maximum likelihood

TheoremCramér–Rao inequality, multiplicative form#✓fully proved

Under the hypotheses of cramerRao_general, g'(θ)² ≤ I(θ) · Var_θ T. Unlike the quotient form, this is informative when I(θ) = 0: it then says g'(θ) = 0.

theorem sq_deriv_le_fisherInformation_mul {ν : Measure 𝓧} {p : ℝ → 𝓧 → ℝ} {T : 𝓧 → ℝ}
    {g : ℝ → ℝ} {θ : ℝ}
    (hp_nonneg : ∀ θ' x, 0 ≤ p θ' x)
    (hp_int : ∀ᶠ θ' in 𝓝 θ, ∫ x, p θ' x ∂ν = 1)
    (hs_meas : AEStronglyMeasurable (fun x => deriv (fun θ' => p θ' x) θ) ν)
    (hI_int : Integrable (fun x => deriv (fun θ' => p θ' x) θ ^ 2 / p θ x) ν)
    (hT_meas : AEStronglyMeasurable T ν)
    (hT_sq : Integrable (fun x => T x ^ 2 * p θ x) ν)
    (h_unbiased : ∀ᶠ θ' in 𝓝 θ, ∫ x, T x * p θ' x ∂ν = g θ')
    (h_deriv_one : HasDerivAt (fun θ' => ∫ x, p θ' x ∂ν)
      (∫ x, deriv (fun θ' => p θ' x) θ ∂ν) θ)
    (h_deriv_T : HasDerivAt (fun θ' => ∫ x, T x * p θ' x ∂ν)
      (∫ x, T x * deriv (fun θ' => p θ' x) θ ∂ν) θ) :
    deriv g θ ^ 2 ≤ fisherInformation ν p θ * ∫ x, (T x - g θ) ^ 2 * p θ x ∂ν

Sources

• Cramér (1946), ch. 32; Rao (1945); Lehmann & Casella (1998), ch. 2.

Uses 1 · Used by 1

Statement usesFisher information

Used byCramér–Rao inequality

TheoremCramér–Rao inequality#✓fully proved

Cramér–Rao inequality, with only the hypotheses the proof needs. Let p θ' be nonnegative probability densities with respect to ν for θ' near θ, with square-integrable score at θ, and let T be an estimator with finite second moment under p θ that is unbiased for g θ' near θ. If ∫ p θ' dν and ∫ T p θ' dν can be differentiated under the integral sign at θ, then g'(θ)² / I(θ) ≤ Var_θ T. When I(θ) = 0 the left side is the junk value 0 and the statement is trivial; the informative case is 0 < I(θ).

theorem cramerRao_general {ν : Measure 𝓧} {p : ℝ → 𝓧 → ℝ} {T : 𝓧 → ℝ} {g : ℝ → ℝ} {θ : ℝ}
    (hp_nonneg : ∀ θ' x, 0 ≤ p θ' x)
    (hp_int : ∀ᶠ θ' in 𝓝 θ, ∫ x, p θ' x ∂ν = 1)
    (hs_meas : AEStronglyMeasurable (fun x => deriv (fun θ' => p θ' x) θ) ν)
    (hI_int : Integrable (fun x => deriv (fun θ' => p θ' x) θ ^ 2 / p θ x) ν)
    (hT_meas : AEStronglyMeasurable T ν)
    (hT_sq : Integrable (fun x => T x ^ 2 * p θ x) ν)
    (h_unbiased : ∀ᶠ θ' in 𝓝 θ, ∫ x, T x * p θ' x ∂ν = g θ')
    (h_deriv_one : HasDerivAt (fun θ' => ∫ x, p θ' x ∂ν)
      (∫ x, deriv (fun θ' => p θ' x) θ ∂ν) θ)
    (h_deriv_T : HasDerivAt (fun θ' => ∫ x, T x * p θ' x ∂ν)
      (∫ x, T x * deriv (fun θ' => p θ' x) θ ∂ν) θ) :
    deriv g θ ^ 2 / fisherInformation ν p θ ≤ ∫ x, (T x - g θ) ^ 2 * p θ x ∂ν

Sources

• Cramér (1946), ch. 32; Rao (1945); Lehmann & Casella (1998), ch. 2.

Uses 2 · Used by 1

Statement usesFisher information

Proof usesCramér–Rao inequality, multiplicative form

Used byCramér–Rao inequality

TheoremCramér–Rao inequality#✓fully proved

Let p θ' be probability densities with respect to ν for θ' near θ, differentiable in the parameter at θ, with finite positive Fisher information I(θ), and let T be an estimator with finite second moment that is unbiased for g θ' near θ. If ∫ p θ' dν and ∫ T p θ' dν can be differentiated under the integral sign at θ, then Var_θ T ≥ g'(θ)² / I(θ). The hypotheses hp_meas, hp_diff and hI_pos are not needed; see cramerRao_general.

MathlibExt.Probability.Statistics.FisherInformation.cramerRao · 16 lines

theorem cramerRao {ν : Measure 𝓧} {p : ℝ → 𝓧 → ℝ} {T : 𝓧 → ℝ} {g : ℝ → ℝ} {θ : ℝ}
    (hp_nonneg : ∀ θ' x, 0 ≤ p θ' x)
    (hp_meas : AEStronglyMeasurable (p θ) ν)
    (hp_int : ∀ᶠ θ' in 𝓝 θ, ∫ x, p θ' x ∂ν = 1)
    (hp_diff : ∀ x, DifferentiableAt ℝ (fun θ' => p θ' x) θ)
    (hs_meas : AEStronglyMeasurable (fun x => deriv (fun θ' => p θ' x) θ) ν)
    (hI_int : Integrable (fun x => deriv (fun θ' => p θ' x) θ ^ 2 / p θ x) ν)
    (hI_pos : 0 < fisherInformation ν p θ)
    (hT_meas : AEStronglyMeasurable T ν)
    (hT_sq : Integrable (fun x => T x ^ 2 * p θ x) ν)
    (h_unbiased : ∀ᶠ θ' in 𝓝 θ, ∫ x, T x * p θ' x ∂ν = g θ')
    (h_deriv_one : HasDerivAt (fun θ' => ∫ x, p θ' x ∂ν)
      (∫ x, deriv (fun θ' => p θ' x) θ ∂ν) θ)
    (h_deriv_T : HasDerivAt (fun θ' => ∫ x, T x * p θ' x ∂ν)
      (∫ x, T x * deriv (fun θ' => p θ' x) θ ∂ν) θ) :
    deriv g θ ^ 2 / fisherInformation ν p θ ≤ ∫ x, (T x - g θ) ^ 2 * p θ x ∂ν

Sources

• Cramér (1946), ch. 32; Rao (1945); Lehmann & Casella (1998), ch. 2. Proves the deferred entry cramerRao.

Uses 2

Statement usesFisher information

Proof usesCramér–Rao inequality

TheoremWald's consistency theorem for maximum likelihood#✓fully proved

Wald's consistency theorem for maximum likelihood (Ferguson's form, positive densities). Let Θ be a compact metric space and p θ probability densities with respect to ν, positive, measurable in x and continuous in θ. Assume the model is identifiable (p θ = p θ₀ ν-a.e. only for θ = θ₀) and that the log-likelihood ratios have an upper envelope K integrable under p θ₀. Let X 0, X 1, … be independent with law p θ₀ ν, and let θhat n ω maximize the log-likelihood ∑_{i<n} log p θ (X i ω) over θ ∈ Θ. Then θhat n → θ₀ almost surely.

theorem ae_tendsto_maximumLikelihood {Θ : Type*} [MetricSpace Θ] [CompactSpace Θ]
    {ν : Measure 𝓧} {p : Θ → 𝓧 → ℝ} {θ₀ : Θ}
    (hp_pos : ∀ θ x, 0 < p θ x) (hp_meas : ∀ θ, Measurable (p θ))
    (hp_cont : ∀ x, Continuous fun θ => p θ x) (hp_int : ∀ θ, ∫ x, p θ x ∂ν = 1)
    (hident : ∀ θ, p θ =ᵐ[ν] p θ₀ → θ = θ₀)
    {K : 𝓧 → ℝ} (hK : Integrable K (lawOf ν p θ₀))
    (hK_bound : ∀ θ x, Real.log (p θ x) - Real.log (p θ₀ x) ≤ K x)
    {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P] {X : ℕ → Ω → 𝓧}
    (hX_law : ∀ i, HasLaw (X i) (lawOf ν p θ₀) P) (hX_indep : iIndepFun X P)
    {θhat : ℕ → Ω → Θ}
    (hmle : ∀ n ω θ, ∑ i ∈ Finset.range n, Real.log (p θ (X i ω)) ≤
      ∑ i ∈ Finset.range n, Real.log (p (θhat n ω) (X i ω))) :
    ∀ᵐ ω ∂P, Tendsto (fun n => θhat n ω) atTop (𝓝 θ₀)

Sources

• Wald (1949); Ferguson (1996), Theorem 17. Proves the deferred entry ae_tendsto_maximumLikelihood.

Uses 1

Statement usesProbability law of a density family member

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.