Likelihood and maximum likelihood estimators

9 fully proved

Probability Theory

StructureNormalized density family#✓fully proved

Let \(\Omega\) be a measurable space with a measure \(\mu\) and let \(\Theta\) be a set of parameters. A normalized density family on \(\Omega\) indexed by \(\Theta\) with dominating measure \(\mu\) consists of a function \(f_\theta : \Omega \to [0, \infty]\) for each \(\theta \in \Theta\) such that \(f_\theta\) is \(\mu\)-almost everywhere measurable and \(\int_\Omega f_\theta \, d\mu = 1\).

Taking \(\mu\) to be counting measure gives probability mass functions, and taking \(\mu\) to be volume gives probability density functions. The densities may take the value \(\infty\).

structure NormalizedDensityFamily (Ω : Type*) (Θ : Type*) [MeasurableSpace Ω]
    (μ : Measure Ω) where
  dens : Θ → Ω → ℝ≥0∞
  measurable : ∀ θ, AEMeasurable (dens θ) μ
  normalized : ∀ θ, ∫⁻ x, dens θ x ∂μ = 1

Used by 8

Used byNormalized density families are determined by their densities · Likelihood of an iid sample · Likelihood of the empty sample · Induced likelihood · Maximum likelihood estimator · Characterization of maximum likelihood estimators · Population laws are probability measures · Population law

Normalized Density Family

TheoremNormalized density families are determined by their densities#✓fully proved

Let \(F\) and \(G\) be normalized density families on a measurable space \(\Omega\) with the same parameter set \(\Theta\) and the same dominating measure \(\mu\). If for every \(\theta \in \Theta\) and every \(x \in \Omega\) the density of \(F\) at \(\theta\) and the density of \(G\) at \(\theta\) take the same value at \(x\), then \(F = G\).

Only the densities are compared; the measurability and normalization conditions are propositions.

@[ext]
theorem ext {F G : NormalizedDensityFamily Ω Θ μ}
    (h : ∀ θ x, F.dens θ x = G.dens θ x) : F = G

Uses 1

Statement usesNormalized density family

DefinitionPopulation law#✓fully proved

Let \(F\) be a normalized density family on a measurable space \(\Omega\) with parameter set \(\Theta\), dominating measure \(\mu\) and densities \(f_\theta\). The population law at \(\theta \in \Theta\) is the measure \(P_\theta\) on \(\Omega\) with density \(f_\theta\) with respect to \(\mu\), so that \(P_\theta(A) = \int_A f_\theta \, d\mu\) for every measurable set \(A \subseteq \Omega\).

noncomputable def law (F : NormalizedDensityFamily Ω Θ μ) (θ : Θ) :
    Measure Ω :=
  μ.withDensity (F.dens θ)

Uses 1 · Used by 1

Statement usesNormalized density family

Used byPopulation laws are probability measures

TheoremPopulation laws are probability measures#✓fully proved

Let \(F\) be a normalized density family on \(\Omega\) with parameter set \(\Theta\), dominating measure \(\mu\) and densities \(f_\theta\). For every \(\theta \in \Theta\), the population law \(P_\theta\), the measure with density \(f_\theta\) with respect to \(\mu\), is a probability measure.

theorem isProbabilityMeasure_law (F : NormalizedDensityFamily Ω Θ μ)
    (θ : Θ) : IsProbabilityMeasure (F.law θ)

Uses 2

Statement usesNormalized density family · Population law

DefinitionLikelihood of an iid sample#✓fully proved

Let \(F\) be a normalized density family on \(\Omega\) with parameter set \(\Theta\) and densities \(f_\theta\) for \(\theta \in \Theta\). For a sample size \(n\), a parameter \(\theta \in \Theta\) and a sample \(x = (x_0, \dots, x_{n-1}) \in \Omega^n\), the iid likelihood of \(\theta\) at \(x\) is \(L_n(\theta; x) = \prod_{i < n} f_\theta(x_i)\), a value in \([0, \infty]\). For \(n = 0\) this is the empty product \(1\).

noncomputable def iidLikelihood (F : NormalizedDensityFamily Ω Θ μ) (n : ℕ)
    (θ : Θ) (x : Fin n → Ω) : ℝ≥0∞ :=
  ∏ i, F.dens θ (x i)

Uses 1 · Used by 4

Statement usesNormalized density family

Used byLikelihood of the empty sample · Induced likelihood · Maximum likelihood estimator · Characterization of maximum likelihood estimators

TheoremLikelihood of the empty sample#✓fully proved

For a normalized density family \(F\), every parameter \(\theta\) and the empty sample \(x\) (sample size \(n = 0\)), the iid likelihood of \(\theta\) at \(x\) equals \(1\), the empty product.

@[simp]
theorem iidLikelihood_nil (F : NormalizedDensityFamily Ω Θ μ) (θ : Θ)
    (x : Fin 0 → Ω) : F.iidLikelihood 0 θ x = 1

Uses 2

Statement usesNormalized density family · Likelihood of an iid sample

DefinitionMaximum likelihood estimator#✓fully proved

Let \(F\) be a normalized density family on \(\Omega\) with parameter set \(\Theta\), let \(n\) be a sample size, and let \(L_n(\theta; x)\) denote the iid likelihood of \(\theta \in \Theta\) at a sample \(x \in \Omega^n\). A map \(\hat\theta\) from \(\Omega^n\) to \(\Theta\) is a maximum likelihood estimator for samples of size \(n\) if for every sample \(x \in \Omega^n\) the parameter \(\hat\theta(x)\) maximizes \(\theta \mapsto L_n(\theta; x)\) over all of \(\Theta\).

def IsMaximumLikelihoodEstimator (F : NormalizedDensityFamily Ω Θ μ) (n : ℕ)
    (θhat : (Fin n → Ω) → Θ) : Prop :=
  ∀ x, IsMaxOn (fun θ => F.iidLikelihood n θ x) Set.univ (θhat x)

Uses 2 · Used by 1

Statement usesNormalized density family · Likelihood of an iid sample

Used byCharacterization of maximum likelihood estimators

TheoremCharacterization of maximum likelihood estimators#✓fully proved

Let \(F\) be a normalized density family on \(\Omega\) with parameter set \(\Theta\), let \(n\) be a sample size, let \(L_n(\theta; x)\) denote the iid likelihood of \(\theta \in \Theta\) at a sample \(x \in \Omega^n\), and let \(\hat\theta\) be a map from \(\Omega^n\) to \(\Theta\). Then \(\hat\theta\) is a maximum likelihood estimator for samples of size \(n\) if and only if \(L_n(\theta; x) \le L_n(\hat\theta(x); x)\) for every sample \(x \in \Omega^n\) and every \(\theta \in \Theta\).

theorem isMaximumLikelihoodEstimator_iff (F : NormalizedDensityFamily Ω Θ μ)
    (n : ℕ) (θhat : (Fin n → Ω) → Θ) :
    F.IsMaximumLikelihoodEstimator n θhat ↔
      ∀ x θ, F.iidLikelihood n θ x ≤ F.iidLikelihood n (θhat x) x

Uses 3

Statement usesNormalized density family · Maximum likelihood estimator · Likelihood of an iid sample

DefinitionInduced likelihood#✓fully proved

Let \(F\) be a normalized density family on \(\Omega\) with parameter set \(\Theta\), let \(n\) be a sample size, let \(\tau : \Theta \to H\) be a map into a set \(H\), and let \(x \in \Omega^n\) be a sample. For \(\eta\) in the image of \(\tau\), the induced likelihood of \(\eta\) at \(x\) is the supremum, in \([0, \infty]\), of the iid likelihood \(L_n(\theta; x)\) over the fiber of \(\tau\) above \(\eta\):

\[L^*_n(\eta; x) = \sup_{\theta \in \Theta,\ \tau(\theta) = \eta} L_n(\theta; x).\]

Since \(\eta\) lies in the image of \(\tau\), the fiber is nonempty; no inverse of \(\tau\) is chosen.

noncomputable def inducedLikelihood (F : NormalizedDensityFamily Ω Θ μ)
    (n : ℕ) {H : Type*} (τ : Θ → H) (x : Fin n → Ω)
    (η : Set.range τ) : ℝ≥0∞ :=
  ⨆ θ : { θ : Θ // τ θ = η.val }, F.iidLikelihood n θ.val x

Uses 2

Statement usesNormalized density family · Likelihood of an iid sample

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.